BRICS RS-94-7 Joyal et al.: Bisimulation from Open Maps

BRICS

Basic Research in Computer Science

Bisimulation from Open Maps

Andr� e Joyal Mogens Nielsen Glynn Winskel

BRICS Report Series RS-94-7 ISSN 0909-0878 May 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, 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

Bisimulation from open maps

André Joyal,  Mogens Nielsen, Glynn Winskel
Dep.de math.et d’info., Comp. Sc. Dept., Comp. Sc. Dept.,
U.Q.A.M.,  Aarhus Univ.,  Aarhus Univ.,
Montreal,  Aarhus,  Aarhus,
Canada  Denmark  Denmark

May 11, 1994

Abstract

An abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets) and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner’s strong bisimulation. On event structures it explains and leads to a revision of history-preserving bisimulation of Rabinovitch and Traktenbrot, Goltz and van Glabeek. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. The general approach yields a logic, generalising Hennessy-Milner logic, which is characteristic for the generalised notion of bisimulation.

Introduction

There are confusingly many models for concurrency and all too many equivalences on them. To an extent their presentation as categories of models has helped explain and unify the apparent differences. But hitherto this category-theoretic approach has lacked any convincing way to adjoin abstract equivalences to these categories of models. This paper reports on an attempt: bisimulation between processes is expressed through the presence of a span of open maps between them.

The open maps are defined abstractly as being those morphisms which satisfy a path-lifting property. Intuitively a path represents a computation or history of a process. For the interleaving models of synchronisation trees and transition systems a computation path is naturally identified with a sequence of consecutive transitions starting at the initial state. For the noninterleaving (or independence) model of event structures a computation path is reasonably taken to be a slight generalisation of this to a partial order of events, and as the events are labelled, this amounts to a pomset [9]. The morphisms described, say f : X → Y, quite naturally have the feature that they preserve behaviour in the sense of sending computation paths of X to computation paths of Y. Roughly, open maps are required to satisfy the additional property that they preserve labels and, whenever a path of X can be extended via f in Y, then that extension can be matched by an extension of the path in X. As a first measure of success, this approach yields a uniform way to understand strong bisimulation on transition systems and history-preserving bisimulation on labelled event structures. This is only part of the story. The approach yields a notion of bisimulation on a relatively new model of transition systems with independence. Also, the concept of bisimulation induced on labelled event structures is not quite that originally proposed in [10] and [3] but, interestingly, a slight strengthening of the original definition. A logic of path assertions is exhibited— it can be viewed as a generalisation of Hennessy-Milner logic. Again it is general and applies to many different models, where it is a characteristic logic for the associated notion of bisimulation. The concept of open map appears in work of Joyal and Moerdijk (cf. [4]) where a concept of a subcategory of open maps of a (pre)topos is defined. The link with these ideas is made via embedding categories of synchronisation trees and labelled event structures in toposes of presheaves over categories of paths, chosen appropriately; in the case of synchronisation trees paths are simply finite branches while for labelled event structures they are finite pomsets. The embeddings are full and faithful and so give a way to generalize the established models to particular presheaf models. One advantage of the presheaf models is the automatic appearance of useful operations as Kan extensions. Another is the possibility of using the general axioms of Joyal and Moerdijk for open maps (and thus bisimulation).

1 Models

1.1 Transition systems

Transition systems are a frequently used model of parallel processes. They consist of a set of states, with an initial state, together with transitions between states which are labelled to specify the kind of events they represent.

Definition: A transition system is a structure

(S, i, L, tran)

where

• S is a set of states with initial state i,

• L is a set of labels,

• tran ⊆ S × L × S is the transition relation. As usual, a transition (s, a, s′) is drawn as s ^{\underline{a}}→ s′.

Definition: Let

T_{0} = (S_{0}, i_{0}, L_{0}, tran_{0}) and T_{1} = (S_{1}, i_{1}, L_{1}, tran_{1})

be transition systems. A morphism f : T_{0} → T_{1} is a pair f = (σ, λ) where

• σ : S_{0} → S_{1}, such that σ(i_{0}) = i_{1}, and

• λ : L_{0} ⇀ L_{1}, a partial function, which together satisfy

(s, a, s′) ∈ tran_{0} & λ(a) defined
⇒ (σ(s), λ(a), σ(s′)) ∈ tran_{1}, and
(s, a, s′) ∈ tran_{0} & λ(a) undefined ⇒ σ(s) = σ(s′).

Morphisms on transition systems represent a form of partial simulation; they preserve the initial state, and preserve or collapse transitions. The intention behind the definition of morphism is that the effect of a transition with label a in T_{0} leads to inaction in T_{1} precisely when λ(a) is undefined. Transition systems with morphisms form a category T in which the composition of two morphisms f = (σ, λ) : T_{0} → T_{1} and g = (σ′, λ′) : T_{1} → T_{2} is g ∘ f = (σ′ ∘ σ, λ′ ∘ λ) : T_{0} → T_{2} and the identity morphism for a transition system T has the form (1_{S}, 1_{L}) where 1_{S} is the identity function on states and 1_{L} is the identity function on the labelling set of T. (Here composition on the left of a pair is that of total functions while that on the right is of partial functions.)

1.2 Synchronisation trees

In his early, foundational work on CCS [6], Milner introduced synchronisation trees as a model of parallel processes and explained the meaning of the language of CCS in terms of operations on them.

Definition: A synchronisation tree is a transition system (S, i, L, tran) where

• every state is reachable,

• if s ^{\underline{a_{1}}}→ ⋯ ^{\underline{a_{n}}}→ s, for a string of labels a_{1}, …, a_{n}, then the string is empty (i.e. the transition system is acyclic), and

• s′ ^{\underline{a}}→ s & s′′ ^{\underline{b}}→ s ⇒ a = b & s′ = s′′.

Regarded in this way, we obtain a category S of synchronisation trees as a full subcategory of transition systems. The familiar operation of unfolding a transition system to a synchronisation tree appears as a right adjoint to the inclusion functor S ↪ T. Note that strings can be regarded as those special synchronisation trees consisting of a single branch.

1.3 Transition systems with independence

Transition systems with independence are precisely what their name suggests, viz. transition systems of the kind used to model languages like CCS and CSP but with an additional relation expressing when one transition is independent of another. They are closely related to Petri nets.

Definition: A transition system with independence is defined to be a structure

(S, i, L, tran, I)

where (S, i, L, tran) is a transition system and the independence relation I ⊆ tran^{2} is an irreflexive, symmetric relation, such that

(1) (s, a, s_{1}) ∼ (s, a, s_{2}) ⇒ s_{1} = s_{2}

(2) (s, a, s_{1})I(s_{1}, b, u) ⇒ ∃s_{2}. (s, a, s_{1})I(s, b, s_{2}) & (s, b, s_{2})I(s_{2}, a, u)

(3) (i) (s, a, s_{1}) ≺ (s_{2}, a, u)I(w, b, w′) ⇒ (s, a, s_{1})I(w, b, w′)

(ii) (w, b, w′)I(s, a, s_{1}) ≺ (s_{2}, a, u) ⇒ (w, b, w′)I(s_{2}, a, u)

where the relation ≺ between transitions is defined by

\begin{aligned}(s, a, s_{1}) ≺ (s_{2}, a, u) ⇔ ∃b. & (s, a, s_{1})I(s, b, s_{2}) & \\ & (s, a, s_{1})I(s_{1}, b, u) & (s, b, s_{2})I(s_{2}, a, u), \end{aligned}

and ∼ is the least equivalence relation including ≺.

Axiom (2) describes an intuitive property of independence; if two actions can occur consecutively and they are independent then they can occur in the opposite order. The relation ≺ expresses when two transitions represent occurrences of the same event; the situation (s, a, s_{1}) ≺ (s_{2}, a, u) means that there is a “square” of transitions

[figure: •; •; •; •; s; u; s_{1}; s_{2}; a; b; b; a]

with

(s, a, s_{1})I(s, b, s_{2}) & (s, a, s_{1})I(s_{1}, b, u) & (s, b, s_{2})I(s_{2}, a, u).

The relation ≺ extends to an equivalence relation ∼ between transitions; the equivalence classes {(s, a, s′)}_{∼}, of transitions (s, a, s′), are the events of the transition system with independence. (In fact, with this view of events, a transition system with independence determines a labelled asynchronous transition system—see [14]). Property (3) is then seen as asserting that the independence relation respects events; for the “square” of independent transitions above we must also have that

(s_{1}, b, u)I(s_{2}, a, u).

The first property (1) simply says that the occurrence of an event at a state yields a unique state. Note that property (1) implies the uniqueness of the state s_{2}, whose existence is asserted by (2). In reasoning about transition systems with independence it is sometimes useful to have a notation for representing independence squares like the one draw above. Sometimes we simply mark the square, as in:

[figure: I]

Sometimes we are more explicit about which transitions are independent of which others, and use an “angle” notation to connect independent transitions, as in

[figure]

—though it should always be born in mind that this graphical notation can be deceptive; some or all of the states in an independence square of a transition system with independence can be the same. A square of transitions

[figure]

shows two consecutively independent transition between a common pair of states— such a square of transitions in a transition system with independence need not be an independence square because the two first transitions need not be independent of each other. As morphisms on transition systems with independence we take morphisms on the underlying transition systems which preserve independence, i.e. a morphism (σ, λ) : T → T′ should satisfy:

If (s, a, s′) and (u, b, u′) are independent transitions of T and λ(a) and λ(b) are both defined, then (σ(s), λ(a), σ(s′)) and (σ(u), λ(b), σ(u′)) are independent transitions of T′.

Composition is inherited from that in T. We write TI for the category of transition systems with independence.

1.4 Event structures

Transition systems with independence unfold to event structures, which capture the significant possible event occurrences of a process, the consistency of event occurrences with each other, and how the occurrence of an event causally depends on the previous occurrence of others.

Definition: Define a (labelled) event structure to be a structure (E, ≤, Con, l) consisting of a set E, of events which are partially ordered by ≤, the causal dependency relation, a consistency relation Con consisting of finite subsets of events, and a labelling function l : E → L, which satisfy

{e′ | e′ ≤ e} is finite,
{e} ∈ Con,
Y ⊆ X ∈ Con ⇒ Y ∈ Con,
X ∈ Con & e ≤ e′ ∈ X ⇒ X ∪ {e} ∈ Con,

for all events e, e′ and their subsets X, Y. We say two events e, e′ ∈ E are concurrent, and write e co e′, iff

(e ≰ e′ & e′ ≰ e & {e, e′} ∈ Con).

The finiteness assumption restricts attention to discrete processes where an event occurrence depends only on finitely many previous occurrences. The remaining axioms express properties of the consistency relation to be thought of as asserting which finite subsets of events can occur together in a computation. For instance, the final condition says a consistent set can be closed downwards with respect to causal dependency and remain consistent. To understand the “dynamics” of an event structure (E, ≤, Con, l) we show how an event structure determines a transition system with independence (S, i, L, tran, I): Guided by our interpretation we can formulate a notion of computation state of an event structure, traditionally called a configuration. Taking a computation state of a process to be represented by the set x of events which have occurred in the computation, we expect that

