BRICS RS-95-23 Cheng & Nielsen: Open Maps (at) Work

BRICS

Basic Research in Computer Science

Open Maps (at) Work

Allan Cheng Mogens Nielsen

BRICS Report Series RS-95-23 ISSN 0909-0878 April 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Open Maps (at) Work^{⋆}

Allan Cheng^{1} and Mogens Nielsen^{2}

1 Department of Computer Science, Cornell University, Ithaca NY 14853, USA

visiting from University of Aarhus, Denmark

                 e-mail: acheng@cs.cornell.edu

2 BRICS, Department of Computer Science, University of Aarhus, Denmark

                    e-mail: mn@daimi.aau.dk

Abstract. The notion of bisimilarity, as defined by Park and Milner, has turned out to be one of the most fundamental notions of operational equivalences in the field of process algebras. Not only does it induce a congruence (largest bisimulation) in CCS which have nice equational properties, it has also proven itself applicable for numerous models of parallel computation and settings such as Petri Nets and semantics of functional languages. In an attempt to understand the relationships and differences between the extensive amount of research within the field, Joyal, Nielsen, and Winskel recently presented an abstract categorytheoretic definition of bisimulation. They identify spans of morphisms satisfying certain “path lifting” properties, so-called open maps, as a possible abstract definition of bisimilarity. In [JNW93] they show, that they can capture Park and Milner’s bisimulation. The aim of this paper is to show that the abstract definition of bisimilarity is applicable “in practice” by showing how a representative selection of well-known bisimulations and equivalences, such as e.g. Hennessy’s testing equivalence, Milner and Sangiorgi’s barbed bisimulation, and Larsen and Skou’s probabilistic bisimulation, are captured in the setting of open maps and hence, that the proposed notion of open maps seems successful. Hence, we confirm that the treatment of strong bisimulation in [JNW93] is not a one-off application of open maps.

1 Introduction

As a response to some of the numerous models for concurrency proposed in the literature Winskel and Nielsen have used category theory as an attempt to understand the relationship between models like event structures, Petri nets, trace languages, and asynchronous transition systems [WN94]. From the algebraic point of view many of the operators of CCS like process algebras have been recasted using category-theoretic concepts such as products, co-products. However, a similar convincing category-theoretic way of adjoining abstract equivalences to a category of models had been missing until Joyal, Nielsen, and Winskel

⋆ This work has been supported by The Danish Research Councils, The Danish Research Academy, and BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation

proposed the notion of span of open maps [JNW93]. They show how these can capture Park and Milner’s strong bisimulation and identify a new bisimulation, strong history-preserving bisimulation, on models with independence like event structures and Petri nets.

As a measure of the applicability of open maps as an abstract definition of equivalences we show that it is possible to capture not only Park and Milner’s strong bisimulation but a representative selection of well-known bisimulations, such as e.g. Milner and Sangiorgi’s barbed bisimulation and Larsen and Skou’s probabilistic bisimulation. The presentation also serves as a tutorial on how open maps are applied. Although we do not identify new bisimulations, the reader should have no trouble using this setting on his or hers favourite model of computation. As an exercise, the reader is encouraged to prove the claims and proofs which are left out. Along, we make several observations clear which are either rather implicit in [JNW93, JNW94] or not mentioned at all.

The rest of the paper is structured as follows. In the next section we give a short stepwise introduction to open maps as presented in [JNW93, JNW94]. Then, in the subsequent sections, we apply the theory of open maps by instantiating the definitions with different models and notions of (simulation) morphisms and characterise the obtained abstract notion of equivalence operationally. It turns out that our choices of categories, which are guided by our intuitive understanding of what it means for a system to simulate another, yield well known notions of equivalence. More specifically, the following Sect. 3 to Sect. 7 are devoted to trace equivalence, weak bisimulation, testing equivalence, barbed bisimulation, and probabilistic bisimulation. In each of the sections we follow the steps presented in Sect. 2, the section recalling the general theory. Finally, in Sect. 8 we conclude with some remarks and hints for future research.

2 Open Maps, an Introduction

In this section we briefly recall the basic definitions from [JNW93].

As presented there, the general setting requires several steps. First, a category which represents a model of computation has to be identified. We denote this category M. A morphism m : X ⟶ Y in M should intuitively be thought of as a simulation of X in Y. Then, within M we choose a subcategory of “observation objects” and “observation extension” morphisms between these objects. We denote this category of observations by P. Given an observation (object) P in P and a model X in M. P is said to be an observable behaviour of X if there exists a morphism p : P ⟶ X in M.

Next, we identify morphisms m : X ⟶ Y which have the property that whenever an observable behaviour of X can be extended via f in Y then that extension can be matched by an extension of the observable behaviour in X.

Definition 1. Open Maps A morphism m : X ⟶ Y in M is said to be P-open if whenever f : O_{1} ⟶ O_{2} in P, p : O_{1} ⟶ X, q : O_{2} ⟶ Y in M, and the diagram

[figure: O_{1}; f; p; X; m; O_{2}; q; Y]  (1)

commutes, i.e. m ∘ p = q ∘ f, there exists a morphism h : O_{2} ⟶ X in M such that the two triangles in the diagram

[figure: O_{1}; f; p; X; m; O_{2}; h; q; Y]  (2)

commute, i.e. p = h ∘ f and q = m ∘ h. When no confusion is possible, we refer to P-open morphisms as open maps.

The abstract definition of bisimilarity is as follows.

Definition 2. P-bisimilarity Two models X and Y in M are said to be P-bisimilar, written X ∼_{P} Y, if there exists a span of open maps from a common object Z:

[figure: Z; m; m′; X; Y]  (3)

Notice that if M has pullbacks, it can be shown that ∼_{P} is an equivalence relation. The important observation is that pullbacks of open maps are themselves open maps. For more details, the reader is referred to [JNW93].

In the next sections, we proceed by following the above presented steps. As a preliminary example of a category of models of computation M we

present labelled transition systems.

Definition 3. A labelled transition system over Act is a tuple

(S, i, Act, ⟶) ,  (4)

where S is a set of states with initial state i, Act is a set of actions ranged over by α, β, …, and ⟶⊆ S × Act × S is the transition relation. For the sake of readability we introduce the following notation. Whenever (s_{0}, α_{1}, s_{1}),

(s_{1}, α_{2}, s_{2}), …, (s_{n−1}, α_{n}, s_{n}) ∈⟶ we denote this as s_{0} ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n}

or s_{0} ⟶^{v} s_{n} where v = α_{1}α_{2} ⋯ α_{n} ∈ Act^{∗}. Also, we assume that all states s ∈ S are reachable from i, i.e. there exists a v ∈ Act^{∗} such that i ⟶^{v} s.

Let us briefly remind the reader about Park and Milner’s definition of strong bisimulation.

Definition 4. Let T_{1} = (S_{1}, i_{1}, Act, ⟶_{1}) and T_{2} = (S_{2}, i_{2}, Act, ⟶_{2}). A strong bisimulation between T_{1} and T_{2} is a relation R ⊆ S_{1} × S_{2} such that

(i_{1}, i_{2}) ∈ R ,  (5)
((r, s) ∈ R ∧ r ⟶^{α}_{1} r′) ⇒ for some s′, (s ⟶^{α}_{2} s′ ∧ (r′, s′) ∈ R) , (6)
((r, s) ∈ R ∧ s ⟶^{α}_{2} s′) ⇒ for some r′, (r ⟶^{α}_{1} r′ ∧ (r′, s′) ∈ R) . (7)

T_{1} and T_{2} are said to be strongly bisimilar if there exists a strong bisimulation between them.

Henceforth, whenever no confusion is possible we drop the indexing subscripts on the transition relations and write ⟶ instead.

By defining morphisms between labelled transition systems we can obtain a category of models of computation, LTS, labelled transition systems.

Definition 5. Let T_{1} = (S_{1}, i_{1}, Act, ⟶_{1}) and T_{2} = (S_{2}, i_{2}, Act, ⟶_{2}). A morphism m : T_{1} ⟶ T_{2} is a function m : S_{1} ⟶ S_{2} such that

m(i_{1}) = i_{2} ,  (8)

s ⟶^{α}_{1} s′ ⇒ m(s) ⟶^{α}_{2} m(s′) .  (9)

Composition of morphisms is defined as the usual composition of functions. The intuition behind this specific choice of morphism is that an α labelled transition in T_{1} must be simulated by an α labelled transition in T_{2}.

If, as done in [JNW93], one chooses P as the full subcategory of M whose objects are finite synchronisation trees with at most one maximal branch, i.e. labelled transition systems of the form

i ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n} ,

P-bisimilarity corresponds to Park and Milner’s strong bisimulation. This follows from the following characterisation of P-open maps [JNW93].

Lemma 6. A morphism m : T_{1} ⟶ T_{2} is P-open if and only if it satisfies the following “zig-zag” property:

If m(r) ⟶^{α} s then there exists an r′ such that r ⟶^{α} r′ and m(r′) = s.

In the following sections we shall “rediscover” well-known behavioural equivalences by varying M and P. In the following, whenever we write e.g. M, P, or P-bisimilarity they refer to the specific choices of categories made in the section they appear.

3 Trace Equivalence

In this section we show how trace equivalence between two labelled transition systems can be captured by open maps. Trace equivalence is perhaps the first and simplest equivalence between labelled transition systems that one can think of. The result is based on the following important fact: Two labelled transition systems are trace equivalent if and only if their underlying deterministic transition systems are bisimilar.

First, we present the category LTS_{1} of labelled transition systems, which will corresponds to M. Then, we identify a subcategory, P, of observations. Finally, we show that P-bisimilarity corresponds to trace equivalence.

The object of LTS_{1} are the labelled transition systems (lts) from Definition 3. The following definition is needed in the definition of the morphisms in LTS_{1}.

Definition 7. Given an lts T = (S, i, Act, ⟶). For nonempty sets X, Y ⊆ S, we define X ⟶^{α} Y if Y = {r′ ∈ S | ∃ r ∈ X. r ⟶^{α} r′}. Notice that this transition relation is deterministic. As before, the transition relation can be generalised to a relation X ⟶^{v} Y, where v ∈ Act^{∗}. Furthermore, we define RS(T), the reachability set of T, to be the least subset of 2^{S}/{∅}, such that

{i} ∈ RS(T) ,  (10)
X ∈ RS(T) and X ⟶^{α} Y implies Y ∈ RS(T) .  (11)

Next, we define morphisms between two lts’s.

Definition 8. Given two lts’s, T_{j} = (S_{j}, i_{j}, Act, ⟶_{j}), j = 1, 2. A morphism m between T_{1} and T_{2} is a function m from RS(T_{1}) to RS(T_{2}), such that

m({i_{1}}) = {i_{2}} ,  (12)
X ⟶^{α} Y implies m(X) ⟶^{α} m(Y) .  (13)

Composition of morphisms is defined as the usual composition of functions. This defines the category LTS_{1}.

The intuition behind this definition of (simulating) morphism is that one is only interested in what action sequences an lts can perform. After performing a sequence σ = α_{1} ⋯ α_{n} of actions from the initial state i one may in general end up in several different states of T, i.e. a set X of states of T. These sets of states are exactly the elements of RS(T). Extending the sequence σ by performing another action α then corresponds to performing an α transition from X.

Next step is to define P.

Definition 9. Let P be the full subcategory of LTS_{1} whose objects are of the form

