Weighted labelled transition systems (WLTSs) are an established (meta-)model aiming to provide general results and tools for a wide range of systems such as non-deterministic, stochastic, and probabilistic systems. In order to encompass processes combining several quantitative aspects, extensions of the WLTS framework have been further proposed, state-to-function transition systems (FuTSs) and uniform labelled transition systems (ULTraSs) being two prominent examples. In this paper we show that this hierarchy of meta-models collapses when studied under the lens of bisimulation-coherent encodings.
Weighted labelled transition systems (WLTSs) [
In the wake of these encouraging results, other meta-models have been
proposed aiming to cover an even wider range of computational models and
concepts. Uniform labelled transition systems (ULTraSs) [
Given all these meta-models, it is natural to wonder about their expressiveness. We should consider not only the class of systems these frameworks can represent, but also whether these representations are faithful with respect to the properties we are interested in. Intuitively, a meta-model M is subsumed by M0 according to a property P if any system S which is an instance of M with the property P , is also an instance of M0 preserving P .
In this paper, we aim to classify meta-models according their ability to correctly express strong bisimulation. Therefore, in our contest a meta-model M is subsumed by M0 if any system S which is an instance of M, is also an instance of M0 preserving strong bisimulation.
Previous work [
In order to formally capture the notion of “expressiveness order between
system classes with respect to (strong) bisimulation”, we introduce the notion
of reduction between classes of systems. Although the driving motivation is
the study of the FuTSs hierarchy under the lens of bisimulation, the notion of
reduction is more general and, as defined in this work, can be used to study any
class of state-based transition systems. In fact, all the constructions and results
are developed abstracting from the “shape” of computation under scrutiny.
Synopsis Section 2 recalls an abstract and uniform account of transition systems
on discrete state spaces, akin to [
For an alphabet A and set of states X, the function space XA is understood as the set of all possible behaviours characterising deterministic input over A. In this context, a transition system exposing this computational behaviour is precisely described by a function α : X → XA mapping each state x ∈ X to some element in XA. For a function f : X → Y and φ ∈ XA, the assignment φ 7→ f ◦ φ defines a function (f )A : XA → Y A that extends the action of f from state spaces X and Y to behaviours defined over them in a coherent way. A function f : X → Y between the state spaces of systems (say, α : X → XA and β : Y → Y A) preserves and reflect their structure whenever f A ◦ α = β ◦ f . Since they preserve and reflect the transition structure of systems, these functions are called homomorphisms (which are functional bisimulations, cf. [17, Thm. 2.5]).
All the structures and observations described in the above example stem from
a single information: the “type” of the behaviour under scrutiny. This is well
understood as an endofunctor over the category of state spaces [
Non-deterministic transitions are captured by the powerset endofunctor P
mapping each set X its powerset PX and function f to its inverse image Pf i.e.
the function given by the assignment Z 7→ {f (z) | z ∈ Z}. Since subsets are
functions weighting elements over the monoid B = ({tt, ff}, ∨, ff), the above readily
extends to quantitative aspects (such as probability distributions, stochastic rates,
delays, etc.) by simply considering other a non-trivial abelian monoids1 [
(summation is well defined because φ is finitely supported, by above).
Probabilistic computations are a special case of the above where weight functions
are distributions (cf. [
From this perspective, D can be thought as a sort of “subtype” of F[0,∞). This situation is formalised by means of (component-wise) injective natural transformations (herein injective transformations). Composition and products of natural transformations are component-wise and the class of injective ones is closed under such operations. In general, for an injective transformation μ and a n endofunctor T , μT is again injective but T μ may not be so. The latter is injective given that T preserves injective maps i.e. T f is injective whenever f is injective. All the examples listed in this paper meet this mild assumption. Lemma 1. Any composition and product of Id, P, FM preserve injections. Example 1. The endofunctor PFM models the alternation of non-deterministic steps with quantitative aspects captured by (M, +, 0). There is an injective transformation η : Id → P whose components are given by the mapping x 7→ {x} and hence, by composition, ηFM : FM → PFM is an injective transformation. tu Definition 1. For an endofunctor T over Set, a transition system of type T ( T system) is a pair (X, α) where X is the set of states ( carrier) and α : X → T X is the transition map. For (X, α) and (Y, β) T -systems, a T -homomorphism from the former to the latter is a function f : X → Y s.t. T f ◦ α = f ◦ β. 1 An abelian monoid is a set M equipped with an associative and commutative binary operation + and a unit 0 for +; such structure is called trivial when M is a singleton.
Since system homomorphism composition is defined in terms of composition of the underlying functions on carriers it is immediate to check that the operation is associative and has identities. Therefore, any class of systems together with their homomorphisms defines a category.
We adopt the following notational conventions. A transition system (X, α)
is referred by its transition map only; in this case its carrier is written car(α).
Homomorphisms are denoted by their underlying function. Categories of systems
are written using sans serif font with Sys(T ) being the category of all T -systems
and T -homomorphisms and C|T its subcategory of systems in the category C.
Example 2 (LTSs). For a set A of labels, labelled transition systems are
(P−)Asystems, and image finite LTSs (Pf −)A-systems [
S ::= FM | FM ◦ S
where A and M range over (non-empty) sets of labels and (non-trivial) abelian
monoids, respectively. Any such endofunctor is equivalently described by:
(FM~ f )A~ , Qin=0(FM~ i f )Ai
and
(FM~ i f )Ai , (FMi,0 . . . FMi,mi f )Ai
for A~ = hA0, . . . , Ani a sequence of non-empty sets, M~ i = hMi,0, . . . , Mi,mi i a
sequence of non-trivial abelian monoids, and M~ = hM~ 0, . . . , M~ ni [
Several definitions of bisimulation found in literature use (more or less explicitly)
some sort of extension of equivalence relations from state spaces to behaviours
over these spaces. For instance, in [
4 ⇐⇒ ∀C ∈ X/R
Px∈C φ(x) = Px∈C ψ(x) .
This section defines equivalence extensions for arbitrary endofunctors (over Set) and studies how constructs such as composition or products reflect on these extensions, providing some degree of modularity.
Definition 2. For an equivalence relation R on X its T -extension is the equivalence relation RT on T X such that φ RT ψ ⇐4⇒ (T κ)(φ) = (T κ)(ψ) where κ : X → X/R is the canonical projection to the quotient induced by R.
As an example, let us consider the endofunctor (−)A describing deterministic inputs on A: the resulting extension for an equivalence relation R relates functions mapping the same inputs to states related by R. Formally: φ R(−)A ψ ⇐⇒ κ ◦ φ = κ ◦ ψ
⇐⇒ ∀a ∈ A (φ(a) R ψ(a)).
Extensions for P are precisely “subset closure” of relations (cf. [
Consider extensions for the endofunctor (P−)A describing LTSs: φ R(P−)A ψ ⇐⇒ ∀a ∈ A (∀y ∈ φ(a) ∃z ∈ ψ(a) (y R z)) ∧ (∀z ∈ ψ(a) ∃y ∈ φ(a) (y R z)) Clearly, RP(−)A can be equivalently written as
φ RP(−)A ψ ⇐⇒ ∀a ∈ A(φ(a) RP ψ(a)) which suggests some degree of modularity in the definition of extensions to composite endofunctors. In general, this kind of reformulations is not possible since for arbitrary endofunctors T ans S, it holds only that φ RS T ψ =⇒ φ RT ◦S ψ. The converse implication holds whenever T preserves injections. Lemma 2.
RS T ⊆ RT ◦S and RS T ⊇ RT ◦S , given T preserves injections.
Endofunctors modelling inputs, such as (−)A and (Pf −)A, can be seen as products (in these cases as powers) of endofunctors indexed over the input space A. As suggested by the above examples, for product endofunctors it holds that: φ R(Q Ti) ψ
⇐⇒ ∀i ∈ I(πi(φ) RTi πi(ψ)) where πi : Q TiX → TiX is the projection on the i-th component of the product. Lemma 3. For I 6= ∅ and {Ti}i∈I , R
Qi∈I Ti =∼ Qi∈I RTi .
FuTSs offer an instance of the above result: the endofunctor (FM~ −)A~ modelling FuTSs over M~ = hM~ 0, . . . , M~ ni and A~ = hA0; . . . ; Ani is a product indexed ~ over {(i, a) | i ≤ n ∧ a ∈ Ai}. Thus, the extension R(FM~ −)A is described by: ~ φ R(FM~ −)A ψ
⇐⇒ ∀i ≤ n∀a ∈ Ai(φi(a) RFM~ i ψi(a)).
For an equivalence relation R define its restriction to X as the equivalence relation R|X , R ∩ (X × X). Both (R|X )T and RT |T X are equivalence relations over the set of T -behaviours for X and, in general, the former is finer than the latter, unless T preserves injections—in such case, the two coincide. Lemma 4. For R and equivalence relation on Y and X ⊆ Y , (R|X )T ⊆ RT |T X , and, provided T preserves injections, (R|X )T ⊇ RT |T X .
Intuitively, this result allows us to encode multiple steps sharing the same computational aspects as single steps at the expense of bigger state spaces. In fact, it follows that (R|X )T n+1 = RT |T nX , assuming T preserves injections. Lemma 5. Let μ : T → S be an injective natural transformation. For R an equivalence relation on X, φ RT ψ ⇐⇒ μX (φ) RS μX (ψ). 4
In this section we give a general definition of bisimulation based on the notion of equivalence relation extension introduced above. This approach is somehow modular, as the definition reflects the structure of the endofunctors characterising systems under scrutiny. This allows to extend results developed in Section 3 to bisimulation and, in Section 5, to reductions.
Definition 3. An equivalence relation R is a strong T -bisimulation (herein, bisimulation) for a T -system α iff x R x0 =⇒ α(x) RT α(x0). We denote by bis(α) the set of all bisimulations for the system α.
The notion of bisimulations as per Definition 3 coincides with Aczel-Mendler’s
notion of precongruence [
Bisimulations for systems considered in this paper are known to be kernel
bisimulations (cf. [
Definition 5. A relation R on X is a kernel bisimulation for α : X → T X iff there is β : Y → T Y and f : α → β s.t. R is the kernel of the map underlying f .
In general, Definition 3 is stricter than Definition 5 but the two coincide for endofunctors preserving (enough) injections—e.g. any example from this paper. Corollary 1. For α : X → T X, the following are true: – A bisimulation for α is a kernel bisimulation for α. – If T preserves injections, a kernel bisimulation for α is a bisimulation for α.
From Corollary 1 and Lemma 1 it follows that Definition 3 captures strong
bisimulation for LTSs [
A special but well known instance of Lemma 6 is given by definitions of bisimulations found in the literature for LTSs, WLTSs and in general FuTSs. In fact, all these bisimulation contain a universal quantification over the set of labels. For instance, a R is a bisimulation for an LTS α : X → (PX)A iff: x R x0 =⇒ ∀a ∈ A (∀y ∈ φ(a) ∃z ∈ ψ(a) (y R z)) ∧ (∀z ∈ ψ(a) ∃y ∈ φ(a) (y R z)) that is, iff R is the intersection of an A-indexed family composed by a bisimulation for each transition system αa : X → PX projection of α on a ∈ A. Lemma 7. For n ∈ N and α ∈ Sys(T n+1), there is α ∈ Sys(T ) such that: – R ∈ bis(α) =⇒ ∃R0 ∈ bis(α)(R = R0|car(α)), – R ∈ bis(α) =⇒ R|car(α) ∈ bis(α).
Proof. Let X be `in=0 T iX and α : X → T (X) be [T ιnα0, T ι0α1 . . . , T ιn−2αn−1] where ιi : T iX → X is the i-th coproduct injection, α0 : X → T (T nX) is α, and αi+1 : T i+1X → T (T iX) is given by the identity for T i+1X. If R ∈ bis(α), then: (i) (ii) x R|X x0 =⇒ x R x0 =⇒ α(x) RT α(x0) ⇐⇒ α(x) RT |T n+1X α(x0) (iii) ⇐⇒ α(x) (R|X ) where (i) follows by R ∈ bis(α); (ii) follows by noting that α acts as α on X and hence both α(x) = α(x) and α(y) = α(y) are elements of T n+1X; (iii) follows by inductively applying Lemmas 2 and 4. Therefore, R|X ∈ bis(α).
Assume R ∈ bis(α) and define R = `in=0 RT i . By construction of R, x R x0 implies that x, x0 ∈ T iX for some i ∈ {0, . . . , n} meaning that the proof can be carried out by cases on each RT i composing R. Assume x, x0 ∈ T 0X = X, then: x R x0 ⇐⇒ x R x0 =(⇒i) α(x) RT n+1 α(x0) ⇐(i⇒i) α(x) (RT n )T α(x0) ⇐⇒ α(x) RT α(x0) ⇐⇒ α(x) RT α(x0) where (i) and (ii) follow by R ∈ bis(α) and Lemma 2, respectively. Assume x, x0 ∈ T i+1X, we have that:
x R x0 ⇐⇒ x RT i+1 x0 ⇐(i⇒) x (RT i )T x0 ⇐(i⇒i) α(x) (RT i )T α(x0)
where (i) and (ii) follow by Lemma 2 and by definition of α on T i+1X. Therefore,
R ∈ bis(α) and clearly R|X = R. tu
Lemma 7 and its proof provide us with an encoding from systems whose steps
are composed by multiple substeps to systems of substeps while preserving and
reflecting their semantics in term of bisimulations. The trade-off of the encoding
is a bigger statespace due to the explicit account of intermediate steps.
Lemma 8. For μ : T → S injective and α ∈ Sys(T ), bis(α) = bis(μcar(α) ◦ α).
By applying the Lemma 8 to Example 1 we conclude that that bisimulations for
ULTraSs coincide with bisimulations for WLTSs when these are seen as functional
ULTraS as shown in [
In this section we formalize the intuition that a behaviour “shape” is (at least) as expressive as another whenever systems and homomorphisms of the latter can be “encoded” as systems and homomorphisms of the former, provided that their semantically relevant structures are preserved and reflected.
Definition 6. For systems α and β, a (system) reduction σ : α → β is given by a function σc : car(α) → car(β) and a correspondence σb ⊆ bis(α) × bis(β) s.t. σc carries a relation homomorphism for any pair of bisimulations in σb, i.e.:
R σb R0 =⇒ (x R x0 ⇐⇒ σc(x) R0 σc(x0)).
A system reduction σ : α → β is called full if σc : car(α) → car(β) is surjective.
For σ : α → β a reduction, σc is always injective: the identity relation is always a bisimulation and hence condition (6) forces all x,x0 such that σc(x) = σc(x0) to be equal in the beginning. Therefore the correspondence σb is always left-unique hence a surjection from bis(β) to bis(α). This is indeed stronger than requiring preservation of bisimilarity since it entails that any bisimulation for α can be recovered by restricting some bisimulation for β to the image of car(α) in car(β) through the map σc. Fullness implies σc and σb are isomorphism. Remark 1. Condition (6) can be relaxed in two ways: (a) R σb R0 =⇒ (x R x0 =⇒ σc(x) R0 σc(x0)), (b) R σb R0 =⇒ (x R x0 ⇐= σc(x) R0 σc(x0)).
The condition (a) requires every bisimulation for α to be contained in some bisimulation for β whereas (b) requires every bisimulation for α to contain some bisimulation for β. Hence the two can be thought as completeness and soundness conditions for the reduction σ, respectively. tu
System reductions can be extended to whole categories of systems provided they respect the structure of homomorphisms. Formally: Definition 7. For C and D categories of system, a reduction σ from C to D, written σ : C → D, is a mapping that 1. assigns to any transition system α in C a system σ(α) in D and a system reduction σα : α → σ(α); 2. assigns to any f : α → β in C an homomorphism σ(f ) : σ(α) → σ(β) s.t.: (a) σβc ◦ f = σ(f ) ◦ σαc; (b) σ(idα) = idσ(α); (c) σ(g ◦ f ) = σ(g) ◦ σ(f ). A reduction σ : C → D is called full if, and only if, every system reduction σα is full. A category C is said to reduce (resp. fully reduce) to D, if there is a reduction (resp. full reduction) from the C to D.
Reductions can be easily composed at the level of their defining assignments. In particular, for reductions σ : C → D and τ : D → E, their composite reduction τ ◦ σ : C → E is a mapping that assigns to each system α the system (τ ◦ σ)(α) and the reduction given by (τ ◦ σ)cα , τσc(α) ◦ σαc and (τ ◦ σ)bα , τσb(α) ◦ σαb; and to each f : α → α0 the homorphism (τ ◦ σ)(f ). Reduction composition is associative and admits identities which are given on every C as the identity assignments for systems and homomorphisms. Any reduction restricts to a reduction from a subcategory of its domain and extends to a reduction to a super-category of its codomain. Moreover, fullness is preserved by the above operations.
For products, reductions can be given component-wise by suitable families of reductions that are “well-behaved” on homomorphisms. Formally: Definition 8. A family of reductions {σi : Ci → Di}i∈I is called coherent iff the following conditions hold for any i, j ∈ I: 1. if a function f extends to fi ∈ Ci then there is fj ∈ Cj s.t. f extends to fj ; 2. σi(fi) and σj (fj ) share their underlying function whenever fi and fj do. Theorem 2. A coherent family of (full) reductions {σi : Sys(Ti) → Sys(Si)}i∈I defines a (full) reduction σ : Sys(Qi∈I Ti) → Sys(Qi∈I Si). Proof. Assume {σi}i∈I as above. For α ∈ Sys(Q Ti) let αi = πi ◦ α and define σ(α) , h. . . , σi(αi), . . . i σαc , σic,αi σαb , Ti∈I σib,αi The assignment extends to all systems in Sys(Qi∈I Ti) and is well-defined by coherency and Lemma 6 since R σαb R0 ⇐⇒ ∀i ∈ I(R σib,αi R0) and for all i ∈ I, σαc = σic,αi . For any i ∈ I, f : α → β defines an homomorphism fi : αi → βi in Sys(Ti) sharing its underlying function. Define σ(f ) as the homomorphism arising from the function underlying σi(fi). By coherency, the mapping is well-defined and satisfies all the necessary conditions since all σi are reductions.
Correspondences for bisimulations presented in Lemmas 7 and 8 extend to reductions: injective transformations define full reductions and homogeneous systems reduce to systems for the base endofunctor, as formalised below. μˆcα , idcar(α), μˆbα , idbis(α), and μˆ(f ) , f .
Theorem 3. For μ : T → S an injective transformation, there is a full reduction μˆ : Sys(T ) → Sys(S) given, on each α and each f : α → β as μˆ(α) , μcar(α) ◦ α,
This theorem allows us to formalise the hierarchy shown in Section 1. For instance, the transformation described in Example 1 defines a full reduction from WLTSs to ULTraSs. Probabilistic systems are covered by the transformation induced by the inclusion DX ⊆ F[0,∞)X whereas the remaining cases are trivial. Theorem 4. If T preserves injections then Sys(T n+1) reduces to Sys(T ). Proof. Recall from Lemma 7 the construction of α : X → T X for any α : X → T n+1X and let ι0 : X → X denote the obvious injection. Define σ : Sys(T n+1) → Sys(T ) as the reduction given on each transition system α in Sys(T n+1) as σ(α) , α σαc , ι0
σαb , {(R, R) | R = R|X , R ∈ bis(α), R ∈ bis(α)} and on each homomorphism f : α → β in Sys(T n+1) as σ(f ) , `in=0 T if . By Lemma 7, σαb is a correspondence and by construction σ respects homomorphism composition and identities. Thus, σ is a reduction from Sys(T n+1) to Sys(T ). tu tu 6
In this section we apply the theory presented in the previous sections to prove that (categories of) FuTSs reduce to (categories of) simple FuTSs, i.e. WLTSs. The reduction is given in stages reflecting the endofunctors structure. Definition 9. A monoid sequence M~ is called homogeneous if its elements are the same. FuTSs on M~ are called homogeneous if M~ is homogeneous. Lemma 9. The FuTSs category fully reduces to that of homogeneous FuTSs. Proof. For a sequence of monoids M~ = hM0, . . . , Mni let N denote the product monoid Qin=0 Mi. Let 0j denote the unit of Mj . For each i ∈ {0, . . . , n}, the assignment x 7→ h00, . . . , 0i−1, x, 0i+1, . . . 0ni extends to an injective monoid homomorphism mi : Mi → N . The assignment φ 7→ mi ◦ φ defines an injective natural transformation FMi → FN which extends to an injective transformation FM~ → FN~ . We conclude by Theorems 2 and 3. tu Lemma 10. The nested FuTSs category reduces to that of simple FuTSs. Proof. By Lemma 9 and Theorems 2 and 4.
Lemma 11. The FuTSs category reduces to that of combined FuTSs. Proof. By Theorem 2 and Lemma 10. tu tu tu Lemma 12. The combined FuTSs category fully reduces to that of simple FuTSs. Proof. For a sequences A~ = hA0, . . . , Ani and M~ = hM0, . . . , Mni let B and N denote the cartesian product Qn i=0 Mi, respeci=0 Ai and the product monoid Qn tively. The mapping hφ0, . . . , φni 7→ λha0, . . . , ani.λx.hφ0(a0)(x), . . . , φn(an)(x)i extends to an injective natural transformation from (FM~ −)A~ = Qin=0 (FMi −)Ai to (FN −)B. We conclude by Theorem 3. tu Theorem 5. The FuTSs category reduces to that of simple FuTSs i.e. WLTSs. Proof. By Lemmas 11 and 12.
For instance, consider an ULTraS α : X → (Pf FM X)A. By Lemma 9 it fully reduces to a homogeneous nested FuTS (X, α0) for the sequences of labels and monoids hAi and hhB × M, B × M ii, respectively and such that: α0(x)(a)(φ) , (htt, 0i hff, 0i given ψ ∈ α(x)(a) s.t. φ(y) = hψ(y), 0i for all y ∈ X otherwise By Lemma 10, α0 reduces to the WLTS (X + FB×M X, α0) with labels from A, weights from B × M , and such that: y(y0) α0(y)(a)(y0) ,
if y ∈ FB×M X and y0 ∈ X hff, 0i α0(y)(a)(y0) if y ∈ X and y0 ∈ FB×M X
otherwise As exemplified by the above reduction for ULTraSs, FuTSs can be reduced to WLTSs by extending the original state space with weight functions and splitting steps accordingly. From this perspective, weight functions are hidden states in the original systems which the proposed reduction renders explicit. This observation highlights a trade-off between state and behaviour complexity of these semantically equivalent meta-models.
In this paper we have introduced a notion of reduction for categories of discrete
state transition systems, and some general results for deriving reductions from the
shape of computational aspects. As an application of this theory we have shown
that FuTSs reduce to WLTSs, thus collapsing the upper part of the hierarchy
in Section 1. Besides the classification interest, this result offers a solid bridge
for porting existing and new results from WLTSs to FuTSs. For instance, SOS
specifications formats presented in [
It remains an open question whether the hierarchy can be further collapsed,
especially when other notion of reduction are considered. In fact, requiring a
correspondence between bisimulations for the original and reduced systems may be
too restrictive in some applications like bisimilarity-based verification techniques.
This suggests to investigate laxer notions of reductions, such as those indicated
in Remark 1. Another direction is to consider different behavioural equivalences,
like trace equivalence or weak bisimulation. We remark that, as shown in [
Proof of Lemma 1 For f injective, the assignments ψ 7→ f ◦ ψ
Z 7→ {f (z) | z ∈ Z} φ 7→ λy. Px:f(x)=y φ(x) describe injective functions. tu tu tu Proof of Lemma 2 Let κS : SX → SX/RS be the canonical projection to the quotient induced by the equivalence relation RS. Since, by definition, κS(ρ) = κS(θ) implies (Sκ)(ρ) = (Sκ)(θ) there is a (unique) function qS : SX/RS → S(X/R) such that Sκ = qS ◦ κS. From T Sκ = T qS ◦ T κS and the definition of RT S and RS T , it follows that: φ RS T ψ =⇒ (T Sκ)(φ) = (T Sκ)(ψ) =⇒ φ RT S ψ proving first part of the thesis. Since ρ RS θ ⇐⇒ κS(ρ) = κS(θ) we conclude that qS is an injection and, by hypothesis, T qS is an injection too. Therefore: φ RT S ψ =⇒ (T Sκ)(φ) = (T Sκ)(ψ) =⇒ (T κS)(φ) = (T κS)(ψ) =⇒ φ RS T ψ completing the proof.
⇐⇒ φ Q RTi ψ Proof of Lemma 3 Write T for Qi∈I Ti and recall that Qi∈I Ti X is Qi∈I TiX. Then: φ RT ψ ⇐⇒ (Q Tiκ)(φ) = (Q Tiκ)(ψ) ⇐⇒ Q(Tiκ)(φi) = Q(Tiκ)(ψi) where κ : X → X/R is the canonical projection to the quotient induced by R and πi : Qi∈I TiX → TiX is the i-th projection. tu Proof of Lemma 4 Let κ : Y → Y /R and κ0 : X → X/R|X be the canonical projections induced by R and R|X , respectively. Since the latter is given by restriction of the former to X ⊆ Y , there is a unique and injective map q : X/R|X → Y /R such that κ = q ◦ κ. The first part of the thesis follows by: φ (R|X )T ψ =⇒ (T κ0)(φ) = (T κ0)(ψ) =⇒ (T κ)(φ) = (T κ)(ψ) =⇒ φ RT ψ
since T κ = T q ◦ T κ0.
On the other hand, by hypothesis on T , T q is injective and hence φ RT |T X ψ =⇒ (T κ)(φ) = (T κ)(ψ) =⇒ (T κ0)(φ) = (T κ0)(ψ)
=⇒ φ (R|X )T ψ Proof of Lemma 5 It holds that
(i) φ RT ψ ⇐⇒ T κ(φ) = T κ(ψ) ⇐⇒ (μX ◦ T κ)(φ) = (μX ◦ T κ)(ψ) (ii) ⇐⇒ (Sκ ◦ μX )(φ) = (Sκ ◦ μX )(ψ) ⇐⇒ μX (φ) RS μX (ψ) where (i) and (ii) follow by μX being injective and by μ being a natural transformation, respectively. Proof of Theorem 1 Assume R is a bisimulation for α : X → T X. For f, f 0 : X → Y s.t. x R x0 =⇒ f (x) = f 0(x0) we have that: x R x =⇒ α(x) RT α(x0) ⇐⇒ (T κ ◦ α)(x) = (T κ ◦ α)(x0) (i) =⇒ (T f ◦ α)(x) = (T f 0 ◦ α)(x0) where (i) follows by noting that, since κ : X → X/R is a canonical projection and x R x0 =⇒ f (x) = f 0(x0), there is (a unique) q : X/R → Y s.t. f = q ◦ κ = f 0.
Assume R is a precongruence for α, we have that: x R x ⇐⇒ κ(x) = κ(x0) =(i⇒i) (T κ ◦ α)(x) = (T κ ◦ α)(x0) (i) (iii) ⇐⇒ α(x) RT α(x0) where (i) follows by definition of κ : X → X/R, (ii) by R being a precongruence, and (iii) by definition of RT .
Proof of Corollary 1 By Theorem 1 and [19, Thm. 4.1].
Proof of Lemma 6 By Theorem 2, α(x) RT α(x0) ⇐⇒ α(x) Qi∈I RTi α(x0) and hence α(x) RT α(x0) ⇐⇒ ∀i ∈ I (πiα)(x) RiT (πiα)(x0). tu Proof of Lemma 8 For a relation R, R ∈ bis(α) iff x R y =⇒ α(x) RT α(y) and R ∈ bis(μX ◦ α) iff x R y =⇒ (μX ◦ α)(x) RS (μX ◦ α)(y). We conclude by Lemma 5.
Proof of Theorem 3 By Lemma 8. tu