e′ ∈ x & e ≤ e′ ⇒ e ∈ x

—if an event has occurred then all events on which it causally depends have occurred too—and also that

∀X ⊆^{fin} x. X ∈ Con

—the computation is consistent. We take S to consist of finite configurations of events, with ∅ being the initial state. If the labelling function has the form l : E → L, we take L as the labelling set of the transition system with independence. Its typical transitions have the form (x, a, x′) where x, x′ are states such that

∃e ∈ E. l(e) = a & e ∉ x & x′ = x ∪ {e}.

Independence on transitions is inherited from the concurrency relation on events: write (x, a, x′)I(y, b, y′) iff the unique events e_{1}, e_{2}, such that e_{1} ∈ x′ \ x & e_{2} ∈ y′ \ y, are concurrent, i.e. e_{1} co e_{2}. Event structures inherit morphisms from their identification with special kinds of transition systems with independence. Alternatively, here is a direct definition: A morphism of event structures consists of

(η, λ) : E → E′,

where E = (E, ≤, Con, l), E′ = (E′, ≤′, Con′, l′) are event structures, η : E ⇀ E′ is a partial function on events, λ : L ⇀ L′ is a partial function on labelling sets such that (i) l′ ∘ η = λ ∘ l,

(ii) If x is a configuration of E, then ηx is a configuration of E′ and if for e_{1}, e_{2} ∈ x their images are both defined with η(e_{1}) = η(e_{2}), then e_{1} = e_{2}.

Let E be the category of event structures with morphisms, as above, composed componentwise. Note that Pratt’s pomsets can be identified with special kinds of event structures, those without any conflict, precisely those event structures (E, ≤, Con, l) in which Con consists of all finite subsets of events E. On pomsets, event-structure morphisms amount to “partial-injective” functions on events—condition (ii) above, which respect a relabelling function—condition (i), and taking downwards-closed sets to downwards-closed sets with respect to ≤.

1.5 Relating the models

The four models are related by coreflections (i.e. adjunctions in which the units are natural isomorphisms)—see [14]:

[figure: S  T E  TI; se; st; tti; eti]

The left adjoints, drawn above, embed one model in another; those in a left-to-right direction are essentially inclusions with unfoldings as right adjoints. Synchronisation trees are simply special kinds of transition systems; the right adjoint of the inclusion st : S ↪ T is given on objects as the familiar operation of unfolding a transition system to a tree. When introducing event structures in Section 1.4 we showed how they determined transition systems with independence and inherited morphisms from the category TI; this gives the left adjoint eti from E to TI; its right adjoint is described in detail in [14], and sketched at the end of this section.^{1}A transition system can be regarded as a transition system with independence, one in which the independence relation is empty, yielding the functor tti, while the functor se specifies how a synchronisation tree determines an event structure—one in which events are arcs of the tree and causal dependency and consistency relations are got from the tree’s branches. Important constructions in giving semantics of process languages like Milner’s CCS, Hoare’s CSP, and OCCAM appear as universal constructions so the limit/colimit preservation properties of adjoints can be exploited in showing how semantics is respected in moving between models. When specifying a functor of one of the coreflections above we adopt a convention; for example, the left adjoint from E to TI is named eti while its right adjoint is tie. It is a consequence of the coreflection between E and TI that the left adjoint tie is full and faithful, and that E is equivalent as a category to that full subcategory of TI with objects those transition systems with independence at which the counit

1The handbook chapter [14] concentrates mainly on event structures for which consistency is determined by a binary conflict relation, for which the corrresponding transition systems with independence, asynchronous languages and Mazurkiewicz trace languages satisfy an extra axiom. The proofs for the slightly more general structures here proceed in essentially the same way, with the minor variations indicated in [14].

ε_{T} : eti ∘ tie(T) → T

is an isomorphism. (We shall sometimes find it useful to confuse event structures with the transition systems with independence corresponding to them.) Some contructions make use of the evident functors projecting objects down to their labelling sets and taking morphisms to their effect as partial functions between labelling sets. For example a morphism (σ, λ) : T_{0} → T_{1} of transition systems projects to the partial function λ : L_{0} ⇀ L_{1} between their labelling sets. With respect to this functor p, a fibre p^{−1}(L), over a set L, is that subcategory with objects those with common labelling set L and morphisms those whose image under p is 1_{L}, the identity on L. We will write the fibre of transition systems over a labelling set L as T_{L}, and follow a similar convention for the other categories. The well-known operations of restriction and relabelling appear as cartesian and cocartesian liftings. In fact, both the projection functors from transition systems and synchronisation trees to labelling sets form bifibrations. While the projection function from event structures does have all cocartesian liftings, the projections are not bifibrations in the cases of event structures and transition systems with independence. As will be seen (cf. Section 4), it is possible to enlarge our understanding of event structure to recover a bifibration, associated with operations of interest, as well as new refinement operations. The coreflections are fibrewise in the sense that they restrict to adjunctions between fibres over a common labelling set—the components of the unit and counit lie in the fibres. The four models have a central position in the theory of concurrency. They straddle an important divide in the treatment of parallelism. Models like transition systems and synchronisation trees are so-called “interleaving models”; they simulate parallelism by nondeterministic interleaving of atomic actions. In contrast event structures and transition systems with independence portray parallelism explicitly as a form of independence. The extra structure of independence can be important in, for example, certain liveness arguments. Petri nets are not dealt with explicitly here, chiefly because they are not as abstract (do not abstract away from the detailed representation) as the other models, and our present concern is that of abstract equivalence between models of processes. Two models here are however strongly related to Petri nets. Event structures are in coreflection with the category of labelled nets (see [13]). While by extending transition systems with independence to labelled asynchronous transition systems, which can have more than one transition with the same label between the same pair of states, we can obtain an adjunction with Petri nets—it cuts down to a coreflection on a rich subcategory of labelled asynchronous transition systems. As a consequence of these results, a semantics of CCS (or a language like it) in terms of Petri nets and one in terms of transition systems with independence “unfold” to the same event structure semantics (see [14]), and consequently to equivalent semantics with respect to the equivalences investigated here. The right adjoint to the function eti : E → TI is described in [14]; there it is shown how a transition system with independence corresponds to a special kind of labelled asynchronous transition system, how this determines a Mazurkiewicz trace language, which in turn gives rise to an event structure. Here we sketch a more direct, equivalent construction. It unfolds a transition system with independence T to a transition system with independence U(T) corresponding to an event structure; more precisely U(T) lies in that subcategory of TI equivalent to E under the coreflection. That this unfolding corresponds to an event structure we won’t prove here—it follows by the results of [14]. To within natural isomorphism, we are showing the result of applying the functor eti ∘ tie. Assume T is a transition system with independence in TI_{L}. We unfold this to another U(T) in TI_{L}. We obtain the states of U(T) as equivalence classes of “runs” of T, where a run is a sequence of consecutive transitions starting at the initial state, and is typically represented by:

i →^{a_{1}} s_{1} →^{a_{2}} ⋯ →^{a_{n}} s_{n}

Two runs should be equivalent (represent the same computation path) if they are the same but for following opposite sides of an independence square, as in the upper and lower contours of:

[figure: \begin{aligned}& & & & s_{m+1} \\ i & s_{1} & ⋯ & s_{m} & I & s_{m+2} & ⋯ & s_{n} \\ & & & & s′_{m+1} \end{aligned}; a_{m+2}; a_{1}; a_{2}; a_{m}; a_{m+1}; a_{m+2}; a_{m+3}; a_{n}; a_{m+1}]

The equivalence is the least equivalence relation with this property. The states of U(T) are its equivalence classes. We define there to be a transition u →^{b} v in U(T) between equivalence classes iff there is a run in v extending a run in u by a b-transition of T. Two transitions in U(T) are taken to be independent if they arise in this way from independent transitions of T. The construction U(T) is a transition system with independence. There is a “folding” morphism ε : U(T) → T in TI_{L} got by taking any equivalence class to the final state of (any of) its runs. To within isomorphism, ε is the component of the counit of the coreflection between E and TI. The operation U extends to functor, naturally isomorphic to eti ∘ tie; for a morphism f : T → T′ the action of U(f) on states of U(T) is induced by f’s action on runs.

2 Path-lifting morphisms

Informally, a computation path should represent a particular run or history of a process. For transition systems or synchronisation trees, a computation path is reasonably taken to be a sequence of transitions. Let’s suppose the sequence is finite. For a labelling set L, define the category of branches Bran_{L} to be the full subcategory of transition systems, with labelling set L, with objects those finite synchronisation trees with at most one maximal branch. A computation path in a transition system T, with labelling set L, can then be represented by a morphism

p : P → T

in T_{L} from an object P of Bran_{L}. How should we represent a computation path of a transition system with independence or an event structure? To take into account the explicit concurrency exhibited by an event structure, it is reasonable to represent a computation path as a morphism from a partial order of labelled events, that is from a pomset. Define the category of pomsets Pom_{L}, with respect to a labelling set L, to be the full subcategory of E_{L} whose objects consist exclusively of finite pomsets. A computation path in an event structure E, with labelling set L, is a morphism

p : P → E

in E_{L} from an object P of Pom_{L}. Because event structures and so pomsets embed in transition systems with independence TI, via the coreflection E → TI, the idea extends: a computation path in a transition system with independence T, with labelling set L, is represented by a morphism

p : P → T

in TI_{L} from the image P of an object of Pom_{L} under the coreflection. In future, when discussing transition systems with independence, we will deliberately confuse pomsets with their image in TI under the embedding. More precisely, assume a category of models M (this can be a fibre in any of the categories of models we are considering) and a choice of path category, a subcategory P ↪ M consisting of path objects (these could be branches, or pomsets) together with morphisms expressing how they can be extended. Define a path in an object X of M to be a morphism

p : P → X,

in M, where P is an object in P. A morphism f : X → Y in M takes such a path p in X to the path f ∘ p : P → Y in Y. The morphism f expresses the sense in which Y simulates X; any computation path in X is matched by the computation path f ∘ p in Y. We might demand a stronger condition of a morphism f : X → Y expressed succinctly in the following path-lifting condition: Whenever, for m : P → Q a morphism in P, a “square”

[figure: \begin{matrix}P & X \\ Q & Y \end{matrix}; m; p; f; q]

in M commutes, i.e. q ∘ m = f ∘ p, meaning the path f ∘ p in Y can be extended via m to a path q in Y, then there is a morphism p′ such that in the diagram

[figure: \begin{matrix}P & X \\ Q & Y \end{matrix}; m; p; f; p′; q]