i ⟶^{α_{1}} r_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r_{n} ,  (14)

where all states are distinct.

Apart from showing that LTS_{1} has pullbacks, the construction in the following lemma will be referred to in the main theorem of this section. Also, it follows at once from the remarks in Sect. 2 that P-bisimilarity is an equivalence relation. We will also be able to conclude this after proving the main theorem of this section; it states that P-bisimilarity coincides with trace equivalence, which is know to be an equivalence relation. However, in general one cannot expect that P-bisimilarity coincides with a known equivalence relation. Lemmas as the following are sufficient for P-bisimilarity to be an equivalence relation.

Lemma 10. LTS_{1} has pullbacks.

Proof. Given a diagram

[figure: T_{1}; m_{1}; T_{2}; m_{2}; T]

Define an lts T′ = (S′, i′, Act, ⟶′) as follows. S′ ⊆ RS(T_{1}) × RS(T_{2}) and ⟶′⊆ (RS(T_{1}) × RS(T_{2})) × Act × (RS(T_{1}) × RS(T_{2})) are the least sets such that

– i′ = ({i_{1}}, {i_{2}}) ∈ S′

– If (X, Y) ∈ S′, X ⟶^{α} X′, Y ⟶^{α} Y′

then (X′, Y′) ∈ S′ and ((X, Y), α, (X′, Y′)) ∈⟶′.

Notice that because the transition relations on the reachability sets are deterministic it is the case that m_{1}(X) = m_{2}(Y) for any (X, Y) ∈ S′ and RS(T′) contains only singletons. Let π_{1} : T′ ⟶ T_{1} be defined as π_{1}({(X, Y)}) = X. It can be shown that π_{1} is well defined and is a morphism from T′ to T_{1}. We can define π_{2} : T′ ⟶ T_{2} in a similar way.

Given an lts T′′ and two morphisms f_{1} : T′′ ⟶ T_{1} and f_{2} : T′′ ⟶ T_{2} such that m_{1} ∘ f_{1} = m_{2} ∘ f_{2}. Define h : T′′ ⟶ T′ by h(Z) = (f_{1}(Z), f_{2}(Z)) for Z ∈ RS(T′′). From the definition of T′ is should be easy to see that h is a morphism; the initial state of T′′ is mapped to that of T′ and transitions are preserved. Furthermore we also have f_{1} = π_{1} ∘ h and f_{2} = π_{2} ∘ h. This is trivial, since there is at most one morphism between any two objects in LTS_{1}. Hence, h is also unique. This gives us the desired pullback. ⊓ ⊔

The next lemma characterises the open maps in LTS_{1}.

Lemma 11. A morphism m : T_{1} ⟶ T_{2} is P-open if and only if m : RS(T_{1}) ⟶ RS(T_{2}) has the following ”zig-zag” property

If m(X) ⟶^{α} Y′, then there exists an X′ such that X ⟶^{α} X′ and m(X′) = Y′.

Proof. Assume m is P-open and m(X) ⟶^{α} Y′. Then it must be the case that

X_{0} ⟶^{α_{1}} X_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} X_{n} for some X_{0}, …, X_{n} ∈ RS(T_{1}), where X_{0} = {i_{1}} and

X_{n} = X. Also, we have Y_{0} ⟶^{α_{1}} Y_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} Y_{n} ⟶^{α} Y′, where Y_{j} = m(X_{j}) for

0 ≤ j ≤ n. Let O_{1} be the observation

i ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n} ,

and O_{2} be the observation

i′ ⟶^{α_{1}} s′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s′_{n} ⟶^{α} s′_{n+1} .

Now let f denote the unique morphism from O_{1} to O_{2}, p denote the morphism that maps {i} to {i_{1}} and {s_{j}} to X_{j} for 1 ≤ j ≤ n, and q denote the morphism that maps {i′} to {i_{2}}, {s′_{j}} to Y_{j} for 1 ≤ j ≤ n, and {s′_{n+1}} to Y′. We then have m ∘ p = q ∘ f. From our assumptions it then follows that there exists a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. We now

conclude h({s′_{n}}) = h(f({s_{n}})) = p({s_{n}}) = X, h({s′_{n}}) ⟶^{α} h({s′_{n+1}}), and

m(h({s′_{n+1}})) = q({s′_{n+1}}) = Y′. Now choose X′ as h({s′_{n+1}}).

Conversely, assume m has the “zig-zag” property and we are given a commuting diagram

[figure: O_{1}; f; p; X; m; O_{2}; q; Y]

where O_{1} is an observations of the form

i ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n} ,

and O_{2} an observation of the form

i′ ⟶^{α_{1}} s′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{m}} s′_{m} ,

and n ≤ m. Notice f is uniquely determined (maps {s_{j}} to {s′_{j}} for 1 ≤ j ≤ n). We will show how to define a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. We start by defining h({i′}) = {i_{1}} and h({s′_{j}}) = p({s_{j}}) for 1 ≤ j ≤ n. Notice that we now already have p = h ∘ f for the partially defined h. Consequently, q = m ∘ h on {i′}, {s′_{1}}, …, {s′_{n}} because of the way f is defined and m ∘ p = q ∘ f. Now assume n < m. Since m(p({s_{n}})) = q(f({s_{n}})) = q({s′_{n}}) ⟶^{α_{n+1}} q({s′_{n+1}}) we know there must exist an X′ such that p({s_{n}}) ⟶^{α_{n+1}} X′ and m(X′) = q({s′_{n+1}}). Now define h({s′_{n+1}}) = X′. Then m(h({s′_{n+1}})) = q({s′_{n+1}}). Continuing this way for the remaining {s′_{n+2}}, …, {s′_{m}} we obtain the desired morphism. ⊓ ⊔ Definition 12. Given an lts T = (S, i, Act, ⟶). The traces/language of T, denoted L(T), is defined as

L(T) = {v ∈ Act^{∗} | i ⟶^{v} r for some r ∈ S} .  (15)

Two lts’s, T_{1} and T_{2}, are said to be trace equivalent if L(T_{1}) = L(T_{2}).

Theorem 13. Given two lts’s T_{1} and T_{2}. Then:

T_{1} and T_{2} are trace equivalent if and only if they are P-bisimilar.

Proof. The “if” direction follows from Lemma 11. For the “only if” direction, let F_{1} be the functor from LTS_{1} to LTS which sends an object T to (RS(T), {i}, Act, ⟶), where ⟶ was defined in Definition 7, and an morphism m : T ⟶ T′ to the obvious morphism between F_{1}(T) and F_{1}(T′) defined by m : RS(T) ⟶ RS(T′). Let F_{2} be the functor from LTS to LTS_{1} which maps an object to itself and a morphism m : T ⟶ T′ to the morphism determined uniquely by the induced function m : RS(T) ⟶ RS(T′). Since all observations of LTS_{1} are isomorphic to their image under F_{1} and there is at most one morphism between any two objects in LTS_{1}, we conclude, using Lemma 6, that F_{2} preserves open maps. So assume that T_{1} and T_{2} are trace equivalent. We then know that F_{1}(T_{1}) and F_{1}(T_{2}) are strong bisimilar. From Sect. 2 this implies that there exists a span of open maps in LTS, m_{1} : T ⟶ F_{1}(T_{1}) and m_{2} : T ⟶ F_{1}(T_{2}). Also, there clearly exist isomorphisms p_{1} : F_{2}(F_{1}(T_{1})) ⟶ T_{1} and p_{2} : F_{2}(F_{1}(T_{2})) ⟶ T_{2}. Since isomorphisms are always open maps we have the following span of open maps:

[figure: F_{2}(T); F_{2}(m_{1}); F_{2}(m_{2}); F_{2}(F_{1}(T_{1})); p_{1}; F_{2}(F_{1}(T_{2})); p_{2}; T_{1}; T_{2}]

We conclude that T_{1} and T_{2} are P-bisimilar. Observe that a construction similar to the one used in Lemma 10 would also have provided a span of open maps. ⊓ ⊔

Having identified trace equivalence we now continue by exploring other possibilities. In the next section we try to take “invisible” or “silent” actions into account.

4 Weak Bisimulation (Milner)

In this section we show that Milner’s weak bisimulation [Mil89] can be characterised using the general setting of Sect. 2.

Weak bisimulation differs from strong bisimulation in at least two respects. First, a special “invisible” action, usually denoted τ, is required to be a member of the set of labels. Second, an α labelled transition in one labelled transition system is no longer required to be simulated exactly by an α labelled transition in the other system. It may be preceded and succeeded by several τ transition.

We write r ⟹^{t} r′ if r ⟶^{τ^{∗}} r_{1} ⟶^{α_{1}} r′_{1} ⟶^{τ^{∗}} ⋯ ⟶^{τ^{∗}} r_{n} ⟶^{α_{n}} r′_{n} ⟶^{τ^{∗}} r′ for some

r_{1}, ⋯, r′_{n}. Furthermore, a τ transition needn’t be simulated by any transitions at all.

We start by defining a category LTS_{2}, labelled transition systems, and a subcategory of observations, P, in LTS_{2}. Then, we show that P-bisimilarity corresponds to Milner’s weak bisimulation.

The objects of LTS_{2} are the same as those from LTS. However, we assume that the set of actions Act contains a special “invisible” action τ. Guided by our intuitive understanding of how an action may be simulated, we define the morphisms between two lts’s as follows.

Definition 14. Given two lts’s, T_{j} = (S_{j}, i_{j}, Act, ⟶_{j}), j = 1, 2. A morphism between T_{1} and T_{2}, m : T_{1} ⟶ T_{2}, is a function m from S_{1} to S_{2}, such that

m(i_{1}) = i_{2} ,  (16)
r ⟶^{α} r′ implies m(r) \underrightarrow{_{α}} m(r′) .  (17)

The function : Act^{∗} ⟶ Act^{∗} removes all τ’s from its argument [Mil90].

Composition of morphisms is defined as the usual composition of functions. This defines the category LTS_{2}. P, the category of observations, is defined as follows.

Definition 15. Let P be the subcategory of LTS_{2} whose objects are of the form

i ⟶^{α_{1}} r_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r_{n} ,  (18)

where all the states are distinct. Moreover, there will be a morphism f from an observation

i ⟶^{α_{1}} r_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r_{n}  (19)

to another observation

i′ ⟶^{α_{1}} r′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r′_{n} ⟶^{α_{n+1}} ⋯ ⟶^{α_{n+k}} r′_{n+k} ,  (20)

if f(i) = i′, f(r_{j}) = r′_{j} for 1 ≤ j ≤ n, and k ≥ 0.

Notice that morphisms between observations are required to simulate action in the “strong” sense — e.g. no additional τ’s may be added. In the conclusion, Sect. 8, we will comment on this interesting choice. Allowing any morphism between two observations will in fact make P-bisimilarity stronger than weak bisimulation; the reader should have no major difficulties in going through the proofs. Lemma 17 will no longer be true, neither will the “only if” in Theorem 19.

Having defined M as LTS_{2} and P we now show that LTS_{2} has pullbacks.

Lemma 16. The category LTS_{2} has pullbacks.

Proof. Given a diagram

[figure: T_{1}; m_{1}; T_{2}; m_{2}; T]

Define T′ = (S′, i′, Act, ⟶′) as follows. S′ ⊆ S_{1} × S_{2} and ⟶′⊆ (S_{1} × S_{2}) × Act × (S_{1} × S_{2}) are the least sets such that

– i′ = (i_{1}, i_{2}) ∈ S′

– If (r, s) ∈ S′, r \underrightarrow{_{α}} r′, s \underrightarrow{_{α}} s′, and m_{1}(r′) = m_{2}(s′) then (r′, s′) ∈ S′ and

((r, s), α, (r′, s′)) ∈⟶′.

Define π_{1} : T′ ⟶ T_{1} and π_{2} : T′ ⟶ T_{2} as π_{1}((r, s)) = r and π_{2}((r, s)) = s. We now show that this defines a pullback. Clearly, π_{1} and π_{2} are morphisms.

Assume we have a commuting diagram

[figure: T′′; f; g; T_{2}; m_{2}; T_{1}; m_{1}; T]

Define h : S′′ ⟶ S_{1} × S_{2} as h(v) = (f(v), g(v)) for v ∈ S′′. It should be easy to see, using the commutativity of the diagram and the definition of T′, that h(v) ∈ S′, since v is reachable from i′′, and that v ⟶^{α} v′ in T′′ implies h(v) ⟶^{α} h(v′) in T′. h is then a well defined morphism from T′′ to T′. Also, f = π_{1} ∘ h and g = π_{2} ∘ h and moreover these equations determine h uniquely. Hence, T′, π_{1}, and π_{2} constitute a pullback. ⊓ ⊔

Next, we characterise the open maps.

Lemma 17. A morphism m : T_{1} ⟶ T_{2} is P-open if and only if it satisfies the following “zig-zag” property:

If m(r) ⟶^{α} s then there exists an r′ such that r \underrightarrow{_{α}} r′ and m(r′) = s.

Proof. Assume m is open and i_{1} ⟶^{α_{1}} r_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r_{n} = r. Let O_{1} be the observation

i ⟶^{α_{1}} r′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r′_{n} ,

O_{2} be the observation

i′ ⟶^{α_{1}} r′′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r′′_{n} ⟶^{α} s′′ ,

and f the unique morphism from O_{1} to O_{2}. Let p : O_{1} ⟶ T_{1} be the morphism which sends r′_{j} to r_{j} for 1 ≤ j ≤ n, and q : O_{2} ⟶ T_{2} the morphism that sends r′′_{j} to m(r_{j}) for 1 ≤ j ≤ n and s′′ to s. Then m ∘ p = q ∘ f and since m is an open map there exists a morphism h : O_{2} ⟶ T_{1} such that the two triangles in the diagram

[figure: O_{1}; f; p; T_{1}; m; O_{2}; h; q; T_{2}]

commutes. Since h(r′′_{n}) \underrightarrow{_{α}} h(s′′), h(r′′_{n}) = h(f(r′_{n})) = p(r′_{n}) = r_{n}, and s =

q(s′′) = m(h(s′′)), we conclude that h(r′′_{n}) = r_{n} = r \underrightarrow{_{α}} h(s′′) and m(h(s′′)) = s.

Hence, there exists a r′ = h(s′′) such that r \underrightarrow{_{α}} r′ and m(r′) = s.

For the other direction, assume m has the “zig-zag” property and we are given a commuting diagram of the form

[figure: O_{1}; f; p; T_{1}; m; O_{2}; q; T_{2}]

where O_{1} is an observation of the form

i ⟶^{α_{1}} r_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r_{n} ,

O_{2} is an observation of the form

i′ ⟶^{α_{1}} r′_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} r′_{n} ⟶^{α_{n+1}} ⋯ ⟶^{α_{n+k}} r′_{n+k} ,

and f : O_{1} ⟶ O_{2} is the uniquely determined morphism which sends r_{j} to r′_{j} for 1 ≤ j ≤ n.

We show that there exists a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. Apart from defining h(r′_{j}) = p(r_{j}) for 1 ≤ j ≤ n, and of course

h(i′) = i_{1}, let us consider which value we should give h(r′_{n+1}). Assume q(r′_{n}) \underrightarrow{_{α_{n+1}}}

q(r′_{n+1}) because q(r′_{n}) ⟶^{β_{1}} v_{1} ⟶^{β_{2}} ⋯ ⟶^{β_{l−1}} v_{l−1} ⟶^{β_{l}} q(r′_{n+1}), where l ≥ 0 and

α̂_{n+1} = β̂_{1} ⋯ β_{l}. By commutativity we have m(p(r_{n})) = q(r′_{n}) and by repeated use of the “zig-zag” property we conclude that there exist states w_{j} such that

p(r_{n}) \underrightarrow{_{β_{1}}} w_{1} \underrightarrow{_{β_{2}}} ⋯ \underrightarrow{_{β_{l}}} w_{l}, m(w_{j}) = v_{j} for 1 ≤ j < l, and m(w_{l}) = q(r′_{n+1}).

Define h(r′_{n+1}) = w_{l}. Then h(r′_{n}) \underrightarrow{_{α_{n+1}}} h(r′_{n+1}) and m(h(r′_{n+1})) = m(w_{l}) =

q(r′_{n+1}). Continuing this process for the remaining r′_{n+2}, …, r′_{n+k} it is easy to see that we obtain a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. Hence, m is an open map. ⊓ ⊔

For the sake of completeness we give Milner’s definition of weak bisimulation [Mil89], here adapted to the case where we consider initial states of lts’s.

Definition 18. Given two lts’s T_{1} and T_{2}. A relation R ⊆ S_{1} × S_{2} is said to be a weak bisimulation over T_{1} and T_{2} if

(i_{1}, i_{2}) ∈ R ,  (21)
((r, s) ∈ R ∧ r ⟶^{α} r′) ⇒ for some s′, (s \underrightarrow{_{α}} s′ ∧ (r′, s′) ∈ R) ,  (22)
((r, s) ∈ R ∧ s ⟶^{α} s′) ⇒ for some r′, (r \underrightarrow{_{α}} r′ ∧ (r′, s′) ∈ R) .  (23)

T_{1} and T_{2} are said to be weakly bisimilar if there exists a weak bisimulation as defined above.

We now show that P-bisimilarity coincides with weak bisimulation.

Theorem 19. Given two lts’s T_{1} and T_{2}. Then,

T_{1} and T_{2} are weakly bisimilar if and only if T_{1} and T_{2} are P-bisimilar.

Proof. Assume R is a weak bisimulation over T_{1} and T_{2}. Define T′ = (S′, i′, Act, ⟶′), where S′ ⊆ S_{1} × S_{2}, as follows. Let S′ and ⟶′ be the least sets such that

– i′ = (i_{1}, i_{2}) ∈ S′

– If (r, s) ∈ S′, r \underrightarrow{_{α}} r′, s \underrightarrow{_{α}} s′, and (r′, s′) ∈ R,

then (r′, s′) ∈ S′ and ((r, s), α, (r′, s′)) ∈⟶′.

Notice that S′ ⊆ R. Now define p : T′ ⟶ T_{1} as p((r, s)) = r and q : T′ ⟶ T_{2} as q((r, s)) = s. From the definitions and the above observation it should be easy to see that p and q are open maps, i.e. T_{1} and T_{2} are P-bisimilar.

Assume T_{1} and T_{2} are P-bisimilar, i.e. there exist a span of open maps

[figure: T; m_{1}; m_{2}; T_{1}; T_{2}]

It is enough to show that T and T_{1} are weakly bisimilar since weak bisimulation is an equivalence relation. Define R to be the least relation in S × S_{1} such that

– (i, i_{1}) ∈ R,

– If (r, s) ∈ R and r ⟶^{α} r′ then (r′, m_{1}(r′)) ∈ R, and

– If (r, s) ∈ R and s ⟶^{α} s′ then (r′, s′) ∈ R where r′ is any state such that

r \underrightarrow{_{α}} r′ and m_{1}(r′) = s′. Such a state exists by Lemma 17.

Notice that (r, s) ∈ R implies m_{1}(r) = s. Hence, in the last item s = m_{1}(r) \underrightarrow{_{α}} m_{1}(r′). It is now easy to show that R is a weak bisimulation over T and T_{1}. ⊓ ⊔

5 Testing Equivalence (Hennessy)

In this section we modify the category from Sect. 3 (basically) only with respect to the morphisms. We then choose a new subcategory P of observations. This time the elements of P will reflect a special type of branching structure. Then we show that the obtained P-bisimilarity coincides with Hennessy’s testing equivalence [Hen88]. Testing equivalence is slightly stronger than trace equivalence, due to an extra requirement on the set of possible actions, so-called acceptance sets, from states reached by performing a sequence of actions/labels.

We continue by defining a new category LTS_{3} of transition systems. The objects are those from LTS_{1} which are finitely branching, i.e. from every state only finitely many actions can be taken. Before defining the morphisms we need some definitions, inspired by [Hen88].

Definition 20. Let T = (S, i, Act, ⟶) be an lts. Let RS(T) denote the reachability set of T. For r ∈ S, X ∈ RS(T), and s ∈ Act^{∗} let

S_{T} (r) = {α ∈ Act | ∃r′. r ⟶^{α} r′} ,  (24)

A_{T} (r, s) = {S_{T} (r′) | r ⟶^{s} r′} ,  (25)

S_{T} (X) = {S_{T} (r) | r ∈ S} .  (26)

Notice that if {i} ⟶^{s} X for s ∈ Act^{∗} then {S_{T} (X)} = A_{T} (i, s). S_{T} (X) is the acceptance set of X.

The morphisms are now defined as follows.

Definition 21. Given two lts’s, T_{j} = (S_{j}, i_{j}, Act, ⟶_{j}), j = 1, 2. A morphism m between T_{1} and T_{2} is a function m from RS(T_{1}) to RS(T_{2}), such that

m({i_{1}}) = {i_{2}} ,  (27)
X ⟶^{α} X′ implies m(X) ⟶^{α} m(X′) ,  (28)
m(X) = Y ⇒ ∀A′ ∈ S_{T_{2}}(Y). ∃A ∈ S_{T_{1}}(X). A ⊆ A′ .  (29)

Notice how the definition of morphisms intuitively simulates Hennessy’s <<_{MAY} and <<_{MUST} pre-orders. Being guided by the definitions in [Hen88] and our results from Sect. 3, (27) and (28) reflect that we want traces to be simulated, and (29) reflects how acceptance sets are to be matched. Composition of morphisms is defined as the usual composition of functions. This defines the category LTS_{3}.

The subcategory P of observations will not consist of finite paths, but of trees consisting of a “trunk” and “branches” of length one, except for the “top” of the tree, where a more general branching structure is allowed.

Definition 22. Let P be the full subcategory of LTS_{3} whose objects are of the form

[figure: ·; i; α_{1,1}; α_{1,m_{1}}; ·; α_{2,1}; α_{2,m_{2}}; ·; ·; α_{n,1}; α_{n,mn}; ·; β_{1,1}; β_{1,k_{1}}; ·; ·; ·; ·; β_{mn,1}; β_{mn,km_{n}}; ·; ·]

where 0 ≤ m_{1}, …, m_{n}, k_{1}, …, k_{m_{n}} and all states are distinct.

Intuitively, the “trunk” corresponds to the observations in Sect. 3, i.e. it will ensure the existence of certain traces. The “top” of the the tree will ensure the existence of acceptance sets. The branches along the trunk are merely there for technical reasons. Think of a tree that has a trunk and only branches (of length one) at the top. Then allow branches of length one (“acceptance sets”) to “grow” at any node. This will produce an observation in P.