the two “triangles” commute, i.e. p′ ∘ m = p and f ∘ p′ = q, meaning the path p can be extended via m to a path p′ in X which matches q. When the morphism f satisfies this condition we shall say it is P-open. It is easily checked that P-open morphisms include all the identity morphisms (in fact, all isomorphisms) of M and are closed under composition there; in other words they form a subcategory of M. For the well-known model of transition systems open morphisms are already familiar:

Proposition 1 With respect to a labelling set L, the Bran_{L}-open morphisms of T_{L} are the “zig-zag morphisms” of [12], the “p-morphism” of [11], the “abstraction homomorphisms” of [2], and the “pure morphisms” of [1], i.e. those label-preserving morphisms (σ, 1_{L}) : T → T′ on transition systems over labelling set L with the property that for all reachable states s of T

if σ(s) ^{\underline{a}}→ s′ in T′ then s ^{\underline{a}}→ u in T and σ(u) = s′, for some state u of T.

Proof: Suppose f = (σ, 1_{L}) : R → T′ is a Bran_{L}-open morphism of T_{L}. Let s be a reachable state of T such that σ(s) →^{a} s′ in T′. As s is reachable, there is a chain of transitions

i = s_{0} →^{a_{1}} s_{1} →^{a_{L}} ⋯ →^{a_{n}} s_{n} = s  (1)

in T starting from its initial state i. Let P be the branch

• →^{a_{1}} • →^{a_{2}} ⋯ →^{a_{n}} •

and p : P → T be the obvious path mapping P to the chain of transitions in (1). Let Q be the branch

• →^{a_{1}} • →^{a_{2}} ⋯ →^{a_{n}} • →^{a} •

and q : Q → T′ the path mapping it to

σ(s_{0}) →^{a_{1}} σ(s_{1}) →^{a_{2}} ⋯ → σ(s) →^{a} s′

in T′. Letting m : P → Q be the obvious (and unique) morphism in Bran_{L}, we observe that the diagram

[figure: \begin{matrix}P & T \\ Q & T_{′} \end{matrix}; p; m; f; q]

commutes. Because f is open there is a path r : Q → T, so that the two “triangles” commute in:

[figure: \begin{matrix}P & T \\ Q & T_{′} \end{matrix}; p; m; f; r; q]

the final state of Q, we obtain s′ →^{a} u and σ(u) = s′. Coversely, suppose f satisfies the “zig-zag” condition stated in Proposition 1. Suppose

[figure: \begin{matrix}P & T \\ Q & T_{′} \end{matrix}; p; m; f; q]

commutes for P, Q in Bran_{L}. Observe that, to within isomorphism, Q is simply an extension of P by extra transitions. Repeated use of the “zig-zag” conditions yields a morphism r : Q → T such that r ∘ m = p and f ∘ r = q. □

Let us return to the general set-up, assuming a path category P in a category of models M. Say two objects X_{1}, X_{2} of M are P-bisimilar iff there is a span of P-open morphisms f_{1}, f_{2}:

[figure: \begin{aligned}& X \\ X_{1} & & X_{2} \end{aligned}; f_{1}; f_{2}]

For the interleaving models of transition systems and synchronisation trees with path category P taken to be branches, P-bisimulation coincides with Milner’s strong bisimulation:

Theorem 2 Two transition systems (and so synchronisation trees), over the same labelling set L, are Bran_{L}-bisimilar iff they are strongly bisimilar in the sense of [7].

Proof: “only if” If transition systems are connected by a Bran_{L}-open morphism then because its function on states satisfies the “zig-zag” condition (Proposition 1) its graph is a strong bisimulation. Strong bisimilarity is an equivalence relation. Hence a span of Bran_{L}-open morphisms between two transition systems makes them strong bisimilar. “if”: Suppose R is a strong bisimulation relating T_{1} and T_{2}, i.e. R ⊆ S_{1} × S_{2}, a relation between their states, containing the pair (i_{1}, i_{2}) of initial states, such that whenever (s_{1}, s_{2}) ∈ R

(i) if s_{1} →^{a} s′_{1} then s_{2} →^{a} s′_{2} & (s′_{1}, s′_{2}) ∈ R, for some s′_{2} ∈ S_{2}, and

(ii) if s_{2} →^{a} s′_{2} then s_{1} →^{a} s′_{1} & (s′_{1}, s′_{2}) ∈ R, for some S′_{1} ∈ S_{1}.

Construct a transition system in T_{L} from R as follows

• Its set of states is R itself with initial state (i_{1}, i_{2}).

• Its transition are triples ((s_{1}, s_{2}), a, (s′_{1}, s′_{2})), where (s_{1}, s_{2}), (s′_{1}, s′_{2}) ∈ R, for

which

(s_{1}, a, s′_{1}) is a transition of T_{1} and
(s_{2}, a, s′_{2}) is a transition of T_{2}.

There are clearly morphisms f_{1} : R → T_{1}, f_{2} : R → T_{2} in T_{L} got by projecting to the left and right components of states. Because R is a strong bisimulation, f_{1} and f_{2} satisfy the “zig-zag” condition of Proposition 1 and therefore form a span of Bran_{L}-open morphisms. □

Clearly, in general, the relation of P-bisimilarity between objects is reflexive (identities are P-open) and symmetric (in the nature of spans). It is also transitive provided M has pullbacks, and so an equivalence relation on objects, by virtue of the following fact:

Proposition 3 Pullbacks of P-open morphisms are P-open.

Proof: Assume in the pullback diagram

[figure: \begin{matrix}X_{′} & X \\ Y_{′} & Y \end{matrix}; g′; f′; f; g]

that f is open. Suppose m : P → Q is a morphism in P so that the following diagram commutes:

[figure: \begin{matrix}P & X_{′} \\ Q & Y_{′} \end{matrix}; p; m; f′; q]

Combining the two commuting squares, as f is open, there is r : Q → X such that

r ∘ m = g′ ∘ p and  (1)
f ∘ r = g ∘ q  (2)

i.e. the two “triangles” commute in

[figure: \begin{matrix}P & X_{′} & X \\ Q & Y_{′} & Y \end{matrix}; p; m; g′; f; r; q; g]

Now, from the property of the pullback square there is s : Q → X′ such that

g′ ∘ s = r and  (3)
f′ ∘ s = q.  (4)

Thus in the diagram

[figure: \begin{matrix}P & X_{′} & X \\ Q & Y_{′} & Y \end{matrix}; p; m; g′; f′; f; s; q; g]

the lower “triangle” commutes by (4). To show, in addition, that the upper “triangle” commutes, i.e. p = s ∘ m (as required for f′ to be open), we note that from the pullback that p is the unique morphism to satisfy

\begin{aligned}g′ ∘ p & = g′ ∘ p, and \\ f′ ∘ p & = q ∘ m. \end{aligned}

However

g′ ∘ (s ∘ m) = (g′ ∘ s) ∘ m = r ∘ m = g′ ∘ p

by (3) and (1), and

f′ ∘ (s ∘ m) = (f′ ∘ s) ∘ m = q ∘ m

by (4). Thus p = s ∘ m. Hence f′ satisfies the path-lifting property required for it to be open. □

Transitivity of P-bisimilarity is clear for M with pullbacks; two spans of open morphisms combine to form a span by pulling back from their vertices, as we can do for all the models we consider:

Proposition 4 Fibres in the categories T, S, TI, E have pullbacks.

Proof: There are coreflections from all categories S_{L}, T_{L}, E_{L} into TI_{L}. Using the fact that right adjoints preserve limits, and pullbacks in particular, we obtain pullbacks in any of S_{L}, T_{L}, E_{L} as images under the right adjoints of the pullback in TI_{L} of diagrams transported into TI_{L} by the left adjoints. Of course, this depends on TI_{L} itself having pullbacks. But these we can construct explicitly in the following way. Suppose f_{1} = (σ_{1}, 1_{L}) : T_{1} → U and f_{2} = (σ_{2}, 1_{L}) : T_{2} → U are morphisms in TI_{L} where

T_{1} = (S_{1}, i_{1}, L, tran_{1}, I_{1}) and T_{2} = (S_{2}, i_{2}, L, tran_{2}, I_{2}).

Define

T = (S, i, L, tran, I)

where

S = {(s_{1}, s_{2}) | σ_{1}(s_{1}) = σ_{2}(s_{2})}, with i = (i_{1}, i_{2}),
((s_{1}, s_{2}), a, (s′_{1}, s′_{2})) ∈ tran iff (s_{1}, a, s′_{1}) ∈ tran_{1} and (s_{2}, a, s′_{2}) ∈ tran_{2},

and