Lemma 23. The category LTS_{3} has pullbacks.

Proof. Assume we are given a diagram

[figure: T_{1}; m_{1}; T_{2}; m_{2}; T_{0}]

where T_{j} = (S_{j}, i_{j}, Act, ⟶_{j}), j = 0, 1, 2.

We start be defining an lts T = (S, i, Act, ⟶) as follows. S will consist of triples whose first, second, and third components are elements from RS(T_{1}), RS(T_{2}), and subsets of Act, respectively. S and ⟶ are defined to be the least set such that

– i = ({i_{1}}, {i_{2}}, S_{T_{1}}(i_{1}) ∩ S_{T_{2}}(i_{2})) ∈ S

– If (X, Y, C) ∈ S, α ∈ C, X ⟶^{α} X′, and Y ⟶^{α} Y′ then (X′, Y′, C′) ∈ S for

all C′ ∈ M(X′, Y′), where M(X′, Y′) = {A′ ∩ (⋃ S_{T_{2}}(Y′)) | A′ ∈ S_{T_{1}}(X′)} ∪

{B′ ∩ (⋃ S_{T_{1}}(X′)) | B′ ∈ S_{T_{2}}(Y′)}. Also, (X, Y, C) ⟶^{α} (X′, Y′, C′) for all

C′ ∈ M(X′, Y′).

It should be easy to see that T is an lts. For later use we notice the following facts.

– For (X, Y, C) ∈ S it is the case that S_{T} ((X, Y, C)) = C. This follows from the definition of C.

– It is the case that L(T) = L(T_{1})∩L(T_{2}). To see this note that L(T) ⊆ L(T_{1})∩ L(T_{2}) clearly holds. So choose any v ∈ L(T_{1}) ∩ L(T_{2}), where v = α_{1} ⋯ α_{n},

n ≥ 0. Then there exists X_{0} ⟶^{α_{1}} ⋯ ⟶^{α_{n}} X_{n} in T_{1} and Y_{0} ⟶^{α_{1}} ⋯ ⟶^{α_{n}} Y_{n} in

T_{2}, where X_{0} = {i_{1}} and Y_{0} = {i_{2}}. Also, there must exists A_{j} ∈ S_{T_{1}}(X_{j}) such that α_{j+1} ∈ A_{j} for 0 ≤ j < n and clearly we have α_{j+1} ∈ ⋃ S_{T_{2}}(Y_{j}) for

0 ≤ j < n. So (X_{0}, Y_{0}, A_{0} ∩⋃ S_{T_{2}}(Y_{0})) ⟶^{α_{1}} ⋯ ⟶^{α_{n}} (X_{n}, Y_{n}, A_{n} ∩⋃ S_{T_{2}}(Y_{n})).

Hence, v ∈ L(T).

– Given Z ∈ RS(T). Then there exist an X ∈ RS(T_{1}) and a Y ∈ RS(T_{2}) such that Z = {(X, Y, C) | C ∈ M(X, Y)}. This follows from that fact that the transitions are deterministic on RS(T_{1}) and RS(T_{2}).

Let us define π_{1} : T ⟶ T_{1} as follows (π_{2} is defined in a similar fashion). Given Z ∈ RS(T) let π_{1}(Z) = X, where X is the unique first component of the elements of Z. We now show that π_{1} is a morphism.

– Clearly π_{1}({i}) = {i_{1}}.

– Assume Z ⟶^{α} Z′, for Z, Z′ ∈ RS(T). Then by definition π_{1}(Z) ⟶^{α} π_{1}(Z′).

– Assume A ∈ S_{T_{1}}(X), where X = π_{1}(Z). By definition (X, Y, A∩⋃ S_{T_{2}}(Y)) ∈ Z, where π_{2}(Z) = Y. Also, S_{T} ((X, Y, A ∩ ⋃ S_{T_{2}}(Y)) = A ∩ ⋃ S_{T_{2}}(Y) ⊆ A. Hence, there exists an C ∈ S_{T} (Z) such that C ⊆ A.

Having argued for that π_{1} and π_{2} are morphisms it trivially follows that m_{1}∘π_{1} = m_{2} ∘ π_{2}.

Now assume that we are given a commuting square of the form

[figure: T′′; f_{1}; f_{2}; T_{1}; m_{1}; T_{2}; m_{2}; T_{0}]

We will show that there exists a morphism h : T′′ ⟶ T. We then necessarily have f_{1} = π_{1} ∘ f_{1} and f_{2} = π_{2} ∘ f_{2}. Hence, we will have the desired pullback. Define h : T′′ ⟶ T by h(V) = {(X, Y, C) | C ∈ M(X, Y)}, where X = f_{1}(V) and Y = f_{2}(V).

– Clearly h({i′′}) = i.

– If V ⟶^{α} V′ in T′′ then f_{1}(V) ⟶^{α} f_{1}(V′) and f_{2}(V) ⟶^{α} f_{2}(V′), and hence, by previous facts we conclude that h(V) ⟶^{α} h(V′).

– Assume C ∈ S_{T} (Z), where Z = h(V). By the previous facts we conclude that (X, Y, C) ∈ Z, where f_{1}(V) = X and f_{2}(V) = Y. Without loss of generality we may assume C is of the form A ∩ ⋃ S_{T_{2}}(Y) for A ∈ S_{T_{1}}(X). Since f_{1} is a morphism we know there exists a D ∈ S_{T′′}(V) such that D ⊆ A. Also, D ⊆ ⋃ S_{T_{2}}(Y) because f_{2} simulates the transitions from V by transitions from Y. Hence, D ⊆ A ∩ ⋃ S_{T_{2}}(Y).

This shows that h is a morphism and completes the proof of the lemma. ⊓ ⊔

Having defined M and P we now characterise the open maps.

Lemma 24. A morphism m : T_{1} ⟶ T_{2} is P-open if and only if m : RS(T_{1}) ⟶ RS(T_{2}) has the following ”zig-zag” property

If m(X) ⟶^{α} Y′, then there exists an X′ such that X ⟶^{α} X′ and m(X′) = Y′,

and ∀A ∈ S_{T_{1}}(X). ∃A′ ∈ S_{T_{2}}(m(X)). A′ ⊆ A .

Proof. Assume m is P-open.

– If m(X) ⟶^{α} Y′ then there exists

X_{0} ⟶^{α_{1}} X_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} X_{n} ,

with {i_{1}} = X_{0} and X = X_{n} in T_{1}. Let Y_{j} = m(X_{j}) for 0 ≤ j ≤ n and Y_{n+1} = Y′. Let O_{1} denote the following observation. For the sake of completeness we show the underlying deterministic transition system and right below the associated acceptance sets.

[figure: i; α_{1}; α_{1}; s_{1}; α_{2}; α_{2}; α_{n}; α_{n}; s_{n}; v_{1}; v_{2}; v_{n}]

\begin{matrix}\{i\} & ⟶^{α_{1}} & \{s_{1}, v_{1}\} & ⟶^{α_{2}} & ⋯ & ⟶^{α_{n−1}} & \{s_{n−1}, v_{n−1}\} & ⟶^{α_{n}} & \{s_{n}, v_{n}\} \\ \{\{α_{1}\}\} & & \{∅, \{α_{2}\}\} & & ⋯ & & \{∅, \{α_{n}\}\} & & \{∅\} \end{matrix}

Let O_{2} denote the following observation.

[figure: i′; α_{1}; α_{1}; s′_{1}; α_{2}; α_{2}; α_{n}; α_{n}; s′_{n}; α; α; s_{n+1}; v′_{1}; v′_{2}; v′_{n}; v′_{n+1}]

\begin{matrix}\{i′\} & ⟶^{α_{1}} & \{s′_{1}, v′_{1}\} & ⟶^{α_{2}} & ⋯ & ⟶^{α_{n}} & \{s′_{n}, v′_{n}\} & ⟶^{α} & \{s′_{n+1}, v′_{n+1}\} \\ \{\{α_{1}\}\} & & \{∅, \{α_{2}\}\} & & ⋯ & & \{∅, \{α\}\} & & \{∅\} \end{matrix}

It should be easy to see that there exists a unique morphism from O_{1} to O_{2}. Denote it f : O_{1} ⟶ O_{2}. Also, defining p : O_{1} ⟶ T_{1} by p({i}) = {i_{1}} and p({s_{j}, v_{j}}) = X_{j} for 1 ≤ j ≤ n yields a morphism. Similarly, q : O_{2} ⟶ T_{2} defined by q({i′}) = {i_{2}} and q({s′_{j}, v′_{j}}) for 1 ≤ j ≤ n + 1 is a morphism. Since there is at most one morphism between any two objects in LTS_{3} we conclude that m ∘ p = q ∘ f. Since m is P-open there exists a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. Now h({s′_{n}, v′_{n}}) =

h(f({s_{n}, v_{n}})) = p({s_{n}, v_{n}}) = X_{n} and since {s′_{n}, v′_{n}} ⟶^{α} {s′_{n+1}, v′_{n+1}}

we conclude h({s′_{n}, v′_{n}}) ⟶^{α} h({s′_{n+1}, v′_{n+1}}).Also, m(h({s′_{n+1}, v′_{n+1}})) =

q({s′_{n+1}, v′_{n+1}}) = Y_{n+1}. So we conclude that there exists an X′ such that

X ⟶^{α} X′ and m(X′) = Y′.

– Let A ∈ S_{T_{1}}(X). We have to show that there exists an A′ ∈ S_{T_{2}}(m(X)) such that A′ ⊆ A. As before, assume

X_{0} ⟶^{α_{1}} X_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} X_{n} ,

with {i_{1}} = X_{0} and X = X_{n} in T_{1}. Let Y_{0}, …, Y_{n} denote m(X_{0}), …, m(X_{n}). Let O_{1} denote the following observation.

[figure: i; α_{1}; α_{1}; s_{1}; α_{2}; α_{2}; α_{n}; α_{n}; s_{n}; v_{1}; v_{2}; v_{n}]

Let O_{2} denote

[figure: i′; α_{1}; α_{1}; s′_{1}; α_{2}; α_{2}; α_{n−1}; α_{n−1}; s′_{n−1}; α_{n}; α_{n}; T_{(n,1)}; v′_{1}; v′_{2}; v′_{n−1}; T_{(n,k)}]

where k = | S_{T_{2}}(Y) |, and if S_{T_{2}}(Y) = {A_{1}, …, A_{k}} then T_{(n,j)} denotes a tree of depth one, whose branches are labelled by A_{j}, for 1 ≤ j ≤ k. For completeness have show the reachability sets and the associated acceptance sets.

{i′} ⟶^{α_{1}} {s′_{1}, v′_{1}} ⋯ {s′_{n−1}, v′_{n−1}} ⟶^{α_{n}} {i_{(n,1)}, …, i_{(n,k)}} … X′_{1}
... X′_{k}
{{α_{1}}}  {∅, {α_{2}}} ⋯ {∅, {α}}  S_{T_{2}}(Y)  ∅

For the sake of clarity we have used X′_{1}, …, X′_{k} to denote the remaining reachability sets. As before, it should be easy to see that there exists a unique morphism f : O_{1} ⟶ O_{2}. Define p : O_{1} ⟶ T_{1} as before. Finally, define q({i′}) = Y_{1}, q({s′_{j}, v′_{j}}) = Y_{j} for 1 ≤ j ≤ n − 1, q({i_{(n,1)}, …, i_{(n,k)}}) = Y_{n}, and since the transitions from {i_{(n,1)}, …, i_{(n,k)}} can all be matched by those of Y_{n} (S_{T_{2}}(Y) = S_{O_{2}}({i_{(n,1)}, …, i_{(n,k)}})) it is possible to extend q uniquely to a morphism q : O_{2} ⟶ T_{2}. Notice how the requirements on the acceptance sets are fulfilled. As noted before, we then necessarily have m ∘ p = q ∘ f and therefore the existence of a morphism h : O_{2} ⟶ T_{1} such that p = h ∘ f and q = m ∘ h. Now the first equation tells us that h({i_{(n,1)}, …, i_{(n,k)}}) = X_{n}. Since A ∈ S_{T_{1}}(X_{n}) there must exist an A′ ∈ S_{O_{2}}({i_{(n,1)}, …, i_{(n,k)}}) such that A′ ⊆ A. But since S_{O_{2}}({i_{(n,1)}, …, i_{(n,k)}}) = S_{T_{2}}(Y_{n}) = S_{T_{2}}(m(X)), we are done.

Assume m has the “zig-zag” property. Given a commuting diagram

[figure: O_{1}; m; p; T_{1}; m; O_{2}; q; T_{2}]

Since m has the property that m(X) ⟶^{α} Y′ implies there exists X ⟶^{α} X′ such that m(X′) = Y′, transitions on the reachability sets are deterministic, and RS(O_{1}) together with the transitions has a tree structure, we can define h : O_{2} ⟶ T_{1} inductively as follows.

– h({i′}) = {i_{1}}

– If h(Y) has been defined, Y ⟶^{α} Y′, and h has not been defined on Y′ then define h(Y′) as follows. By induction we may assume q(Y) = m(h(Y)) and we know q(Y) ⟶^{α} q(Y′). Then there must exist a (necessarily unique) X′ such that h(Y) ⟶^{α} X′ and m(X′) = q(Y′). Define h(Y′) = X′. Notice also that for all A′ ∈ S_{T_{1}}(h(Y′)) there exists an A ∈ S_{O_{2}}(Y′) such that A ⊆ A′. This follows from m being P-open and q being a morphism; There must exist an A′′ ∈ S_{T_{2}}(m(h(Y′))) = S_{T_{2}}(q(Y′)) such that A′′ ⊆ A′ and also an A ∈ S_{O_{2}}(Y′) such that A ⊆ A′′.

Checking that h : O_{2} ⟶ T_{1} is a morphism is now routine work. The equations p = h ∘ f and q = m ∘ h now follows trivially. ⊓ ⊔

We continue by defining Hennessy’s testing equivalence.

Definition 25. Given two lts’s, T_{j} = (S_{j}, i_{j}, Act, ⟶_{j}), j = 1, 2. i_{1} is said to be testing equivalent to i_{2} if

L(T_{1}) = L(T_{2}) ,  (30)

and for any s ∈ L(T_{1})

∀A′ ∈ A(i_{2}, s). ∃A ∈ A(i_{1}, s). A ⊆ A′ ,  (31)
∀A ∈ A(i_{1}, s). ∃A′ ∈ A(i_{2}, s). A′ ⊆ A .  (32)

The above definition follows from Definition 2.8.8 in [Hen88]. Using the notation from [Hen88] the above definition can be rewritten to i_{1} <<_{MAY} i_{2}, i_{2} <<_{MAY} i_{1}, i_{1} <<_{MUST} i_{2}, and i_{2} <<_{MUST} i_{1}.

With the given choice of M and P it turns out that testing equivalence corresponds to P-bisimilarity.

Theorem 26. Given two lts’s T_{1} and T_{2}. Then,

T_{1} and T_{2} are testing equivalent if and only if T_{1} and T_{2} are P-bisimilar.

Proof. Assume T_{1} and T_{2} are testing equivalent. Define T = (S, i, Act, ⟶), π_{1} and π_{2} as in the proof of Lemma 23. By symmetry it is enough to show that π_{1} is P-open.

Let X = π_{1}(Z) for Z ∈ RS(T) and assume X ⟶^{α} X′. Assume X_{0} ⟶^{α_{1}}

X_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} X_{n} ⟶^{α} X′, where X_{0} = {i_{1}} and X_{n} = X. Since L(T_{1}) = L(T_{2})

we know that there exist Y_{0} ⟶^{α_{1}} Y_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} Y_{n} ⟶^{α} Y′ in T_{2}, where Y_{0} = {i_{2}}. Then necessarily Z ⟶^{α} Z′, where Z′ = {(X′, Y′, C) | C ∈ M(X′, Y′)} and π_{1}(Z′) = X′.

Let C ∈ S_{T} (Z), where Z ∈ RS(T). We conclude that (X, Y, C) ∈ Z, where Y = π_{2}(Z). There exists a v ∈ L(T) such that {i_{1}} ⟶^{v} X and {i_{2}} ⟶^{v} Y. Without loss of generality assume C is of the form A ∩ ⋃ S_{T_{2}}(Y), where A ∈ S_{T_{1}}(X), Consider any minimal (with respect to set inclusion) A_{min} ∈ S_{T_{1}}(X) such that A_{min} ⊆ A. Since S_{T_{1}}(X) = A(i_{1}, v) = A(i_{2}, v) = S_{T_{2}}(Y), we conclude A_{min} ∈ S_{T_{2}}(Y) and hence, A_{min} ⊆ ⋃ S_{T_{2}}(U). Hence, A_{min} ⊆ C, i.e. there exists an A′ ∈ S_{T_{1}}(X) such that A′ ⊆ C.

Next, assume T_{1} and T_{2} are P-bisimilar, i.e. there exists a span of open maps

[figure: T; m_{1}; m_{2}; T_{1}; T_{2}]

It is enough to show that T and T_{1} are testing equivalent. By Lemma 24 it follows easily that L(T) = L(T_{1}). Given an s ∈ L(T). Assume A ∈ A(i, s). We have to show that there exists an A_{1} ∈ A(i_{1}, s) such that A_{1} ⊆ A. Let X be the unique element in RS(T) such {i} ⟶^{s} X. Then A ∈ S_{T} (X). Since m_{1} is an open map there exists an A_{1} ∈ S_{T_{1}}(m(X)) such that A_{1} ⊆ A. Since A(i_{1}, s) = S_{T_{1}}(m(X)) we are done.

Now assume A_{1} ∈ A(i_{1}, s). We have to show that there exists an A ∈ A(i, s) such that A ⊆ A_{1}. Let X_{1} be the unique element from RS(T_{1}) such that {i_{1}} ⟶^{s} X_{1}. Then A_{1} ∈ S_{T_{1}}(X_{1}). Since m_{1} is open there exists an X ∈ RS(T) such that {i} ⟶^{s} X and m_{1}(X) = X_{1}. By the definition of morphisms there exists an A ∈ S_{T} (X) such that A ⊆ A_{1}. But since S_{T} (X) = A(i, s) we are done. Hence, T_{1} and T_{2} are testing equivalent. ⊓ ⊔

6 Barbed Bisimulation (Milner & Sangiorgi)

In this section we show how we can obtain Milner and Sangiorgi’s barbed bisimulation [MS92].

Barbed bisimulation differs from strong bisimulation in three obvious ways. First, as in the case of weak bisimulation, we distinguish between “visible” and “invisible” actions. Second, only τ transitions are required to be (bi)simulated. And third, only the existence of a “visible” transition has to be matched.

We start by defining the category of models LTS_{4}, then the subcategory of observations P, and finally we characterise the P-open maps and prove that P-bisimilarity coincides with barbed bisimulation.

Let LTS_{4} be the category of labelled transition systems (lts) whose objects are those from LTS. Again we assume that Act contains a special “invisible” action denoted τ. Before defining the morphisms of LTS_{4} we need the following definition.

Definition 27. Given an lts T = (S, i, Act, ⟶). R_{τ} (T), the set of τ-reachable states of T, is defined to be the set {s ∈ S | i ⟶^{τ} ⋯ ⟶^{τ} s}. We use the notation s↓ if there exist an α ∈ Act − {τ} and an s′ ∈ S such that s ⟶^{α} s′.

Morphisms between two lts in LTS_{4} are defined as follows:

Definition 28. Given two lts’s, T_{1} = (S_{1}, i_{1}, Act, ⟶_{1}) and T_{2} = (S_{2}, i_{2}, Act, ⟶_{2}). A morphism m from T_{1} to T_{2} is a function m : R_{τ} (T_{1}) ⟶ R_{τ} (T_{2}) such that

m(i_{1}) = i_{2} ,  (33)

r ⟶^{τ} r′ implies m(r) ⟶^{τ} m(r′) ,  (34)

r ↓ implies m(r)↓ .  (35)

This definition reflects that we only want to simulate τ’s and preserve the ↓ predicate. This corresponds well to our intuitive understanding of barbed (bi)simulation. Composition of morphisms is defined as the composition of the functions between the underlying τ-reachable states.

Next we define the category of observations.

Definition 29. Let P be the subcategory of LTS_{4} whose objects are of the form

i ⟶^{τ} r_{1} ⟶^{τ} ⋯ ⟶^{τ} r_{n−1} ⟶^{α} r_{n} ,  (36)

where α ∈ Act and all states are distinct.

Notice how the observations correspond to the τ-reachability of a state (r_{n}, when α = τ) and the ↓ predicate holding at it (r_{n−1}, when α ≠ τ).

Having defined M as LTS_{4} and P we show that LTS_{4} has pullbacks.

Lemma 30. The category LTS_{4} has pullbacks.

Proof. Given a diagram

[figure: T_{1}; m_{1}; T_{2}; m_{2}; T]

Define S′ ⊆ R_{τ} (T_{1}) × R_{τ} (T_{2}) and ⟶′ as the least sets such that

– (i_{1}, i_{2}) ∈ S′

– If (r, s) ∈ S′, r ⟶^{τ} r′, s ⟶^{τ} s′, and m_{1}(r′) = m_{2}(s′)

then (r′, s′) ∈ S′ and ((r, s), τ, (r′, s′)) ∈⟶′.

Intuitively, S′ is the τ-reachable states of the lts that will constitute the pullback. Now choose any α ∈ Act − {τ} and define

– S′′ = {(r′, s′)|∃(r, s) ∈ S′. r ⟶^{β} r′ ∧ s ⟶^{γ} s′ ∧ β ≠ τ ∧ γ ≠ τ}

– ⟶′′= {((r, s), α, (r′, s′)) | (r, s) ∈ S′ ∧ (r′, s′) ∈ S′′ ∧

∃β ≠ τ, γ ≠ τ. r ⟶^{β} r′ ∧ s ⟶^{γ} s′}

S′′ and ⟶′′ ensure that the ↓ predicate has the desired value at the states in S′. Now define T′ = (S′ ∪ S′′, (i_{1}, i_{2}), ⟶′ ∪ ⟶′′, Act), π_{1} : T′ ⟶ T_{1} as π_{1}((r, s)) = r, and π_{2} : T′ ⟶ T_{2} as π_{2}((r, s)) = s. It can be shown that T′, π_{1}, and π_{2} constitute a pullback of the above diagram. ⊓ ⊔