\begin{matrix}((s_{1}, s_{2}), a, (s′_{1}, s′_{2})I((u_{1}, u_{2}), b, (u′_{1}, u′_{2})) \\ iff (s_{1}, a, s′_{1})I_{1}(u_{1}, b, u′_{1}) & & (s_{2}, a, s′_{2})I_{2}(u_{2}, b, u′_{2}). \end{matrix}

There is an inclusion morphism from T, defined above, to the (fibre) product T_{1}×_{L} T_{2} in TI_{L}. Consequently T satisfies Axioms (1) and (3) required of a transition system with independence—they are inherited from the product. Axiom (2) remains to be checked; but it follows simply from the associated properties in the components. The projections π_{1} : T → T_{1}, π_{2} : T → T_{2} determine a pullback, essentially because it is based on pullback in the category of sets:

[figure: \begin{matrix}T & T_{2} \\ T_{1} & U \end{matrix}; π_{2}; π_{1}; f_{2}; f_{1}]

□

We conclude this section with some useful general facts about how open morphisms are preserved and reflected by functors, especially as part of a coreflection.

For notational simplicity we shall assume the left adjoints of the coreflections are inclusions. It follows that for the coreflections of Section 1.5, open morphisms, with respect to a choice of path category, are preserved in both directions of the adjunction.

Proposition 5 Let M be a full subcategory of N, and P a subcategory of M. A morphism f of M is P-open in M iff f is P-open in N.

Proof: Directly from the definition of open morphism. □

Lemma 6 Let M be a coreflective subcategory of N with R right adjoint to the inclusion function M ↪ N and P a subcategory of M. Then:

(i) A morphism f of M is P-open in M iff f is P-open in N.

(ii) The components of the counit of the adjunction ε_{X} : R(X) → X are P-open in M.

(iii) A morphism f is P-open in N iff R(f) is P-open in M.

Proof:

(i) By Proposition 5, this is a direct consequence of the functor M ↪ N being full and faithful, itself a consequence of the coreflection. (ii) Let ε : R(X) → X be a component of the counit of the adjunction. Suppose the following diagram commutes

[figure: \begin{matrix}P & R(X) \\ Q & X \end{matrix}; p; m; ε; q]

where m is a morphism in P, i.e. that q ∘ m = ε ∘ p. By the cofreeness of R(X), ε over X, there is a (unique) morphism r : Q → R(X) such that in

[figure: \begin{matrix}P & R(X) \\ Q & X \end{matrix}; p; m; ε; r; q]

the lower “triangle” commutes, i.e. ε ∘ r = q. In addition,

ε ∘ (r ∘ m) = (ε ∘ r) ∘ m = q ∘ m = ε ∘ p

whence by cofreeness (this time uniqueness) we can conclude r ∘ m = p, i.e. that the upper tringle also commutes. It follows that ε is open.

(iii) Suppose f : X → Y is a morphism in N. From the adjunction we have the commuting diagram:

[figure: \begin{matrix}R(X) & X \\ R(Y) & Y \end{matrix}; ε_{X}; R(f); f; ε_{Y}]

“only if”: Assume f is P-open. Let m be a morphism in P for which

[figure: \begin{matrix}P & R(X) \\ Q & R(y) \end{matrix}; p; m; R(f); q]

commutes. Combining the two commuting squares we obtain a commuting diagram:

[figure: \begin{matrix}P & R(X) & X \\ Q & R(Y) & Y \end{matrix}; p; m; ε_{X}; f; q; ε_{Y}]

where the composition f ∘ ε_{X}, of open morphisms, is open. Hence there is a morphism r : Q → R(X) such that the two halves of the following diagram commute:

[figure: \begin{matrix}P & R(X) & X \\ Q & R(Y) & Y \end{matrix}; p; m; ε_{X}; f; r; q; ε_{Y}]

In particular,

f ∘ ε_{X} ∘ r = ε_{Y} ∘ q

Now, argue that

ε_{Y} ∘ (R(f) ∘ r) = (ε_{Y} ∘ R(f)) ∘ r = f ∘ ε_{X} ∘ r = ε_{Y} ∘ q.

But R(Y), ε_{Y} is cofree over Y, ensuring that

R(f) ∘ r = q.

Hence the two “triangles” commute in:

[figure: \begin{matrix}P & R(X) \\ Q & R(Y) \end{matrix}; p; m; R(f); r; q]

It follows that R(f) is P-open in M. “if”: Assume R(f) is P-open. Given a commuting square

[figure: \begin{matrix}P & X \\ Q & Y \end{matrix}; p; m; f; q]

with m in P, the morphisms p and q factor through ε_{X} and ε_{Y}

[figure: \begin{aligned}P \\ & R(X) & X \\ & R(Y) & Y \\ Q \end{aligned}; p′; p; m; ε_{X}; R(f); f; ε_{Y}; q′; q]

i.e. p = ε_{X} ∘ p′ and q = ε_{Y} ∘ q′. By cofreeness of R(Y), ε_{Y} over Y, we obtain that

R(f) ∘ p′ = q′ ∘ m.

Because R(f) is open there is r : Q → R(X) so that

r ∘ m = p′ & R(f) ∘ r = q′.

Hence taking r′ = ε_{X} ∘ r the two “triangles” commute in:

[figure: \begin{matrix}P & X \\ Q & Y \end{matrix}; p; m; f; r′; q]

Thus f is open. □

3 Characterisations

We have already seen (Lemma 1, Theorem 2) that for the well-known model of transition systems, the general definition of P-open morphism and P-bisimilarity coincide with familiar notions; in particular, we recover the equivalence of strong bisimilarity central to Milner’s work. Here we explore how the general definitions specialise to the models of event structures and transition systems with independence.

We start by characterising Pom_{L}-open morphisms on transition systems with independence. As usual, we shall identify pomsets with their image under the embedding E → TI.

Proposition 7 The Pom_{L}-open morphisms of TI_{L} are precisely those which satisfy the “zig-zag” condition of Proposition 1 and which, in addition, reflect consecutive independence (a morphism (σ, 1_{L}) : T_{1} → T_{2} between transition systems with independence T_{1} = (S_{1}, i_{1}, L, tran_{1}, I_{1}) and T_{2} = (S_{2}, i_{2}, L, tran_{2}, I_{2}) reflects consecutive independence iff

whenever (s, a, s′), (s′, b, s′′) ∈ tran_{1}, with s reachable, and
(σ(s), a, σ(s′))I_{2}(σ(s′), b, σ(s′′)) in T_{2},
then (s, a, s′)I_{1}(s′, b, s′′) in T_{1}.)

Proof: Let f = (σ, 1_{L}) : T → T′ be an open morphism in TI_{L}. By considering linear pomsets, where causal dependency is a total order, it is clear as in Proposition 1, that f satisfies the “zig-zag” condition. Suppose

s →^{a} u and u →^{b} v,

with s reachable, are two consecutive transitions in T for which

σ(s) →^{a} σ(u) and σ(u) →^{b} σ(v)

are independent in T′. Because s is reachable there is a chain of transitions

i = s_{0} →^{a_{1}} s_{1} →^{a_{2}} ⋯ →^{a_{n}} s_{n} = s

in T from its initial state i. Let P be the linear pomset (regarded as a transition system with independence):

[figure: •  •  •  ⋯  •  •  •  •; a_{1}; a_{2}; a_{n}; a; b]

Let p : P → T be that morphism in TI_{L} which maps this chain of transitions to

[figure: s_{0}  s_{1}  ⋯  s  u  v.; a_{1}; a_{2}; a_{n}; a; b]

in T. Let Q be the pomset (regarded as a transition system with independence):

[figure: \begin{aligned}& & & & & & • \\ • & • & • & ⋯ & • & • & I & • \\ & & & & & & • \end{aligned}; b; a_{1}; a_{2}; a_{n}; a; b; a]

Let q : Q → T′ be that morphism in TI_{L} mapping these transitions to

[figure: \begin{aligned}& & & & σ(u) \\ σ(s_{0}) & σ(s_{1}) & ⋯ & σ(s) & I & σ(v) \\ & & & & • \end{aligned}; b; a_{1}; a_{2}; a_{n}; a; b; a]

in T′. Letting m : P → Q be the obvious morphism of pomsets, we observe the commuting diagram:

[figure: \begin{matrix}P & T \\ Q & T_{′} \end{matrix}; p; m; f; q]

But f is open, so we obtain a morphism p′ : Q → T such that the two “triangles” commute in:

[figure: \begin{matrix}P & T \\ Q & T_{′} \end{matrix}; p; m; f; q; p′]

Because p′ preserves independence, we see that s →^{a} u and u →^{b} v are independent in T. So because f is open it satisfies the “zig-zag” condition and reflects consecutive independence. It is sufficient to show the converse for a morphism between the transition systems with independence of event structures: The adjunction from E to TI yields the commuting diagram

[figure: \begin{matrix}E & T \\ E_{′} & T_{′} \end{matrix}; ε; g; f; ε′]

in TI_{L}, where E = eti ∘ tie(T), E′ = eti ∘ tie(T′), g = eti ∘ tie(f) and ε, ε′ are components of the counit of the adjunction. Considering the functor eti∘tie—see Section 1.5—it can be seen that g satisfies the “zig-zag” condition and reflects consecutive independence if f does. Moreover, by Lemma 6(iii), it is clear that if g is an open map then so is f. Thus it is sufficient to assume that g : E → E′ is a morphism between the transition systems with independence of event structures in TI_{L} which satisfies the “zig-zag” condition and reflects consecutive independence, and then show it follows that g is open. To this end let

[figure: \begin{matrix}P & E \\ Q & E_{′} \end{matrix}; p; m; g; q]

be a commuting diagram in TI_{L}, with P, Q (transition systems with independence) of pomsets in P_{L}. Forgetting the independence structure, we obtain a commuting diagram in T_{L}:

[figure: \begin{matrix}tit(P) & tit(E) \\ tit(Q) & tit(E′) \end{matrix}; p; m; g; q]

Because g satisfies the “zig-zag” condition, there is a morphism r of transition systems T_{L} so that

[figure: \begin{matrix}tit(P) & tit(E) \\ tit(Q) & tit(E′) \end{matrix}; p; m; g; r; q]

where the two “triangles” commute. We show that r is, in fact, also a morphism r : Q → E in TI_{L}. This will make essential use of E and E′ being transition systems with independence of event structures. For r : Q → E to be a morphism in TI_{L} it is sufficient to show that r preserves independence on transitions. From the commuting diagram

[figure: \begin{aligned}& tit(E) \\ tit(Q) & tit(E′) \end{aligned}; g; r; q]

we can first deduce that r preserves consecutive independence: Two consecutive independent transitions t, t′ of Q have as image under r two consecutive transitions of E; the two consecutive transitions of E go under g to the two consecutive independent transitions got as the image under q of t, t′—recall q is a morphism in TI_{L}, which must therefore preserve independence; now, because g reflects consecutive independence the two consecutive transitions of E must be independent. This shows r preserves consecutive independence. A similar argument, shows that r preserves independence squares. We can represent the images under q, r and g of an original independence square in Q by:

\begin{aligned}& [figure] C \\ A [figure] & [figure] B \end{aligned}_{g} [figure]_{r} [figure]_{q} [figure]

Because q is a is morphism in TI_{L} it sends the independence square A in Q to an independence square B in E′. By the commutativity q = g ∘ r, the independence square A is sent by r to a square of transitions C in E, where we have the consecutive independence indicated in C because r preserves consecutive independence. Because E is got from an event structure, the consecutive independence in C must be due to two concurrent events, which forces C to be an independence square. Because Q is a got from a pomset, it inherits the property of event structures that two transitions are independent if they are ∼-related to independent transitions in an independence square. As the relation ∼ itself is obtained from independence squares, and r preserves such squares, this entails that r preserves independent transitions in general. Hence r is a morphism in TI_{L} and we have the required path lifting property in TI_{L}; the two “triangles” commute in:

[figure: \begin{matrix}P & E \\ Q & E_{′} \end{matrix}; p; m; g; r; q]

The morphism g is thus open. □

In the case of event structures taking the path category P to be pomsets yields a reasonable strengthening of a previously studied equivalence, that of historypreserving bisimulation. Its definition depends on the simple but important remark, that a configuration of an event structure can be regarded as a pomset, with causal dependency relation and labelling got by restricting that of the event structure. In more detail, assume

E = (E, ≤, Con, ℓ)

is an event structure. If x is a configuration of E it determines a pomset, viz

(x, ≤ ∩(x × x), F in(x), ℓ ↾ x : x → L),

which we will also call x; here F in(x) consists of all finite subsets of x which coincides with the restriction of Con to subsets of x because configurations are consistent.

Definition: (Rabinovitch-Traktenbrot [10], van Glabeek-Goltz [3]) A history-preserving bisimulation between two event structures E_{1}, E_{2} consists of a set H of triples (x_{1}, f, x_{2}) where x_{1} is a configuration of E_{1}, x_{2} a configuration of E_{2} and f is a isomorphism between them (regarded as pomsets), such that (∅, ∅, ∅) ∈ H and, whenever (x_{1}, f, x_{2}) ∈ H

(i) if x_{1} →^{a} x′_{1} in E_{1} then x_{2} →^{a} x′_{2} in E_{2} and (x′_{1}, f′, x′_{2}) ∈ H with f ⊆ f′, for

some x′_{2} and f′.

(ii) if x_{2} →^{a} x′_{2} in E_{2} then x_{1} →^{a} x′_{1} in E_{1} and (x′_{1}, f′, x′_{2}) ∈ H with f ⊆ f′, for

some x′_{1} and f′

We say a history-preserving bisimulation H is strong when it further satisfies

(I) (x, f, y) ∈ H & x′ ⊆ x, for a configuration x′ of E_{1} implies (x′, f′, y′) ∈ H, for some f′ ⊆ f and y′ ⊆ y.

(II) (x, f, y) ∈ H & y′ ⊆ y, for a configuration y′ of E_{2}, implies (x′, f′, y′) ∈ H, for some f′ ⊆ f and x′ ⊆ x.

Example: We give an example of two event structures which are history-preserving bisimilar but not strong history-preserving bisimilar. They are presented below as transition systems with independence (cf. Section 1.4). Each of the two event structures has six events, and we have indicated below a few configurations. The reader can fill in the rest, and provide a history-preserving bisimulation H between the two structures. It is clear that H cannot be strong since H must relate the configurations {e_{1}} and {e′_{1}} (because of the b-labelled events), and hence must relate configurations {e_{1}, e_{2}} and {e′_{1}, e′_{2}}. But {e_{2}} cannot be related to {e′_{2}} (because of the c-labelled event, {e_{2}} can only be related to {e′_{3}}).

[figure: \begin{matrix}· & · & · \\ · & ⊙ & ·\{e_{1}\} \\ · & · \{e_{2}\} & ·\{e_{1}, e_{2}\} \end{matrix}; a; a; a; a; a; a; b; a; c; a; \begin{matrix}· & · & · \\ \{e′_{3}\}· & ⊙ & ·\{e′_{1}\} \\ · & · \{e′_{2}\} & ·\{e′_{1}, e′_{2}\} \end{matrix}; a; a; c; a; a; a; a; b; a; a]

Proposition 8 Let f : E → E′ be an open morphism in E_{L}, for event structures E and E′. If x is a configuration of E then the restriction f : x → fx is an isomorphism of pomsets in Pom_{L}, where configurations x and fx are regarded as pomsets (with pomset structure induced by E and E′ respectively).

Proof: Assume f : E → E′ is an open morphism in E_{L} between event structures E, E′. Let x be a configuration of E. Regarding x as a pomset, there is a morphism in E_{L} induced by inclusion

x ↪ E.

A property of morphisms of event structures is that the set image fx is a configuration of E′ and that f is 1-1 when restricted to x. (See the definition in Section 1.4). Again, identifying the configuration fx of E′ with the pomset got by restricting E′, we obtain the commuting square

[figure: \begin{matrix}x & E \\ fx & E_{′} \end{matrix}; f_{x}; i; f; i′]

where f_{x} is the morphism of pomsets got as the restriction of f to x, and i, i′ are the inclusion morphisms associated with the configurations. Now, using the fact that f is open there is a morphism fx → E so that in

[figure: \begin{matrix}x & E \\ fx & E_{′} \end{matrix}; f_{x}; i; f; i′]

both “triangles” commute. Because f is a morphism in E_{L}, we already know that f_{x} is 1-1 and onto between the sets x and fx. Commutativity of the upper “triangle” forces f_{x} to be an isomorphism of pomsets. □

Theorem 9

(i) Two event structures, with labelling sets L, are Pom_{L}-bisimilar iff they are strong history-preserving bisimilar.

(ii) Two transition systems with independence, with label sets L, are Pom_{L}- bisimilar iff their unfoldings to event structures are strong history-preserving bisimilar.

Proof:

(i) The relation of being strong history-preserving bisimilar is an equivalence relation; for example, to show transitivity if E_{1}, E_{2} are strong history-preserving bisimilar via H_{1} and E_{2}, E_{3} are strong history-preserving bisimilar via H_{2}, than E_{1}, E_{3} are strong history-preserving bisimilar via H where

H = {(x, θ ∘ φ, z) | ∃y. (x, φ, y) ∈ H_{1} & (y, θ, z) ∈ H_{2}}

It is thus sufficient to show that an open morphism between event structures establishes a strong history-preserving bisimulation between them. Assume f : E → E′ is an open morphism in E_{L} between event structures E and E′. In the light of Proposition 8, we tentatively take as the strong historypreserving-bisimulation the relation H consisting of all triples

(x, f_{x}, fx)

for x a configuration of E. The relation H clearly contains (∅, ∅, ∅). The conditions (I) and (II) required of a strong history-preserving bisimilation are fulfilled automatically with this definition. We further require conditions (i) and (ii) in the definition of history-preserving bisimulation. Condition (i) follows directly from f being a morphism. In showing condition (ii), suppose (x, f_{x}, fx) ∈ H and that fx →^{a} y in E′, for a configuration y of E′. Identifying the configurations fx and y with the pomset structures induced on them by E′, the inclusion fx ⊆ y gives a morphism of pomsets

fx ↪ y.

Letting m be the composition

x →^{f_{x}} fx ↪ y

we have the commuting square

[figure: \begin{matrix}x & E \\ y & E_{′} \end{matrix}; m; i; f; j]

where i, j are the morphisms of event structures associated with the obvious inclusions. As f is open, there is a morphism of event structures r : y → E such that both “triangles” commute in:

[figure: \begin{matrix}x & E \\ y & E_{′} \end{matrix}; m; i; f; r; j]

Take x′ to be the configuration of E which is the image of y under r. As fx′ = y, by Proposition 8, we obtain the isomorphism of pomsets

f_{x′} : x′ ≅ y

extending f_{x}. This shows the remainder (ii), required for H to be a strong history-preserving bisimulation. Hence f : E → E′ being open in E_{L} implies E, E′ are strong history-preserving bisimilar. “if:” Suppose E_{1} = (E_{1}, ≤_{1}, Con_{1}, ℓ_{l}), E_{2} = (E_{2}, ≤_{2}, Con_{2}, ℓ_{2}) are event structures related by a strong history-preserving bisimulation H. We first observe that H can itself be regarded as a transition system with independence, T = (S, i, L, tran, I). (In fact, it is one arising, to within isomorphism, from an event structure). As states take

S = {θ | ∃x_{1}, x_{2}. (x_{1}, θ, x_{2}) ∈ H}

with initial state i = ∅. We take as transitions:

(θ, a, θ′) ∈ tran iff ∃e_{1}, e_{2}. θ′ = θ∪^{·}{e_{1}, e_{2}} & ℓ_{1}(e_{1}) = ℓ_{2}(e_{2}) = a

(Here we are regarding the isomorphism θ as the graph of its function, and by ∪^{·} indicate the union is disjoint.) It is clear that a transition (θ, a, θ′) determines a unique pair of events e_{1} ∈ E_{1}, e_{2} ∈ E_{2}, with the same label, for which θ′ = θ∪^{·}{(e_{1}, e_{2})}; we write ev(θ, a, θ′) for (e_{1}, e_{2}). We take two transitions (θ, a, θ′) and (φ, b, φ′) to be independent, setting

(θ, a, θ′) I (φ, b, φ′),

iff their associated pairs of events (e_{1}, e_{2}) = ev(θ, a, θ′) and (e′_{1}, e′_{2}) = ev(φ, b, φ′) are such that

e_{1} co e′_{1} in E_{1}, and e_{2} co e′_{2} in E_{2}.

By considering a typical independence square it is easily seen that

(θ, a, θ′) ∼ (φ, b, φ′) ⇒ a = b & ev (θ, a, θ′) = ev(φ, b, φ′).

It follows that T satisfies axioms (1) and (3) required of a transition system with independence. Axiom (2) also holds, its proof relying on the history-preserving bisimulation being strong: Assume (θ, a, θ_{1}) I (θ_{1}, b, φ), for transitions of T. Let (e_{1}, e_{2}) = ev(θ, a, θ_{1}) and (e′_{1}, e′_{2}) = ev(θ_{1}, b, φ). Let x be the domain of θ and u the domain of φ. We observe that u is a configuration of E_{1} with subconfiguration y_{1} = x∪^{·}{e′_{1}}—it has this subconfiguration because e_{1}co e′_{1} from the assumption that the transitions are independent. H being strong yields an isomorphism of pomsets θ_{2} ⊆ φ with (y_{1}, θ_{2}, y_{2}) ∈ H, where y_{2} is the range of θ_{2}. It follows that θ_{2} = θ∪^{·}{(e′_{1}, e′_{2})} and φ = θ_{2}∪^{·}{(e_{1}, e_{2})} yielding two transitions for which (θ, b, θ_{2}) I (θ_{2}, a, φ), as required by Axiom (2). Let π_{1} and π_{2} be the projections which for θ ∈ S give its domain and range respectively. It is easily checked that (π_{1}, 1_{L}) : T → eti(E_{1}) and (π_{2}, 1_{L}) : T → eti(E_{2}) are open morphisms in TI_{L}, (for openness use Proposition 7), making the transition systems with independence of E_{1} and E_{2} Pom_{L}-bisimilar in TI_{L}. The image of this span under tie consists of two open morphisms in E_{L}, by Lemma 6. Composed with inverses to isomorphisms of the unit

\begin{matrix}η_{1} : E_{1} → tie ∘ eti(E_{1}), \\ η_{2} : E_{2} → tie ∘ eti(E_{2}) \end{matrix}

they yield the following span of open morphisms in E_{L}:

[figure: \begin{aligned}& & tie(T) \\ E_{1} & tie ∘ eti(E_{1}) & & tie ∘ eti(E_{2}) & E_{2} \end{aligned}; tie(π_{1},1_{L}); tie(π_{2},1_{L}); η_{1}^{−1}; η_{2}^{−1}]

Hence E_{1}, E_{2} are Pom_{L}-bisimilar in E_{L}. (ii) To conclude the proof, we show that two transition systems with independence T_{1}, T_{2} are Pom_{L}-bisimilar iff their event-structure unfoldings are strong historypreserving bisimilar. “only if”: Assuming T_{1}, T_{2} are Pom_{L}-bisimilar, there is a span of open morphisms in TI_{L} whose image under tie is a span of open morphisms in E_{L} (by Lemma 6. This ensures the unfoldings tie(T_{1}), tie(T_{2}) are strong history-preserving bisimilar by part (i). “if”: By the proof of part (i), assuming the unfoldings of T_{1} and T_{2} are strong history-preserving bisimilar we obtain a span of open morphisms in TI_{L}:

[figure: \begin{aligned}& T \\ eti ∘ tie(T_{1}) & & eti ∘ tie(T_{2}) \end{aligned}; f_{1}; f_{2}]

Composing with components of the counit

\begin{matrix}ε_{1} : eti ∘ tie(T_{1}) → T_{1}, \\ ε_{2} : eti ∘ tie(T_{2}) → T_{2}, \end{matrix}

which are open by Lemma 6, we obtain a span of open morphisms relating T_{1}, T_{2}. □

From the proof of Proposition 7 we can see that the relation of strong historypreserving bisimulation is quite robust. It might be thought that strong historypreserving bisimulation, presented as Pom_{L}-bisimilarity, is affected by restricting the category Pom_{L} to a smaller class of objects. However, no matter how much the objects in the path category Pom_{L} are restricted, provided they include all pomsets of the “stick” and “lollipop” forms in the proof of Proposition 7, then the relation of bisimulation that results will coincide with strong historypreserving bisimulation: By the “only if” part of the proof, an open morphism with respect to such a smaller class of pomsets will be “zig-zag” and reflect consecutive independence; hence the notion of open map, and so bisimulation, is unaffected by restricting to a smaller class of pomsets.^{2}

Example: An observation central to [2, 1] is that two synchronisation trees or transition systems are strong bisimilar iff they are related by a cospan of “zigzag” morphisms (defined in Proposition 1). Their development, which is only for transition systems, is in a sense dual to that here, and does not generalise to the other models. (Another difference is that they begin with the notion of “zigzag” morphism, so don’t have universal characterisations of the constructions of process calculi.) As an example, consider the following two transition systems with independence, where all squares but the lower squares (labelled a, b, c, d) are independence squares:

2We are grateful to Allan Cheng for this remark.

[figure: \begin{aligned}& · & & & · & & · \\ · & · & · & · & & · & & · \\ · & & · & & · & & · \\ & · & & & & · \end{aligned}; c; e; e; d; c; e; e; d; e; c; d; e; e; c; d; e; a; b; a; b]

T_{0} T_{1}

It follows that the unfolding of T SI_{0} and T SI_{1} into event structures are isomorphic, and hence from Theorem 9, that T_{0} and T_{1} are Pom_{L}-bisimilar. On the other hand, there can be no cospan of P om_{L}-open maps T_{0} →^{f_{0}} T ←^{f_{1}} T_{1} (left for the reader to verify). Hence, it follows that “being related by a cospan of Pom_{L}- open maps” is a different relation over transition systems with independence–as a matter of fact a non-transitive relation.

4 Presheaf models

The notion of open map applies to morphisms of a topos [4]. Consider a category of models M and a choice of path category forming a subcategory P ↪ M. In order to compare the notions we consider the canonical functor from the category of models M to the topos of presheaves [P^{op}, Set]. The functor

M → [P^{op}, Set]

takes an object X of M to the presheaf M(−, X), and a morphism f : X → Y in M to the natural transformation

M(−, f) : M(−, X) → M(−, Y)

whose component at an object P of P is the function M(P, X) → M(P, Y) taking g to f ∘ g. In general, the canonical functor will not be full and faithful, i.e. a full embedding of M into [P^{op}, Set]. However, it is a full embedding iff the inclusion P ↪ M is dense, i.e. every object of M is the colimit of objects in P (see [5] P.243). This is the case for two major examples:

Theorem 10

(i) With respect to a labelling set L, the inclusion Bran_{L} ↪ S_{L} of branches into the category of synchronisation trees is dense. The canonical functor from S_{L} to [Bran_{L}^{op}, Set] is a full embedding.

(ii) With respect to a labelling set L, the inclusion Pom_{L} ↪ E_{L} of pomsets into the category event structures is dense. The canonical functor from E_{L} to [Pom_{L}^{op}, Set] is a full embedding.

Proof: As remarked, the canonical functors to presheaves are full and faithful iff the inclusions of the subcategories of path category are dense. Here we only show Pom_{L} ↪ E_{L} is dense—that Bran_{L} ↪ S_{L} is dense follows by a similar, but easier, argument. For the subcategory Pom_{L} to be dense in E_{L}, we require that every event structure E in E_{L} is the colimit of pomsets. More precisely, we require that the cocone, given by the following constructions, is colimiting: Let D be the category consisting of objects p : P → E in E_{L} where P is a pomset in Pom_{L} and morphisms from (p : P → E) to (q : Q → E) are morphisms m : P → Q such that

[figure: \begin{matrix}P & E \\ Q \end{matrix}; p; m; q]

commutes in E_{L}. The functor d : D → Pom_{L} typically takes such a morphism to m : P → Q. There is a cocone over d with vertex E and components p, for p : P → E in D. We require that this cocone E, p is colimiting. Suppose there is another cocone over d with vertex an event structure E′ and components p′. Objects of D include inclusion morphisms

x ↪ E

where x is a configuration of E, regarded as a pomset (as earlier in Section 3, x inherits the causal dependency and labelling of E). Write p_{x}, p′_{x} for the components of the cocones at x ↪ E in D. In particular, there are inclusion morphisms

⌈e⌉ ↪^{i} E

where e is an event of E and ⌈e⌉ =_{def} {e_{1} | e_{1} ≤ e}. Define η(e) to be the event in E′ which is the image of e under p′_{⌈e⌉}. Because the components p′ preserve labels so does η. Because E′, p′ is a cocone over D, the diagram

[figure: \begin{matrix}x & E_{′} \\ ⌈e⌉ \end{matrix}; p′_{x}; p′_{⌈e⌉}]

commutes for e ∈ x, a configuration of E. This ensures that ηx is a configuration of E′ and moreover that η is 1-1 when restricted to x. Thus η is a morphism E → E′. Because any component p : P → E of the cocone E, p factors as

[figure: \begin{aligned}P & & E \\ & x \end{aligned}; p]

where x is the configuration-image of P, it follows that η is a mediating morphism of cocones from E, p to E′, p′. The morphism η is unique such that

[figure: \begin{aligned}⌈e⌉ & E \\ & E′ \end{aligned}; p_{⌈e⌉}; p′_{⌈e⌉}; η]

commutes, a property required of the mediating morphism. We conclude that the cocone E, p is colimiting, and hence that Pom_{L} ↪ E_{L} is dense. □

There are more objects in the presheaf categories than in the original models. In the case where path objects are branches, objects of the presheaf category [Bran_{L}^{op}, Set] consist of “synchronisation forests”, viz. collections of synchronisation trees. Such a collection may be empty. The embedding has as image all those collections which are singletons. The collections carry a computational intuition similar to that of synchronisation trees—there is no longer simply one initial state. The embeddings, being full, faithful and dense, preserve limits, so products in the larger category of presheaves coincide with the fibre product on synchronisation trees, though coproducts will differ, amounting to disjoint union of forests in [Bran_{L}^{op}, Set]. The extra objects in [Pom_{L}^{op}, Set], over those presheaves corresponding to event structures, are more difficult to explain, though some are representable via models such as general Petri nets. For several categories of labelled Petri nets N_{L}, there is an embedding functor N : E_{L}^{#} → N_{L} from a full subcategory of event structures, where consistency is determined by a binary conflict, which restricts to a functor from pomsets Pom_{L}. We obtain a functor

N_{L} → [Pom_{L}^{op}, Set] with N ↦ N_{L}(N (−), N).

When N possesses a right adjoint U, unfolding a net to an event structure (as is so for the nets considered in [13, 14]), the presheaf N_{L}(N (−), N), obtained from a net N, is naturally isomorphic to E_{L}(−, U(N))—the presheaf which corresponds to the event-structure unfolding of N. But the functor N_{L} → [Pom_{L}^{op}, Set] also makes sense for general Petri nets, providing an unfolding of them into presheaves, even when N is not a left adjoint. For example, consider the particular presheaf which assigns a singleton set to each finite pomset over a single label a, and ∅ elsewhere; this does not correspond to any event structure but can be represented by a Petri net consisting of a single event, with no pre or post conditions, labelled by a—this Petri-net event can occur with arbitrary multiplicity. The presence of such extra objects in presheaves makes an important contribution. It allows the definition of operations which would not otherwise be defined on the smaller category of event structures, a point we shall return to. The embeddings of Theorem 10 extend the Yoneda embedding of P → [P^{op}, Set], regarding a path object P as the presheaf P(−, P) = M(−, P) because, in these cases, the subcategory P ↪ M is full. Now, if we regard presheaves as the model M′ and the image of P under the Yoneda embedding as its path category P′, we can apply the general definition of Section 2, to obtain the class of P′-open morphisms of the presheaf category. They form a category of open maps of the topos [P^{op}, Set], in the sense of Joyal and Moerdijk.^{3} The two notions of P-open and open map agree for the models of synchronisation trees and event structures, because generally:

Proposition 11 Let P be a dense, full subcategory of M. A morphism f : X → Y of M is P-open iff the morphism M(−, f) : M(−, X) → M(−, Y) is an open map (in the sense of [4]).

Proof: From P being a full subcategory we have that the canonical functor from M to presheaves coincides with the Yoneda embedding on P. Denseness of P in M ensures the canonical functor is full and faithful. Now we can apply Proposition 5 to deduce that the two notions of open morphism agree. □

So, in particular, a morphism f of event structures is Pom_{L}-open iff the corresponding morphism E(−, f) in the presheaf category [Pom_{L}^{op}, Set] is an open map. When it comes to relating notions of bisimilarity, care must taken. It is not the case that two event structures are Pom_{L}-bisimilar iff their associated presheaves are related by a span of open maps in [Pom_{L}^{op}, Set]. This is because there are many more objects in the presheaf category, and, in particular, there is always a span of open maps between any two presheaves subtended from the initial (always empty) presheaf. There are two simple ways to get a correspondence. One is to restrict the objects in the presheaf category. In the situation where the path category P of a model M have an initial object I, a rooted presheaf is a presheaf F in which F (I) is a singleton. As has been remarked, the full subcategory of rooted presheaves of [Bran_{L}^{op}, Set] is equivalent to the category S. Note incidentally, that in the full subcategories of rooted presheaves of [Bran_{L}^{op}, Set] and [Pom_{L}^{op}, Set], the coproduct glues presheaves together at a common initial state; thus there the construction coincides with that required to represent Milner’s sum of processes.

3See [4] P.3, Example 1.1, though there the definition is expressed in terms of the existence of certain quasi-pullbacks—a condition stated in the proof of Lemma 16 below; its equivalence with P′-openness, expressed as a path-lifting property, follows by the Yoneda Lemma.

Proposition 12

(i) Two synchronisation trees, over labelling set L, are Bran_{L}-bisimilar (i.e. strong bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of open maps in the full subcategory of rooted presheaves of [Bran_{L}^{op}, Set].

(ii) Two event structures, over labelling set L, are Pom_{L}-bisimilar (i.e. strong history-preserving bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of open maps in the full subcategory of rooted presheaves of [Pom_{L}^{op}, Set].

Proof: Because the canonical functors are full and faithful, a span of open morphisms in the categories of synchronisation trees or event structures is carried by the canonical functors to a span of open morphisms in rooted presheaves. The proof of the converse directions relies on the definition of path bisimulations and lemmas from the next section. There, Lemma 16 shows that the existence of a span of open morphisms between two objects in the category of rooted presheaves is equivalent to there being a strong path bisimulation between the objects. For the particular models, synchronisation trees and event structures, and their respective choices of path categories P, path bisimulation coincides with P-bisimulation by Theorems 17 and 19. □

Another way to get a correspondence is to define bisimilarity in the entire presheaf category via spans of epimorphic open maps. For the presheaf categories, where sheaves need not be rooted and can consist of several or no components—a situation more general than that previously considered in concurrency, this seems to be the appropriate notion of bisimilarity. Note that Bran_{L}-open morphisms in S and Pom_{L}-open morphisms in E are automatically epimorphic, though this is not so in T and TI because some states can be unreachable.

Proposition 13

(i) Two synchronisation trees, over labelling set L, are Bran_{L}-bisimilar (equivalently, strong bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of epimorphic open maps in [Bran_{L}^{op}, Set].

(ii) Two event structures, over labelling set L, are Pom_{L}-bisimilar (equivalently, strong history-preserving bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of epimorphic open maps in [Pom_{L}^{op}, Set].

Proof: These follow from Proposition 12; in the “if” directions, given a span of open morphisms from a presheaf, taking a single component of it yields a span of open morphisms from a rooted presheaf, whence the earlier proposition applies.

□

Consider now operations relating the presheaf categories [Pom_{L}^{op}, Set], for a labelling set L. Let L and M be labelling sets. Assume a functor θ : Pom_{L} → Pom_{M}. It induces the evident functor

θ^{∗} : [Pom_{M}^{op}, Set] → [Pom_{L}^{op}, Set]

on presheaves which takes a presheaf G : Pom_{M}^{op} → Set to the presheaf G ∘ θ : Pom_{L}^{op} → Set. By standard results on Kan extensions (see [5] corollary 2, P.235), the functor θ^{∗} has both a left and right adjoint:

θ_{!} ⊣ θ^{∗} ⊣ θ_{∗}

The functor θ can be obtained in various ways yielding a variety of useful, and potentially useful, operations. One way to obtain a functor on pomset categories is from a partial function on labels. A partial function

λ : L ⇀ M

between labelling sets induces a functor

λ̂ : Pom_{L} → Pom_{M}

which takes a pomset over L to its image under λ—events are relabelled except where this yields undefined when they are removed. The functor λ̂^{∗} gives the expected restriction operation when λ is an inclusion. The functor λ̂_{!} is the expected relabelling operation when λ is total. The Grothendieck fibration of the functor from sets with partial functions, to categories, taking a partial function

λ : L ⇀ M

to

λ̂^{∗} : [Pom_{M}^{op}, Set] → [Pom_{L}^{op}, Set],

“glues” all the fibres of presheaves together to a model into which the entire category of event structures E embeds. Unlike E, this category has all cartesian (and cocartesian) liftings with respect to the projection to labelling sets. Another way to induce functors on pomset categories is to “refine” labels in L to a finite pomsets over M—if L ⊆ M this might leave some labels unchanged; this operation extends to a functor θ : Pom_{L} → Pom_{M}. The functor θ_{!} is a good candidate for the extension of this refinement to presheaves including those corresponding to event structures. A similar method gives a possibly good notion of refinement of labels by event structures (not just finite pomsets). But both of these proposals need work, and in particular examples, to justify their appropriateness. An exactly analogous development goes through for presheaves over Bran_{L}. What of presheaves as a model of parallel computation? In some ways, from a computer-science viewpoint, they are less concrete and harder to motivate than traditional models like event structures. In another way they give a more direct, positivistic, observation-based representation of processes as coherent collections of possible computation paths.

5 A path logic

Assume the path category P is a small subcategory of a category M of models. Assume P and M have a common initial object I. In the cases where P is Bran_{L} the initial path object is the empty branch consisting of a single initial state, while for Pom_{L} it is the empty pomset. A logic characteristic for P-bisimulation is arrived at via the concept of a path bisimulation.

Definition: A path bisimulation, with respect to P, between objects X_{1}, X_{2} of M is a set R of pairs of paths (p_{1}, p_{2}) with common domain P, so p_{1} : P → X_{1} is a path in X_{1} and p_{2} : P → X_{2} is a path in X_{2}, such that

(1) Initial paths are related: letting p_{1}, p_{2} be the unique paths p_{1} : I → X_{1} and p_{2} : I → X_{2} from the initial object, (p_{1}, p_{2}) ∈ R.

(2) (a) For (p_{1}, p_{2}) ∈ R, if p′_{1} ∘ m = p_{1}, with m in P, in

[figure: \begin{aligned}& P \\ X_{1} & P_{′} & X_{2} \end{aligned}; p_{1}; m; p_{2}; p′_{1}]

then there is p′_{2} such that (p′_{1}, p′_{2}) ∈ R and p′_{2} ∘ m = p_{2} in

[figure: \begin{aligned}& P \\ X_{1} & P_{′} & X_{2} \end{aligned}; p_{1}; m; p_{2}; p′_{1}; p′_{2}]

(b) —the symmetric condition to 2(a).

We say a path bisimulation is strong if further it satisfies (3) If (p_{1}, p_{2}) ∈ R, with p_{1} : P → X_{1} and p_{2} : P → X_{2} and m : P′ → P in P,

then (p_{1} ∘ m, p_{2} ∘ m) ∈ R.

We say two objects X_{1}, X_{2} are (strong) path bisimilar iff there is a (strong) path bisimulation between them.

Define path assertions by:

A ::= \overline{⟨m⟩}A | ⟨m⟩A | ¬A | ⋀_{j ∈ J} A_{j}

where m is a morphism in P, and J is an indexing set, possibly empty and not restricted to being finite. The modality \overline{⟨m⟩} is an “backwards” modality, while ⟨m⟩ is a “forwards” modality, the meaning of which is explained shortly. For the semantics of path assertions, we specify when a path, typically of the form p : P → X, for P an object of P and X an object of M, satisfies an assertion; by structural induction on assertions, define:

• p ⊧ \overline{⟨m⟩}A, for m : P′ → P, iff there is a path p′ : P′ → X for which p′ ⊧ A and p′ = p ∘ m,

• p ⊧ ⟨m⟩A, for m : P → P′, iff there is a path p′ : P′ → X for which p′ ⊧ A and p = p′ ∘ m,

• p ⊧ ¬A iff p |̸= A,

• p ⊧ ⋀_{j ∈ J} A_{j} iff p ⊧ A_{j}, for all j ∈ J.

(This includes the basis of the induction when the indexing set J is empty, and the empty conjunction stands for true).

We call forwards assertions those built without backwards modalities, so with no subassertion of the form \overline{⟨m⟩}A.

Theorem 14 Let X_{1}, X_{2} be objects in M.

(i) X_{1}, X_{2} are path bisimilar iff the two initial paths I → X_{1} and I → X_{2} satisfy the same forwards path assertions.

(ii) X_{1}, X_{2} are strong path bisimilar iff the initial paths I → X_{1} and I → X_{2} satisfy the same path assertions.

Proof: (i) “only if”: Assume R is a path bisimulation between objects X_{1}, X_{2}. A routine structural induction on forwards asssertions A shows that, for any such assertion A, whenever (p_{1}, p_{2}) ∈ R,

p_{1} ⊧ A ⇔ p_{2} ⊧ A.

“if”: For paths p_{1} : P → X_{1}, p_{2} : P → X_{2} define the relation R by

(p_{1}, p_{2}) ∈ R iff (p_{1} ⊧ A ⇔ p_{2} ⊧ A)

for all forwards path assertions A.

By assumption, the initial paths I → X_{1}, I → X_{2} are in R. A proof by contradiction shows R is a path bisimulation: Suppose R were not a path bisimulation. This could only be through 2(a) or 2(b) failing in the definition of path bisimulation. By symmetry it is sufficient to consider one case, 2(a). So assume (p_{1}, p_{2}) ∈ R, where p_{1} : P → X_{1}, p_{2} : P → X_{2}, and p′_{1} ∘ m = p_{1} for p′_{1} : P′ → X_{1} and m : P → P′ in P. Assuming 2(a) fails means that for any q : P′ → X_{2} with p_{2} = q ∘ m we have (p′_{1}, q) ∉ R. From the definition of R, for any such path q with p_{2} = q ∘ m there must be a forwards path assertion B_{q} such that

p′_{1} ⊧ B_{q} and q |̸= B_{q}

—because (p′_{1}, q) ∉ R the paths p′_{1}, q must be distinguished by an assertion holding for one and not the other; using negation, if necessary, we can always find such a B_{q}. Now, take

A ≡ ⟨m⟩( ⋀_{q∈I} B_{q})

where

I = {q : P′ → X_{2} | p_{2} = q ∘ m}.

Then

p_{1} ⊧ A and p_{2} |̸= A,

contradicting (p_{1}, p_{2}) ∈ R. Hence R is a path bisimulation. (ii) The proof for all path assertions proceeds as in (i), but taking care of (3) in the definition of strong path bisimulation and “backwards” modalities. □

We obtain path bisimulations from P-bisimulations:

Lemma 15 If X_{1}, X_{2} are P-bisimilar, then X_{1}, X_{2} are strong path bisimilar with respect to P.

Proof: Assume X_{1}, X_{2} are P-bisimilar. Then there is a span of open maps:

[figure: \begin{aligned}& X \\ X_{1} & & X_{2} \end{aligned}; f_{1}; f_{2}]

Tentatively, define the strong path bisimulation R by

R = {(f_{1} ∘ p, f_{2} ∘ p) | p : P → X with P an object of P}.

It is clear that R satisfies condition (1) and (3) required of a strong path bisimulation. The remaining condition, (2), follows because f_{1}, f_{2} are open. For instance, to show 2 (a), assume (p_{1}, p_{2}) ∈ R, so

p_{1} = f_{1} ∘ p & p_{2} = f_{2} ∘ p & p : P → X

for P an object of P. Suppose for m : P → P′ in P that p′_{1} ∘ m = p_{1} where p′_{1} : P′ → X_{1}. Then because f_{1} is open there is a morphism p′ : P′ → X such that the two “triangles” commute in:

[figure: \begin{aligned}& P \\ P_{′} & X \\ X_{1} & & X_{2} \end{aligned}; m; p; p′_{1}; p′; f_{1}; f_{2}]

Defining p′_{2} = f_{2} ∘ p′ we obtain (p′_{1}, p′_{2}) ∈ R and see

p′_{2} ∘ m = f_{2} ∘ p′ ∘ m = f_{2} ∘ p = p_{2},

as required by 2(a). □

Now, we ask when the existence of a strong path bisimulation with respect to P implies P-bisimilarity. As we will see it does so for all the models we have considered. But first we state a general result. For presheaf models the two notions of path bisimilarity with respect to P and P-bisimilarity coincide. As the following proof shows this is because a path bisimulation corresponds via the Yoneda Lemma, to a span of open morphisms in a presheaf model.

Lemma 16 Let M be the subcategory of rooted presheaves in [P^{op}, Set]. Rooted presheaves X_{1}, X_{2} are strong path bisimilar iff they are P-bisimilar.

Proof: “if”: This follows by Lemma 15. “only if”: Via the isomorphism of the Yoneda Lemma, a strong path bisimulation corresponds to a relation

R ↪ X_{1} × X_{2}

in [P^{op}, Set] such that whenever P →^{m} Q is a morphism of P, if (p_{1}, p_{2}) ∈ R(P) then (1) ∀q_{1} ∈ X_{1}(Q). (X_{1}(m))(q_{1}) = p_{1} ⇒

∃q_{2} ∈ X_{2}(Q). (X_{2}(m))(q_{2}) = p_{2} & (q_{1}, q_{2}) ∈ R(Q), and

(2) ∀q_{2} ∈ X_{2}(Q). (X_{2}(m))(q_{2}) = p_{2} ⇒ ∃q_{1} ∈ X_{1}(Q). (X_{1}(m))(q_{1}) = p_{1} & (q_{1}, q_{2}) ∈ R(Q).

We can express these conditions diagrammatically. For instance (1) is captured by saying that

[figure: \begin{matrix}R(Q) & R(P) \\ X_{1}(Q) & X_{1}(P) \end{matrix}; R(m); _{f_{1}_{Q}}; _{f_{1}_{P}}; X_{1}(m)]

is a quasi-pullback in Set (i.e. we have the existence condition, but not necessarily the uniqueness condition, of a pullback)—here f_{1} : R → X_{1} is the projection to the first coordinate restricted to R. But this condition says f_{1} is an open morphism—a consequence of the Yoneda Lemma (in fact, this formulation of open maps is that used in[4]). Similarly, f_{2} : R → X_{2} got via projection, is open and we have a span of open morphisms

[figure: \begin{aligned}& R \\ X_{1} & & X_{2} \end{aligned}; f_{1}; f_{2}]

establishing that X_{1}, X_{2} are P-bisimilar. □

We conclude this section by showing that the two relations of P-bisimilarity and strong path bisimilarity with respect to P coincide for the specific models of Section 1. Because in the path category Bran_{L} there is at most one morphism between any two path objects, for transition systems with this choice of path category, strong path bisimilarity is equivalent to path bisimilarity.

Theorem 17 For transition systems over a labelling set L, with branches Bran_{L} as path objects, Bran_{L}-bisimilarity, path bisimilarity and strong path bisimilarity with respect to Bran_{L}, all coincide with strong bisimilarity in Milner’s sense.

Proof: If two transition systems in T_{L} are (strong) path bisimilar with respect to Bran_{L}, then they are strong bisimilar in Milner’s sense: given a (strong) path bisimulation between transition systems T_{1} and T_{2}, define the relation R to consist of those pairs of states (s_{1}, s_{2}) of T_{1} and T_{2} for which there is (p_{1}, p_{2}) in the path bisimulation and s the final state in the branch which is their common domain such that

p_{1}(s) = s_{1} and p_{2}(s) = s_{2}

—the relation R may be checked to be a strong bisimulation. The remaining claims have already been proved (Lemma 15, Theorem 2). □

On event structures, path bisimulations and history-preserving bisimulations are intimately related; any path bisimulation includes a history-preserving bisimulation which generates it, as is shown in the following proof:

Lemma 18 Two event structures E_{1}, E_{2} in E_{L} are (strong) path bisimilar, with pomsets Pom_{L} as paths, iff E_{1}, E_{2} are (strong) history-preserving bisimilar.

Proof: “if”: Assume E_{1}, E_{2} are related by a (strong) path bisimulation R. Say (p_{1}, p_{2}) ∈ R is extremal when any epi-mono factorisation

[figure: \begin{aligned}& P \\ E_{1} & Q & E_{2} \end{aligned}; p_{1}; m; p_{2}; q_{1}; q_{2}]

with p_{1} = q_{1} ∘ m and p_{2} = q_{2} ∘ m, implies m is an isomorphism. Because R is a path bisimulation, if (p_{1}, p_{2}) ∈ R are extremal then p_{1} and p_{2} are isomorphisms when restricted to their ranges regarded as pomsets. We can define

H = {(x_{1}, p_{2} ∘ p_{1}^{−1}, x_{2}) |(p_{1}, p_{2}) ∈ R is extremal and
x_{1}, x_{2} are the ranges of p_{1}, p_{2}}.

From R being a (strong) path bisimulation it follows that H is a (strong) historypreserving bisimulation. “only if”: Conversely, given a (strong) history preserving bisimulation H, we can define a (strong) path bisimulation R. First note that for (x, θ, x_{2}) ∈ H, the isomorphism θ carries a pomset structure induced by that of x_{1} and x_{2}; we will identify θ with its associated pomset. Write p_{1}(θ), p_{2}(θ) for the compositions

\begin{matrix}p_{1}(θ) : θ → x_{1} ↪ E_{1}, \\ p_{2}(θ) : θ → x_{2} ↪ E_{2}, \end{matrix}

where θ, x_{1}, x_{2} are identified with pomsets, the morphisms θ → x_{1}, θ → x_{2} are got by projections and x_{1} ↪ E_{1}, x_{2} ↪ E_{2} are the inclusions of configurations. Now, define

R = {(p_{1}(θ) ∘ m, p_{2}(θ) ∘ m | m : P → θ & ∃x_{1}, x_{2}. (x_{1}, θ, x_{2}) ∈ H}.

The relation R inherits the properties required of a (strong) path-relation from those of the (strong) history-preserving bisimulation H. □

Theorem 19 For transition systems with independence over a labelling set L, with pomsets Pom_{L} as path objects, (i) Pom_{L}-bisimilarity and strong path bisimilarity coincide, and hold of two

transition systems with independence precisely when they unfold to event structures which are are strong history-preserving bisimilar,

(ii) two transition systems with independence are path bisimilar precisely when they unfold to event structures which are history-preserving bisimilar.

Proof: By combining Lemmas 18 and 15 in the light of Theorem 9. □

The logic of path assertions is, of course, characteristic for P-bisimilarity when this coincides with strong path bisimilarity; in particular this holds of the models, with the choice of path objects, in the theorems above.

6 Concluding remarks

The operations of process algebra arise as universal constructions in the categories of models discussed here (see [14]). Many of the process-algebra operations (product, sums in rooted presheaves, cartesian liftings in bifibration like that got from presheaves, ⋯) preserve open maps for general reasons and so respect bisimulation by virtue of its abstract definition. We could wish for a more workable logic characteristic for bisimulation on event structures and transition systems with independence than that of Section 5. A step in this direction and an alternative characterisation of Pom_{L}-bisimulation is presented in [8]. This article concentrates on generalisations of Milner’s strong bisimulation. What of weak bisimulation? One way is to imitate Milner who derives weak bisimulation from strong bisimulation between modifications of the original transition systems (based on his transition relations ⇒^{a}). A preliminary idea is to define weak bisimulation between objects X, Y as strong bisimulation between T (X), T (Y), the results of a functorial analogue to Milner’s modification to transition systems. The presheaf models seem promising. As remarked, the refinement operation which arises there from Kan extensions should be related to existing definitions of refinement on event structures for instance. The move to presheaf models means that we can use the abstract axioms satisfied by open maps [4] to establish bisimulations between presheaves. The notion of bisimulation is parameterised by the choice of model, presented as a category, and within that a choice of path objects. Clearly one could vary the choice of path category and explore the subsequent notion of bisimulation. Here we have restricted attention to finite paths. Generalisations such as that to presheaves (or more likely sheaves) over possibly infinite path objects may be a suitable way to extend the treatment here to cope with phenomena such as fairness.

References

[1] Benson, D.B., and Ben-Shachar, O., Bisimulation of automata. Information and Computation, 79, pp.60-83, 1988.

[2] Castellani, I., Bisimulation and abstraction homomorphisms. Proc. of CAAP 85, Springer Lecture Notes in CS, 1985.

[3] Van Glabeek, R.J., and Goltz, U., Equivalence notions for concurrent systems and refinement of actions. Proc of MFCS, Springer Lecture Notes in CS vol.379, 1989.

[4] Joyal, A., and Moerdijk, I., A completeness theorem for open maps. To appear.

[5] MacLane, S., Categories for the Working Mathematician. Graduate Texts in Mathematics, Springer, 1971.

[6] Milner,A.R.G.,Calculus of communicating systems.LNCS 92, 1980.

[7] Milner,A.R.G., Communication and concurrency. Prentice Hall, 1989.

[8] Nielsen, M., and Clausen, C., Bisimulations, Games, and Logic. To be published in New Results in Theoretical Computer Science, Springer Lecture Notes, 1994.

[9] Pratt, V.R., Modelling concurrency with partial orders, International Journal of Parallel Programming, 15,1, pp. 33–71, 1986.

[10] Rabinovitch, A., and Traktenbrot, B., Behaviour structures and nets. Fundamenta Informatica, 11(4), pp.357-404, 1988.

[11] Segerberg, K., Decidability of S4.1, Theoria 34, pp.7-20, 1968.

[12] Van Bentham, J., Correspondence theory. In the Handbook of Philosophical Logic, Vol.II, ed. Gabbay and Guenther, Reidel, pp.167-247, 1984

[13] Winskel,G., Event structures. LNCS 255, 1987.

[14] Winskel, G., and Nielsen, M., Models for concurrency. To appear as a chapter in the Handbook of Logic in Computer Science, Oxford University Press. A draft appears as Aarhus University DAIMI PB 429, 1992.

Recent Publications in the BRICS Report Series

RS-94-1 Glynn Winskel. Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk. February 1994, 8 pp.

RS-94-2 Alexander E. Andreev. Complexity of Nondeterministic Functions. February 1994, 47 pp.

RS-94-3 Uffe H. Engberg and Glynn Winskel. Linear Logic on Petri Nets. February 1994, 54 pp. To appear in Proceedings of REX, LNCS, 1993.

RS-94-4 Nils Klarlund and Michael I. Schwartzbach. Graphs and Decidable Transductions based on Edge Constraints. February 1994, 19 pp. Appears in: Trees in Algebra and Programming CAAP ’94 (ed. S. Tison), LNCS 787, 1994.

RS-94-5 Peter D. Mosses. Uni�ed Algebras and Abstract Syntax. March 1994, 21 pp. To appear in: Recent Trends in Data Type Speci�cation (ed. F. Orejas), LNCS 785, 1994.

RS-94-6 Mogens Nielsen and Christian Clausen. Bisimulations, Games and Logic. April 1994, 37 pp. Full version of paper to appear in: New Results and Trends in Computer Science, LNCS, 1994.

RS-94-7 Andr� e Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from Open Maps. May 1994, 42 pp. Submitted to a LICS 93 special issue of Information and Computation.