Next, we characterise the open maps.

Lemma 31. A morphism m : T_{1} ⟶ T_{2} is P-open if and only if it satisfies the following “zig-zag” property:

If m(r) ⟶^{τ} s then there exists an r′ such that r ⟶^{τ} r′ and m(r′) = s.

Also, m(r)↓ implies r ↓.

Proof. Assume m is open, r ∈ R_{τ} (T_{1}), and m(r) ⟶^{τ} s. We first prove the existence of the above mentioned r′. Assuming i_{1} ⟶^{τ} r_{1} ⟶^{τ} ⋯ ⟶^{τ} r_{n} = r, let O_{1} be the observation

i ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n} ,

and O_{2} the observation

i′ ⟶^{τ} s′_{1} ⟶^{τ} ⋯ ⟶^{τ} s′_{n} ⟶^{τ} s′ .

Let f : O_{1} ⟶ O_{2} be the unique function from O_{1} to O_{2} which sends s_{j} to s′_{j}, p : O_{1} ⟶ T_{1} the morphism which sends s_{j} to r_{j} for 1 ≤ j ≤ n, and q : O_{2} ⟶ T_{2} the morphism which sends s′_{j} to m(r_{j}), for 1 ≤ j ≤ n, and s′ to s. Then the diagram

[figure: O_{1}; f; p; T_{1}; m; O_{2}; q; T_{2}]

commutes, and there exists a morphism h : O_{2} ⟶ T_{1} such that p = h∘f and q = m ∘ h. Observe that h(s′_{n}) = h(f(s_{n})) = p(s_{n}) = r_{n}. Hence, r = r_{n} = h(s′_{n}) ⟶^{τ} h(s′). Also, m(h(s′)) = q(s′) = s. Now choose r′ = h(s′). Finally, assume m(r)↓

because m(r) ⟶^{α} s for α ≠ τ. Choosing O_{2} as i′ ⟶^{τ} s′_{1} ⟶^{τ} ⋯ ⟶^{τ} s′_{n} ⟶^{α} s′

and the other components as before (adjusting the morphisms in the obvious way) we obtain another commuting diagram and a morphism h′ : O_{2} ⟶ T_{1} such that the triangles commute. So h′(s′_{n}) = h′(f(s_{n})) = p(s_{n}) = r_{n} = r and since s′_{n} ↓ we have r ↓.

Assume m has the “zig-zag” property and the diagram

[figure: O_{1}; f; p; T_{1}; m; O_{2}; q; T_{2}]

commutes. We proceed by a case analysis on the shape of the observations O_{1} and O_{2}.

– Assume O_{1} is of the form i ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n} and O_{2} of the form

i′ ⟶^{τ} s′_{1} ⟶^{τ} ⋯ ⟶^{τ} s′_{n} ⟶^{τ} ⋯ ⟶^{τ} s′_{n+k}, where k ≥ 0.

Define h(s′_{j}) = p(s_{j}) for 1 ≤ j ≤ n. Next, we define h on s′_{n+1}. Since q(s′_{n}) = q(f(s_{n})) = m(p(s_{n})), p(s_{n}) ∈ R_{τ} (T_{1}), and m(p(s_{n})) ⟶^{τ} q(s′_{n+1}) there exists a r′ such that p(s_{n}) ⟶^{τ} r′ and m(r′) = q(s′_{n+1}). Define h(s′_{n+1}) = r′. Continuing this way for the remaining state s′_{n+2}, …, s′_{n+k} it can be shown that the produced h is a morphism from O_{2} to T_{1} such that p = h ∘ f and q = m ∘ h.

– Assume O_{1} is of the form i ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n−1} ⟶^{α} s_{n} and O_{2} of the

form i′ ⟶^{τ} s′_{1} ⟶^{τ} ⋯ ⟶^{τ} s′_{m−1} ⟶^{β} s′_{m}, where α ≠ τ and β ≠ τ.

Since f is a morphism we conclude n = m and f(s_{j}) = s′_{j} for 1 ≤ j ≤ n. It is then easy to see that h(s′_{j}) = p(s_{j}) for 1 ≤ j ≤ n defines a morphism from O_{2} to T_{1} such that p = h ∘ f and q = m ∘ h.

– Finally assume O_{1} is of the form i ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n} and O_{2} of the form

i′ ⟶^{τ} s′_{1} ⟶^{τ} ⋯ ⟶^{τ} s′_{m−1} ⟶^{α} s′_{m}, where α ≠ τ.

As before, we conclude m > n. Using the same procedure as in case 1, only this time observing that m(h(s′_{m−1})) = q(s′_{m−1}) ↓ implies h(s′_{m−1}) ↓, we obtain a morphism h : O_{2} ⟶ T_{1} such that the two triangles in the diagram commute.

We conclude that m is P-open. ⊓ ⊔

We now give Milner and Sangiorgi’s definition of barbed bisimulation adapted to the case where the labelled transition systems have initial states.

Definition 32. Given T_{1} and T_{2}. A barbed bisimulation over T_{1} and T_{2} is a relation R ⊆ R_{τ} (T_{1}) × R_{τ} (T_{2}) such that

(i_{1}, i_{2}) ∈ R ,  (37)
((r, s) ∈ R ∧ r ⟶^{τ} r′) ⇒ for some s′ (s ⟶^{τ} s′ ∧ (r′, s′) ∈ R) ,  (38)
((r, s) ∈ R ∧ s ⟶^{τ} s′) ⇒ for some r′ (r ⟶^{τ} r′ ∧ (r′, s′) ∈ R) ,  (39)
(r, s) ∈ R ⇒ (r ↓ ⇔ s↓) .  (40)

T_{1} and T_{2} are said to be barbed bisimilar if there exists such an R.

And now to the theorem relating P-bisimilarity to barbed bisimilarity.

Theorem 33. Given two lts’s, T_{1} and T_{2}. Then:

T_{1} is barbed bisimilar to T_{2} if and only if T_{1} and T_{2} are P-bisimilar.

Proof. Assume R is a barbed bisimulation over T_{1} and T_{2} and γ ∈ Act − {τ}. Now define

– S′ = {(r, s) ∈ R | ∃(r_{1}, s_{1}), …, (r_{n−1}, s_{n−1}) ∈ R.

i_{1} ⟶^{τ} r_{1} ⟶^{τ} ⋯ ⟶^{τ} r_{n−1} ⟶^{τ} r ∧

i_{2} ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n−1} ⟶^{τ} s},

– ⟶′= {((r, s), τ, (r′, s′)) | (r, s), (r′, s′) ∈ S′ ∧ r ⟶^{τ} r′ ∧ s ⟶^{τ} s′},

– S′′ = {(r′, s′) ∈ S_{1} × S_{2} | ∃(r, s) ∈ S′, α, β ∈ Act − {τ}.r ⟶^{α} r′ ∧ s ⟶^{β} s′},

– ⟶′′= {((r, s), γ, (r′, s′)) | (r, s) ∈ S′ ∧ (r′, s′) ∈ S′′ ∧

∃α, β ∈ Act − {τ}.r ⟶^{α} r′ ∧ s ⟶^{β} s′},

– T = (S′ ∪ S′′, (i_{1}, i_{2}), Act, ⟶′ ∪ ⟶′′),

– π_{1} : T ⟶ T_{1} by π_{1}((r, s)) = r, and

– π_{2} : T ⟶ T_{2} by π_{1}((r, s)) = s.

It can be shown that T is a lts and that π_{1} and π_{2} are morphisms. Without loss of generality we show that π_{1} is open. Choose any (r, s) ∈ R_{τ} (T).

– Assume π_{1}((r, s)) = r ⟶^{τ} r′. Since R_{τ} (T) = S′ ⊆ R and R was a barbed bisimulation over T_{1} and T_{2}, we know that there exists a s′ such that s ⟶^{τ} s′ and (r′, s′) ∈ R. But by definition of S′ we conclude (r′, s′) ∈ S′ and also

(r, s) ⟶^{τ} (r′, s′) in T, where π_{1}((r′, s′)) = r′.

– Assume that π_{1}((r, s)) = r ↓, i.e. there exists an r′ such that r ⟶^{α} r′ and α ≠ τ. Since (r, s) ∈ R_{τ} (T) we know that r ↓⇒ s ↓, i.e. there exists s′ such

that s ⟶^{β} s′ and β ≠ τ. But then (r′, s′) ∈ S′′ and ((r, s), γ, (r′, s′)) ∈⟶′′,

i.e. (r, s)↓.

Assume T_{1} and T_{2} are P-bisimilar. Then there must exist a span of open maps:

[figure: T; m_{1}; m_{2}; T_{1}; T_{2}]

It is sufficient to show that if m_{1} : T ⟶ T_{1} (m_{2} : T ⟶ T_{2}) is open then T and T_{1} (T_{2}) are barbed bisimilar, since being barbed bisimilar is an equivalence relation. So define R_{1} = {(r, m_{1}(r)) | r ∈ R_{τ} (T)}. We claim that R_{1} is a barbed bisimulation over T and T_{1}, namely;

– (i, i_{1}) ∈ R_{1},

– (r, s) ∈ R_{1} and r ⟶^{τ} r′ implies s = m_{1}(r) ⟶^{τ} m_{1}(r′) and (r′, m_{1}(r′)) ∈ R_{1},

– if (r, s) = (r, m_{1}(r)) ∈ R_{1} and m_{1}(r) ⟶^{τ} s′ then there exists an r′ such that r ⟶^{τ} r′ and m_{1}(r′) = s′, since m_{1} is open, and (r′, s′) = (r′, m_{1}(r′)) ∈ R_{1}, and

– if (r, s) ∈ R_{1} and r ↓ then s = m_{1}(r)↓ since m_{1} is a morphism and if s↓ then r ↓ since m_{1}(r) = s, r ∈ R_{τ} (T), and m_{1} is open.

This concludes the proof. ⊓ ⊔

7 Probabilistic Transition Systems (Larsen & Skou)

In this section we show that the probabilistic bisimulation of Larsen and Skou [LS91] can be characterised using the general setting in Sect. 2. We will however apply the theory in a slightly different way. Until now, we have tried to characterise P-bisimilarity between objects of M, for the specific choices of P and M. In this section we will focus on P-bisimilarity between objects of a subcategory of M. This application of the theory of open maps still turns out “successful”.

Intuitively, Larsen and Skou’s probabilistic bisimulation differs from strong bisimulation in at least two respects. First, to each labelled transition there is associated a real number from the interval [0; 1] which is to be understood as the probability with which the transition can be performed. Second, it is no longer single labelled transitions between two states that have to be matched but a set of identically labelled transitions into an equivalence class of probabilistic bisimilar states.

Based on [LS91] we start by defining a category PPTS, partial probabilistic transition systems, corresponding to M, and a subcategory of observations, P, in PPTS. Then, we show that P-bisimilarity in the full subcategory of probabilistic transition systems, PTS, in PPTS, corresponds to Larsen and Skou’s probabilistic bisimulation. Contrary to Larsen and Skou we do not assume lower limit on the probability of transitions. Because we wish to allow arbitrary small probabilities and for technical reasons, we consider IR^{∗}, the field of hyperreal numbers, instead of IR, the field of real numbers. IR^{∗} is the proper ordered extension of IR containing infinitesimals. An element ϵ ∈ IR^{∗} is infinitesimal if 0 < |ϵ| < r for all positive real numbers r. We reserve the symbol ϵ to denote infinitesimals. For a thorough presentation the reader is referred to [Kei76].

Definition 34. A partial probabilistic transition system (ppts) is a tuple

T = (P r, i, Act, Can, μ) ,  (41)

where P r is a set of processes (or states), i is the initial state, Act is the set of observable actions that processes may perform, Can is an Act-indexed family of sets of processes, and μ is a family of partial probability distributions indexed by states and actions. For any action a ∈ Act and any process r ∈ P r, r ∈ Can_{a} indicates that the process r can perform an a-action, in which case μ_{r,a} : P r → [0; 1] ⊆ IR^{∗} is a function such that ∑_{r′} μ_{r,a}(r′) ≤ 1.

In general, we do not require the sum to be equal to 1; hence the name partial probability distribution. If all μ_{r,a} are probability distributions, i.e. μ_{r,a} maps into the real numbers and ∑_{r′} μ_{r,a}(r′) = 1, we leave out the term partial and refer to T as a probabilistic transition system (pts). μ_{r,a}(r′) = μ can intuitively be read as “r can perform the action a and with probability μ become r′ ”.

Given a ppts T. We shall use the following notations:

r ⟶^{a}_{μ} r′ whenever r ∈ Can_{a} and μ_{r,a}(r′) = μ
r ⟶^{a} r′ whenever r ⟶^{a}_{μ} r′ for some μ > 0
r ⟶^{a} whenever r ∈ Can_{a}
r −̸→^{a} whenever r ∉ Can_{a}
r ⟶^{a}_{μ} S whenever S is any set of processes,
r ∈ Can_{a} and μ = ∑_{r′∈S} μ_{r,a}(r′).

We assume the set Act to be fixed and that all processes in P r are reachable from the initial state via transitions having non-zero probabilities. Finally, two ppts will be said to be distinct if their sets of processes are disjoint.

Next, we define morphisms between ppts’s.

Definition 35. A ppts-morphism f between two ptts’s, T_{j} = (P r_{j}, i_{j}, Act, Can_{j}, μ_{j}), j = 1, 2, is a function between P r_{1} and P r_{2} such that

f(i_{1}) = i_{2} ,  (42)

f(r) ⟶^{a} f(r′) whenever r ⟶^{a} r′ ,  (43)
If r ⟶^{a} r′ and f(r) ⟶^{a}_{μ′} f(r′) then ∑_{r\underrightarrow{a}μr′′f(r′′)=f(r′)}μ ≤ μ′ .  (44)

The intuition behind (44) is that all transitions from r in T_{1} which are simulated by a transition from f(r) can occur with a probability which is no higher than the probability of the simulating transition from f(r).

Let PPTS denote the category of partial probabilistic transition systems, whose objects are ppts’s and morphisms are ppts-morphisms, with composition of morphisms defined as the usual composition of functions. Let PTS denote the full subcategory of PPTS whose objects are pts’s.

In our model of computation, PPTS, we identify the following subcategory P of observations.

Definition 36. Let P be the full subcategory of PPTS whose objects are ppts’s of the following form

i ⟶^{a_{1}}_{ϵ_{1}} r_{1} ⟶^{a_{2}}_{ϵ_{2}} ⋯ ⟶^{a_{n}}_{ϵ_{n}} r_{n} ,  (45)

for some natural number n, distinct states, and actions a_{1}, …, a_{n} ∈ Act. Notice that all the probabilities are infinitesimals.

The intuition behind using only infinitesimals on the transitions is that we will only be interested in whether or not a transition can occur rather the probability with which is occurs. This is only true because PTS are the models which we consider.

This time, we postpone the investigation of the existence of pullbacks in PPTS. Instead, we now try to characterise the P-open maps in PPTS between any two pts’s.

Lemma 37. A morphism m : T_{1} ⟶ T_{2} between two pts’s is P-open if and only if it is “zig-zag” in the following sense:

If m(r) ⟶^{a} s then there exists an r′ such that r ⟶^{a} r′ and m(r′) = s.

Proof. Assume m is P-open and m(r) ⟶^{a} s. Since r is reachable from i_{1} there exists

i_{1} = r_{0} ⟶^{a_{1}} r_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} r_{n} = r

in T_{1}. Let O_{1} be any observation of the form

i ⟶^{a_{1}}_{ϵ_{1}} s_{1} ⟶^{a_{2}}_{ϵ_{2}} ⋯ ⟶^{a_{n}}_{ϵ_{n}} s_{n} ,

and O_{2} any observation of the form

i′ ⟶^{a_{1}}_{ϵ′_{1}} s′_{1} ⟶^{a_{2}}_{ϵ′_{2}} ⋯ ⟶^{a_{n}}_{ϵ′_{n}} s′_{n} ⟶^{a}_{ϵ′} s′ ,

where ϵ_{j} ≤ ϵ′_{j} for 1 ≤ j ≤ n. Let h denote the unique morphism between O_{1} and O_{2}, f denote the morphism from O_{1} to T_{1} which maps s_{j} into r_{j} for 1 ≤ j ≤ n, and g denote the morphism from O_{2} to T_{2} which maps O_{2} into

i_{2} = m(r_{0}) ⟶^{a_{1}} m(r_{1}) ⟶^{a_{2}} ⋯ ⟶^{a_{n}} m(r_{n}) = m(r) ⟶^{a} s .

It is easy to see, that the square

[figure: O_{1}; h; f; T_{1}; m; O_{2}; g; T_{2}]

commutes. But since m is P-open there exists a morphism m′ : O_{2} ⟶ T_{1} such that m′ ∘ h = f and m ∘ m′ = g. This implies the existence of an r′ such that

r ⟶^{a} r′ and m(r′) = s.

Conversely, assume that m is “zig-zag”. Let O_{1} and O_{2} be any two observations and f, g, and h any morphisms such that the square

[figure: O_{1}; h; f; T_{1}; m; O_{2}; g; T_{2}]

commutes. We now define a morphism m′ from O_{2} to T_{1} such that m′ ∘ h = f and m ∘ m′ = g.

Assume O_{1} has the form

i ⟶^{a_{1}}_{ϵ_{1}} r_{1} ⟶^{a_{2}}_{ϵ_{2}} ⋯ ⟶^{a_{n}}_{ϵ_{n}} r_{n} ,

and O_{2} has the form

i′ ⟶^{a_{1}}_{ϵ′_{1}} r′_{1} ⟶^{a_{2}}_{ϵ′_{2}} ⋯ ⟶^{a_{n}}_{ϵ′_{n}} r′_{n} ⟶^{a_{n+1}}_{ϵ′_{n+1}} ⋯ ⟶^{a_{n+k}}_{ϵ′_{n+k}} r′_{n+k} ,

where ϵ_{j} ≤ ϵ′_{j} for 1 ≤ j ≤ n. Apart from m′(i′) = i_{1}, we must define m′(r′_{j}) = f(r_{j}) for 1 ≤ j ≤ n. Since g(r′_{n}) = m(f(r_{n})) ⟶^{a_{n+1}} g(r′_{n+1}) and m is “zigzag”, there exists an s such that f(r_{n}) ⟶^{a_{n+1}} s and m(f(s)) = g(r′_{n+1}). Define m′(r_{n+1}) = s. Continuing this process for the remaining r′_{n+2}, …, r′_{n+k} we obtain the map m′ : O_{2} ⟶ T_{1}. It is now easy to show that m′ is indeed a morphism, since the transitions in the observations have infinitesimal probabilities, and that the “triangles” in the diagram commute. Hence, m must be P-open ⊓ ⊔

Going through the proof the reader should be able to realise why only infinitesimal probabilities are allowed on the observations from P. Allowing arbitrary probabilities would imply that two pts’s which are related by an open map m would be locally isomorphic in the following sense: if m(r) ⟶^{a}_{μ} s′, then there exists an r ⟶^{a}_{μ} r′ such that m(r′) = s′.

From the definition of the morphisms in PPTS one observes the following facts:

– If m : T_{1} ⟶ T_{2} and T_{1} is a pts then T_{2} must also be a pts.

– PPTS does not have pullbacks, neither does PTS. Consider the following example which illustrates three pts’s.

[figure: i; 1; a; i′; 0.55; a; 0.45; a; i′′; 0.5; a; 0.5; a; r; s; s′; s′′; s′′′]

Let T, T_{1}, and T_{2} denote the pts’s from left to right. Clearly there are uniquely determined morphisms from T_{1} to T and from T_{2} to T. Together, they form a diagram which does not have a pullback.

However, for P-bisimilarity to be an equivalence relation (a transitive relation, to be more precise) it is in general not necessary for the category M to have pullbacks. The following weaker result suffices.

Theorem 38. Given two P-open morphisms between pts’s, m_{1} : T_{1} ⟶ T_{0} and m_{2} : T_{2} ⟶ T_{0}. There exists a pts T and P-open morphisms π_{1} and π_{2} such that

[figure: T; π_{1}; π_{2}; T_{1}; m_{1}; T_{2}; m_{2}; T_{0}]

is a commuting square.

Proof. We define a pts, T = (P r, i, Act, Can, μ), and two maps π_{1} : T ⟶ T_{1}, π_{2} : T ⟶ T_{2} with the desired properties.

– Define S = {m_{1}^{−1}(r) × m_{2}^{−1}(r) | r ∈ P r_{0}}.

– Let P r ⊆ S and ⇝⊆ S × Act × [0; 1] × S be the least sets such that • i = (i_{1}, i_{2}) ∈ P r

• If (r, s) ∈ P r, r ⟶^{a}_{μ_{1}} r′, μ_{1} > 0, s ⟶^{a}_{μ_{2}} s′, μ_{2} > 0, m_{1}(r′) =

m_{2}(s′), and μ′ = \frac{μ_{1}μ_{2}}{μ}, where μ > 0 is uniquely determined by m_{1}(r) =

m_{2}(s) ⟶^{a}_{μ} m_{2}(s′) = m_{1}(r′), then (r′, s′)∈ P r and ((r, s), a, μ′, (r′, s′))∈

⇝, written (r, s) ⇝^{a}_{μ′} (r′, s′).

– Now for (r, s) ∈ P r, a ∈ Act define (r, s) ∈ Can_{a} if (r, s) ⇝^{a}_{μ} (r′, s′) for some

(r′, s′) ∈ P r. Also, define μ_{(r,s),a}((r′, s′)) = μ′ > 0 if (r, s) ⇝^{a}_{μ′} (r′, s′) and

otherwise 0.

– Define π_{1} : T ⟶ T_{1} by π_{1}((r, s)) = r and π_{2} : T ⟶ T_{2} by π_{2}((r, s)) = s.

It can be shown that π_{1} and π_{2} are morphisms. Here we merely show that T is a pts.

Clearly, all states in P r are reachable from the initial state. Since m_{1} and m_{2} form a co-span of open maps between pts’s we know e.g. that if m_{1}(r) ⟶^{a}_{μ} v then

μ = ∑_{r′m_{1}(r′)=v} μ_{r,a}(r′) = ∑_{r\underrightarrow{a}μr′m_{1}(r′)=v} μ .

Also, if (r, s) ∈ Can_{a} then (r, s) ⇝^{a}_{μ′} (r′, s′) for some μ′ > 0 and we have to show

∑_{(r′,s′)} μ_{(r,s),a}((r′s′)) = 1 .

It follows from the definition that r ∈ Can_{a} and s ∈ Can_{a}. We then have

∑_{(r′,s′)} μ_{(r,s),a}((r′s′))

= ∑_{I_{1}} ∑_{I_{2}} ∑_{I_{3}} \frac{μ_{1}μ_{2}}{μ}

= ∑_{I_{1}} ∑_{I_{2}} \frac{μ_{1}}{μ} ∑_{I_{3}} μ_{2}

= ∑_{I_{1}} ∑_{I_{2}} \frac{μ_{1}}{μ} μ

= ∑_{I_{1}} ∑_{I_{2}} μ_{1}

= ∑_{I_{1}} μ

= 1 .

where the index sets are

I_{1} = {v | m_{1}(r) ⟶^{a}_{μ} v ∧ μ > 0} ,

I_{2} = {r′ | r ⟶^{a}_{μ_{1}} r′ ∧ m_{1}(r′) = v} ,

and

I_{3} = {s′ | s ⟶^{a}_{μ_{2}} s′ ∧ m_{2}(s′) = v} .

⊓ ⊔

Noticing that the composition of two open maps is itself an open map [JNW93], we obtain the following corollary.

Corollary 39. P-bisimilarity between pts’s is an equivalence relation.

If, as done by Larsen and Skou in [LS91], we had assumed a lower limit γ on the probability of transitions (minimal probability assumption) and only considered the field of real numbers it would have been hard to obtain a result as the above, at least for us. The problem is that “pullback like” constructions of T involves expressions of the type \frac{μ_{1}μ_{2}}{μ} which may denote values smaller than γ.

Next, we recall the definition of probabilistic bisimulation from [LS91]. We have adapted it to the case where the probabilistic transition systems have initial states.

Definition 40. Let T_{j} = (P r_{j}, i_{j}, Act, Can_{j}, μ_{j}), where j = 1, 2, be two distinct pts’s. A probabilistic bisimulation between T_{1} and T_{2} is an equivalence ≡ on P r = P r_{1} ∪ P r_{2} such that i_{1} ≡ i_{2} and whenever r ≡ s, then the following holds:

∀a ∈ Act. ∀S ∈ P r/_{≡}. r ⟶^{a}_{μ} S ⇔ s ⟶^{a}_{μ} S ,  (46)

where the notation r ⟶^{a}_{μ} S was defined after Definition 34.

Now to the main result of this section.

Theorem 41. Given two pts’s, T_{1} and T_{2}. Then :

T_{1} is probabilistic bisimilar to T_{2} if and only if T_{1} is P-bisimilar to T_{2}.

Proof. Assume ≡ is a probabilistic bisimulation between T_{1} and T_{2}. We define a pts T = (P r, i, Act, Can, μ) and two P-open morphisms, m_{1} : T ⟶ T_{1} and m_{2} : T ⟶ T_{2}, which constitute a span of open maps, showing that T_{1} and T_{2} are P-bisimilar.

– Let S = {(r, s) ∈ P r_{1} × P r_{2} | r ≡ s}.

– Let P r ⊆ S and ⇝⊆ S × Act × [0; 1] × S be the least sets such that • i = (i_{1}, i_{2}) ∈ P r

• If (r, s) ∈ P r, r ⟶^{a}_{μ_{1}} r′, μ_{1} > 0, s ⟶^{a}_{μ_{2}} s′, μ_{2} > 0, r′ ≡ s′,

and μ′ = \frac{μ_{1}μ_{2}}{μ}, where μ > 0 is uniquely determined by r ⟶^{a}_{μ} [r′] and [r′] is the equivalence class of r′ under ≡, then (r′, s′) ∈ P r and

((r, s), a, μ′, (r′, s′)) ∈ ⇝, written (r, s) ⇝^{a}_{μ′} (r′, s′).

– Now for (r, s) ∈ P r, a ∈ Act define (r, s) ∈ Can_{a} if (r, s) ⇝^{a}_{μ} (r′, s′) for some

(r′, s′) ∈ P r. Also, define μ_{(r,s),a}((r′, s′)) = μ′ > 0 if (r, s) ⇝^{a}_{μ′} (r′, s′) and

otherwise 0.

– Define m_{1} : T ⟶ T_{1} by m_{1}((r, s)) = r and m_{2} : T ⟶ T_{2} by m_{2}((r, s)) = s.

It can be shown that T is a pts, that m_{1} and m_{2} are open maps, and that together they constitute the desired span of open maps.

Now assume there is a span of open maps:

[figure: T; m_{1}; m_{2}; T_{1}; T_{2}]

Define the relation ∼ ⊆ P r × P r as

r ∼ r′ if and only if m_{1}(r) = m_{1}(r′) or m_{2}(r) = m_{2}(r′) ,

and let ≈=∼^{∗}. Now define an equivalence relation ≡ on P r_{1} ∪ P r_{2} whose set of equivalence classes are

{m_{1}(S′) ∪ m_{2}(S′) | S′ ∈ P r/_{≈}} .

That ≡ is indeed an equivalence relation on P r_{1} ∪ P r_{2} follows from the definition of ≈ and that m_{1} and m_{2} are P-open morphisms, which implies that they are surjective functions.

We now claim that ≡ is a probabilistic bisimulation between T_{1} and T_{2}. This follows from the following observations (without loss of generality stated for T_{1}).

– i_{1} ≡ i_{2}.

– If s ∈ P r_{1}, a ∈ Act, and S is an equivalence class of ≡ then s ⟶^{a}_{μ} S if and only if s ⟶^{a}_{μ} (S ∩ P r_{1}). Also, for any r ∈ m_{1}^{−1}(s), s ⟶^{a}_{μ} S implies r ⟶^{a}_{μ} S′ for the unique equivalence class S′ = m_{1}^{−1}(S ∩ P r_{1}) ∈ P r/_{≈}, and

r ⟶^{a}_{μ} S′ for S′ ∈ P r/_{≈} implies m_{1}(r) ⟶^{a}_{μ} m_{1}(S′).

– For r_{1} ≈ r_{2} in T and any S′ ∈ P r/_{≈} we have r_{1} ⟶^{a}_{μ} S′ if and only if

r_{2} ⟶^{a}_{μ} S′.

⊓ ⊔

8 Conclusion

In this paper we have tried in practice to investigate the applicability of Joyal, Nielsen, and Winskel’s theory of open maps which was proposed as an abstract definition of equivalence in categories of models of computations.

Guided by our intuitive understanding of what it means for a system X to be simulated by a system Y we defined different categories of models of computation. Our choices of (sub)categories of observations were also guided by which behaviours ought to be observable.

It turned out that we could identify well-know notions of behavioural equivalences. We started by the most fundamental (or coarsest) namely, trace equivalence. Then, we considered “invisible” actions and identified weak bisimulation, testing equivalence, and barbed bisimulation.

Finally, in a more technical section, we showed how the theory of open maps could be relaxed and we identified Larsen and Skou’s probabilistic bisimulation. For technical reasons we applied the theory to a category in which the subcategory of observations was disjoint from the subcategory of models we were interested in.

Our results have shown that the theory of open maps does give meaningful equivalences when applied to well know models of computation.

We also noticed that the equivalences we identified could be captured by several different choices of observations. E.g., from the proofs in Sect. 5 it is clear that we could choose a smaller subcategory of observations; binary branching along the “trunks” of the trees is sufficient. A similar observation has been made in [JNW94] in connection with strong history preserving bisimulation. On the other hand, consider the characterisation of strong bisimulation from [JNW93] (see also Sect. 2). Had P been chosen to be of the form

[figure: s_{n,1}; i; α_{1}; s_{1}; α_{2}; α_{n−1}; s_{n−1}; α_{n,1}; α_{n,m}; s_{n,m}]

then an P-open map m would have been characterised by the usual “zig-zag” property

if m(r) ⟶^{α} s′, then there exists an r′ such that r ⟶^{α} r′ and m(r′) = s′,

and the additional “local bijection” property

for any α ∈ Act, {r′ | r ⟶^{α} r′} is in bijective correspondence with

{s′ | m(r) ⟶^{α} s′} under m.

So apart from helping identifying “characterising observations” for behavioural equivalences, the theory of open maps also allows us to test how “robust” an equivalence is against different choices of observations.

Also, the choice of simulating morphisms turned out to be important. In the category of labelled transition systems LTS we didn’t expect to be able to capture weak bisimulation just by changing the choice of observations. We defined new morphisms which intuitively corresponded to a “weak simulation”.

As for future work, the section on weak bisimulation can be seen as starting point to understand how weak bisimulations can be obtained abstractly from (strong) bisimulations using category theory. Glynn Winskel has observed that one can motivate the choice of morphism between the observations (which were the same as those used for characterising strong bisimulation in [JNW93]) from a category theoretical point of view using monads.

References

[Hen88] Matthew Hennessy. Algebraic Theory of Processes. MIT Press series in the foundations of computing, 1988.

[JNW93] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In Proc. LICS’93, Eighth Annual Symposium on Logic in Computer Science, pages 418–427, 1993.

[JNW94] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Research Series RS-94-7, BRICS, Department of Computer Science, University of Aarhus, May 1994. 42 pp. Journal version of LICS ’93 paper.

[Kei76] H. Jerome Keisler. Foundations of Infinitesimal Calculus. Prindle, Weber & Schmidt, Incorporated, 1976.

[LS91] Kim G. Larsen and Arne Skou. Bisimulation through Probabilistic Testing. Information and Computation, 94:1–28, 1991.

[Mil89] Robin Milner. Communication and Concurrency. Prentice Hall International Series In Computer Science, C. A. R. Hoare series editor, 1989.

[Mil90] Robin Milner. Operational and Algebraic Semantics of Concurrent Processes, chapter 19. Elsevier Science Publishers, 1990. in Handbook Of Theoretical Computer Science, editor J. van Leeuwen.

[MS92] Robin Milner and Davide Sangiorgi. Barbed Bisimulation. In Automata, Languages and Programming, 19th International Colloquium, Wien, Austria (Proc. ICALP’92), pages 685–695. Springer-Verlag (LNCS 623), July 1992.

[WN94] Glynn Winskel and Mogens Nielsen. Models for concurrency. Research Series RS-94-12, BRICS, Department of Computer Science, University of Aarhus, May 1994. 144 pp. To appear as a chapter in the Handbook of Logic and the Foundations of Computer Science, Oxford University Press.

This article was processed using the L^{A}TEX macro package with LLNCS style

Recent Publications in the BRICS Report Series

RS-95-23 Allan Cheng and Mogens Nielsen. Open Maps (at) Work. April 1995. 33 pp.

RS-95-22 Anna Ingólfsdóttir. A Semantic Theory for Value– Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.

RS-95-21 Jesper G. Henriksen, Ole J. L. Jensen, Michael E. Jrgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic Second-Order Logic in Practice. May 1995. 17 pp.

RS-95-20 Anders Kock. The Constructive Lift Monad. March 1995. 18 pp.

RS-95-19 François Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suffix and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp. To appear in Theoretical Computer Science.

RS-95-14 Devdatt P. Dubhashi. Inclusion–Exclusion(3) Implies Inclusion–Exclusion(n). February 1995. 6 pp.

RS-95-13 Torben Braüner. The Girard Translation Extended with Recursion. 1995. Full version of paper to appear in Proceedings of CSL ’94, LNCS, 1995.