BRICS RS-95-4 Nielsen & Winskel: Petri Nets and Bisimulations

BRICS

Basic Research in Computer Science

Petri Nets and Bisimulations

Mogens Nielsen Glynn Winskel

BRICS Report Series RS-95-4 ISSN 0909-0878 January 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

PETRI NETS AND BISIMULATION

Mogens Nielsen Glynn Winskel Department of Computer Science, University of Aarhus, Denmark

Abstract

Several categorical relationships (adjunctions) between models for concurrency have been established, allowing the translation of concepts and properties from one model to another. A central example is a coreflection between Petri nets and asynchronous transition systems. The purpose of the present paper is to illustrate the use of such relationships by transferring to Petri nets a general concept of bisimulation.

Introduction

Category theory has been used to structure the seemingly confusing world of models for concurrency—see [27] for a survey. The general idea is to formalize that one model is more expressive than another in terms of an “embedding”, most often taking the form of a coreflection, i.e. an adjunction in which the unit is an isomorphism. The models are equipped with behaviour preserving morphisms, to be thought of as kinds of simulations. Besides providing an abstract language for expressing relationships between seemingly very different models, category theory also allows the translation of constructions and properties between models via adjunctions. For instance, most process algebra constructs, like parallel and nondeterministic composition, may be understood in terms of universal constructions, like product and coproduct. The preservation properties of adjoints are helpful in showing, and explaining why, semantics is respected in moving from one model to another. A coreflection central to this paper is that embedding asynchronous transition systems, in the sense of Bednarczyk [1] and Shields [22], in Petri nets.

The purpose of this paper is to illustrate the translation of concepts between models, focussing here on the transference of the concept of bisimulation to Petri nets from other models. The notion of bisimulation was defined categorically in [8] in a form directly applicable to a wide range of models equipped with a notion of path. This general definition takes the form of an existence of a span of open maps. In [8] it was shown that in the special case of standard labelled transition systems with sequential paths, the definition agrees with the strong bisimulation of Milner [12], and in the case of event structures with nonsequential paths in the form of pomsets, the definition yielded an interesting strengthening of the history-preserving bisimulation introduced by Rabinovitch and Trakhtenbrot [20]. Here we show how the coreflection from other models to nets combined with abstract properties of the general definition of bisimulation from [8], provides a notion of bisimulation on nets which automatically inherits a number of important properties.

The main message of this paper is that the categorical view of models for concurrency, like Petri nets, provides guidelines for definitions of concepts like behavioural equivalences, consistent across a range of models. We illustrate how a notion of bisimulation can be read off for nets, and that this comes automatically equipped with a number of essential properties. The categorical approach here contrasts with the more common alternative of searching for a sensible candidate for bisimulation on nets and, having found one of then checking it possesses these essential properties.

A word on our choice of morphisms, which might otherwise seem rather arbitrary. Objects of our categories will represent processes. Morphisms will represent a relationship between one process and another. Following [27], the morphisms we focus on here arise in relating the behaviours of processes and their components in languages like CCS. In CCS, communication is based on the synchronisation of atomic actions. Because of this we can restrict attention to morphisms which respect the granularity of actions, in the sense that an action may only be sent to at most one action, and not to a computation consisting of several actions. As is shown in [27], the resulting definitions of morphisms are sufficient to express via morphisms the relationship between a constructed process and its components built up using the operations of CCS. Conversely the choice of morphisms also produces universal constructions which form the basis of a process description language. This language is a little richer than that of CCS and CSP in the sense that their operations are straightforwardly definable within it.

1 Models—a coreflection

In this section we introduce the models of Petri nets and asynchronous transition systems, and present a coreflection between them. The purpose is mainly to set the scene for the main results in the next section, and hence the presentation here focusses on central definitions and constructions. For further details and all missing proofs we refer to [27].

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′.

It is convenient to introduce idle transitions, associated with any state. This has to do with our representation of partial functions. We view a partial function from a set L to a set L′ as a (total) function λ : L ∪ {∗} → L′ ∪ {∗} such that f(∗) = ∗, where ∗ is a distinguished element standing for “undefined”. This representation is reflected in our notation λ : L →_{∗} L′ for a partial function λ from L to L′. It assumes that ∗ does not appear in the sets L and L′, and more generally we shall assume that the reserved element ∗ does not occur in any of the sets of the structures we consider. The expected composition of partial functions is obtained by composing their representations. We shall identify total functions on a set L with partial functions never yielding ∗ on L.

Definition: Let T = (S, i, L, tran) be a transition system. An idle transition of T typically consists of (s, ∗, s), where s ∈ S. Define

tran_{∗} = tran ∪ {(s, ∗, s) | s ∈ S}.

Idle transitions help give a simple definition of morphism between transition systems.

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}, a function between sets of states,

• λ : L_{0} →_{∗} L_{1}, a partial function between sets of labels, are such that σ(i_{0}) = i_{1} and

(s, a, s′) ∈ tran_{0} ⇒ (σ(s), λ(a), σ(s′)) ∈ tran_{1}_{∗}.

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. In our definition of morphism, idle transitions represent this inaction, so we avoid the fuss of considering whether or not λ(a) is defined. With the introduction of idle transitions, morphisms on transition systems can be described as preserving transitions and the initial state. It is stressed that an idle transition (s, ∗, s) represents inaction, and is to be distinguished from the action expressed by a transition (s, a, s′) for a label a.

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 Petri nets

A Petri net may be seen as a transition system with an explicit representation of (global) states as sets of (local) states (usually called conditions). The specific version adopted here was introduced in [10].

Definition: A Petri net consists of (B, M_{0}, E, pre, post) where

B is a set of conditions, with initial marking M_{0} a nonempty subset of B, E is a set of events, and pre : E→Pow(B) is the precondition map such that pre(e) is nonempty for all e ∈ E, post : E → Pow(B) is the postcondition map such that post(e) is nonempty for all e ∈ E.

A Petri net comes with an initial marking consisting of a subset of conditions which are imagined to hold initially. Generally, a marking, a subset of conditions, formalizes a notion of global state by specifying those conditions which hold. Markings can change as events occur, precisely how being expressed by the transitions

M →^{e} M′

events e determine between markings M, M′. In defining this notion it is convenient to extend events by an “idling event”.

Definition: Let N = (B, M_{0}, E, pre, post) be a Petri net with events E. Define E_{∗} = E ∪ {∗}. We extend the pre and post condition maps to ∗ by taking

pre(∗) = ∅, post(∗) = ∅.

Notation: Whenever it does not cause confusion we write^{•}e for the preconditions pre(e) and e^{•} for the postconditions, post(e), of e ∈ E_{∗}. We write ^{•}e^{•} for ^{•}e ∪ e^{•}.

Definition: Let N = (B, M_{0}, E, pre, post) be a net. For M, M′ ⊆ B and e ∈ E_{∗}, define

M →^{e} M′ iff ^{•}e ⊆ M & e^{•} ⊆ M′ & M \^{•}e = M′ \ e^{•}.

Say e_{0}, e_{1} ∈ E_{∗} are independent iff ^{•}e_{0}^{•} ∩^{•}e_{1}^{•} = ∅. A marking M of N is said to be reachable when there is a sequence of events, possibly empty, e_{1}, e_{2} … e_{n} such that

M_{0} →^{e_{1}} M_{1} →^{e_{2}} ⋯ →^{e_{n}} M_{n} = M.

in N. There is contact at a marking M when for some event e, all its preconditions are marked at M and yet e cannot ocur at M:

•e ⊆ M & e^{•} ∩ (M \^{•}e) ≠ ∅.

A net is said to be safe when contact never occurs at any reachable marking.

Example: The following is an example of a standard graphical representation of a safe net with six events and nine conditions. Notice in particular that events e_{0} and e_{1} are independent, whereas e_{3} and e_{4} are not. One of the essential properties of nets is this possibility of specifying independence amongst events in terms of pre- and postconditions.

[figure: e_{3}; e_{4}; e_{1}; e_{0}; e_{2}; e_{5}; ·; ·; ·]

As morphisms on nets we take:

Definition: Let N = (B, M_{0}, E, pre, post) and N′ = (B′, M′_{0}, E′, pre′, post′) be nets. A morphism (β, η) : N → N′ consists of a relation β ⊆ B ×B′, such that its opposite relation β^{op} ⊆ B′ × B is a partial function from B′ to B, and a partial function η : E →_{∗} E′ such that

βM_{0} = M′_{0},
β^{•}e = ^{•}η(e) and
βe^{•} = η(e)^{•}.

Thus morphisms on nets preserve initial markings and events when defined. A morphism (β, η) : N → N′ expresses how occurrences of events and conditions in N induce occurrences in N′. Morphisms on nets preserve behaviour:

Proposition 1 Let N = (B, M_{0}, E, pre, post), N′ = (B′, M′_{0}, E′, pre′, post′) be nets. Suppose (β, η) : N → N′ is a morphism of net.

• If M →^{e} M′ in N then βM →^{η(e)} βM′ in N′.

• If ^{•}e_{1}^{•} ∩^{•}e_{2}^{•} = ∅ in N then ^{•}η(e_{1})^{•} ∩^{•} η(e_{2})^{•} = ∅ in N′.

Proof: By definition,

•η(e) = β^{•}e and η(e)^{•} = βe^{•}

for e an event of N. Observe too that because β^{op} is a partial function, β in addition preserves intersections and set differences. These observations mean that βM →^{η(e)} βM′ in N′ follows from the assumption that M →^{e} M′ in N, and that independence is preserved. □

Proposition 2 Nets and their morphisms form a category in which the composition of two morphisms (β_{0}, η_{0}) : N_{0} → N_{1} and (β_{1}, η_{1}) : N_{1} → N_{2} is (β_{1} ∘ β_{0}, η_{1} ∘ η_{0}) : N_{0} → N_{2} (composition in the left component being that of relations and in the right that of partial functions).

Definition: Let N be the category of nets described above.

Remark The rich structure of conditions on nets leaves room for variation, and another definition of morphism gives sensible results on the subclass of “safe” nets. A limitation with the above definition of morphism on nets is that it does not permit all “folding” morphisms of the kind illustrated in the example below.

[figure: ⋮; b_{2}; e_{1}; b_{1}; ·; b; e; e_{0}; b_{0}; ·]

The folding sends each event e_{0}, e_{1}, … to the common event e, and each condition b_{0}, b_{1}, … to the condition b. By restricting attention to safe nets we can relax the definition of morphisms on nets to include foldings, as in [25, 26], and still parallel the results of this paper—see [27] and the remark following Corollary 21.

1.3 Asynchronous transition systems

Following tradition, the behaviour of a net may be described via its reachable case graph, i.e. a transition system in which the states are the reachable markings and the transitions are triples

M →^{e} M′

as defined above. The case graph of our previous net example will be as follows:

[figure: •; •; •; •; e_{4}; e_{4}; e_{3}; e_{3}; e_{0}; e_{1}; e_{1}; e_{0}; •; •; •; I; e_{5}; e_{2}]

Notice how the event pairs (e_{0}, e_{1}) and (e_{3}, e_{4}) give rise to the same kind of diamonds in the underlying transition system. Hence, in order to get a representation of the important distinction between the pairs in terms of independence, we need to add some structure to the notion of case graph, here indicated by the I in the independent diamond. This is exactly the motivation behind asynchronous transition systems, as introduced independently by Bednarczyk [1] and Shields [22]. The idea on which they are based is simple enough: extend transition systems by, in addition, specifying which transitions are independent of each other. More accurately, transitions are to be thought of as occurrences of events which bear a relation of independence.

Definition: An asynchronous transition system consists of (S, i, E, I, tran) where (S, i, E, tran) is a transition system, I ⊆ E^{2}, the independence relation is an irreflexive, symmetric relation on the set E of events such that

(1) e ∈ E ⇒ ∃s, s′ ∈ S. (s, e, s′) ∈ tran

(2) (s, e, s′) ∈ tran & (s, e, s′′) ∈ tran ⇒ s′ = s′′

(3) e_{1}Ie_{2} & (s, e_{1}, s_{1}) ∈ tran & (s_{1}, e_{2}, u) ∈ tran ⇒ ∃s_{2}. (s, e_{2}, s_{2}) ∈ tran & (s_{2}, e_{1}, u) ∈ tran.

Say an asynchronous transition system is coherent if it also satisfies

(4) e_{1}Ie_{2} & (s, e_{1}, s_{1}) ∈ tran & (s, e_{2}, s_{2}) ∈ tran ⇒ ∃u. (s_{1}, e_{2}, u) ∈ tran & (s_{2}, e_{1}, u) ∈ tran.

Axiom (1) says every event appears as a transition, and axiom (2) that the occurrence of an event at a state leads to a unique state. Axioms (3) and (4) express properties of independence: if two independent events can occur one immediately after the other then they should be able to occur with their order interchanged (3); if two events can occur independently from a common state then they can occur together and in so doing reach a common state (4). Both situations lead to an “independence square” associated with the independence e_{1}Ie_{2}:

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

Morphisms between asynchronous transition systems are morphisms between their underlying transition systems which preserve the additional relations of independence.

Definition: Let T = (S, i, E, I, tran) and T′ = (S′, i′, E′, I′, tran′) be asynchronous transition systems. A morphism T → T′ is a morphism of transition systems

(σ, η) : (S, i, E, tran) → (S′, i′, E′, tran′)

such that

e_{1}Ie_{2} & η(e_{1}), η(e_{2}) both defined ⇒ η(e_{1})I′η(e_{2}).

Morphisms of asynchronous transition systems compose as morphisms between their underlying transition systems, and are readily seen to form a category.

Definition: Let A be the category of asynchronous transition systems.

1.4 Asynchronous transition systems and nets

1.4.1 An adjunction

There is an adjunction between the categories A and N.^{1} First, we note there is an obvious functor from nets to asynchronous transition systems, that associated with the case graph of a net.

1The adjunction between coherent asynchronous transition systems and nets is shown in detail in [27], to which the reader can refer for missing details (including missing proofs) in this section—the argument is virtually unaffected when working with the broader category of all asynchronous transition systems.

Definition: Let N = (B, M_{0}, E,^{•}( ), ( )^{•}) be a net. Define na(N) = (S, i, E, I, tran) where

S = Pow(B) with i = M_{0}, e_{1}Ie_{2} ⇔^{•} e_{1}^{•} ∩^{•}e_{2}^{•} = ∅,

(M, e, M′) ∈ tran ⇔ M →^{e} M′ in N, for M, M′ ∈ Pow(B).

Let (β, η) : N → N′ be a morphism of nets. Define

na(β, η) = (σ, η)

where σ(M) = βM, for any M ∈ Pow(B).

It may be shown [27] that na is indeed a functor, and that the construction na(N), for a net N, yields a coherent asynchronous transition system.

As a preparation for the definition of a functor from asynchronous transition systems to nets we examine how a condition of a net N can be viewed as a subset of states and transitions of the asynchronous transition system na(N). Intuitively the extent |b| of a condition b of a net is to consist of those markings and transitions at which b holds uninterruptedly. In fact, for simplicity, the extent |b| of a condition b is taken to be a subset of tran_{∗}, the transitions (M, e, M′) and idle transitions (M, ∗, M) of na(N); the idle transitions (M, ∗, M) play the role of markings M.

Definition: Let b be a condition of a net N. Let tran be the transition relation of na(N). Define the extent of b to be

|b| = {(M, e, M′) ∈ tran_{∗} | b ∈ M & b ∈ M′ & b ∉^{•} e^{•}}.

Not all subsets of transitions tran_{∗} of a net N are extents of conditions of N. For example, if (M, e, M′) ∉ |b| and (M′, ∗, M′) ∈ |b| for a transition M →^{e} M′ in N this means the transition starts the holding of b. But then b ∈ e^{•} so any other transition P →^{e} P′ must also start the holding of b. Of course, a condition cannot be started or ended by two independent events because, by definition, they can have no pre- or postcondition in common. These considerations motivate the following definition of condition of a general asynchronous transition system. The definition is a generalization of the notion of regions for transition systems introduced by Ehrenfeucht and Rozenberg [17].

Definition: Let T = (S, i, E, I, tran) be an asynchronous transition system. Its conditions are nonempty subsets b ⊆ tran_{∗} such that

(1) (s, e, s′) ∈ b ⇒ (s, ∗, s) ∈ b & (s′, ∗, s′) ∈ b (2) (i) (s, e, s′) ∈^{•} b & (u, e, u′) ∈ tran ⇒ (u, e, u′) ∈^{•} b

(ii) (s, e, s′) ∈ b^{•} & (u, e, u′) ∈ tran ⇒ (u, e, u′) ∈ b^{•}

where for (s, e, s′) ∈ tran we define

(s, e, s′) ∈^{•} b ⇔ (s, e, s′) ∉ b & (s′, ∗, s′) ∈ b, (s, e, s′) ∈ b^{•} ⇔ (s, ∗, s) ∈ b & (s, e, s′) ∉ b, and •b^{•} =^{•} b ∪ b^{•}.

(3) (s, e_{1}, s′) ∈^{•} b^{•} & (u, e_{2}, u′) ∈^{•} b^{•} ⇒ ¬e_{1}Ie_{2}.

Let B be the set of conditions of T. For e ∈ E_{∗}, define

e^{•} = {b ∈ B | ∃s, s′. (s, e, s′) ∈^{•} b},
•e = {b ∈ B | ∃s, s′. (s, e, s′) ∈ b^{•}}, and
•e^{•} = ^{•}e ∪ e^{•}.

(Note that ^{•}∗^{•} = ∅.) Further, for s ∈ S, define M(s) = {b ∈ B | (s, ∗, s) ∈ b}.

As an illustrative exercise, we check that the extent of a condition of a net is indeed a condition of its asynchronous transition system.

Lemma 3 Let N be a net with a condition b. Its extent |b| is a condition of na(N). Moreover,

(I) (M, e, M′) ∈^{•} |b| ⇔ b ∈ e^{•}

(II) (M, e, M′) ∈ |b|^{•} ⇔ b ∈^{•} e.

whenever M →^{e} M′ in N.

Proof: We prove (I) (the proof of (II) is similar):

(M, e, M′) ∈^{•} |b| ⇔ (M, e, M′) ∉ |b| & (M′, ∗, M′) ∈ |b|
⇔ ¬(b ∈ M & b ∈ M′ & b ∉^{•} e^{•}) & b ∈ M′
⇔ (b ∉ M & b ∈ M′) or (b ∈^{•} e^{•} & b ∈ M′)
⇔ b ∈ e^{•}, as M →^{e} M′.

Using (I) and (II), it is easy to check that |b| is a condition of na(N)—note that |b| is nonempty because it contains, for instance, ({b}, ∗, {b}). □

Definition: Let (σ, η) : T → T′ be a morphism between asynchronous transition systems T = (S, i, E, I, tran) and T′ = (S′, i′, E′, I′, tran′). For b ⊆ tran′_{∗}, define

(σ, η)^{−1}b = {(s, e, s′) ∈ tran_{∗} | (σ(s), η(e), σ(s′)) ∈ b}

Definition: Let T = (S, i, E, I, tran) be an asynchronous transition system. Define an(T) = (B, M_{0}, E, pre, post) by taking B to be the set of conditions of T, M_{0} = M(i), with pre and post condition maps given by the corresponding operations in T, i.e. pre(e) =^{•} e and post(e) = e^{•} in T. Let (σ, η) : T → T′ be a morphism of asynchronoustransition systems. Define an(σ, η) = (β, η) where for conditions b of T and b′ of T′ we take

bβb′ iff b = (σ, η)^{−1}b′.

It may be shown that an as defined is indeed a functor, [27]. Let us illustrate here how a net is produced from an asynchronous transition system.

Example: Consider the following asynchronous transition system T with two independent events, 1 and 2:

[figure: \begin{aligned}& · \\ · & & · & 1 I 2 \\ & ⊙ \end{aligned}; 2; 1; 1; 2]

It has these conditions, where those transitions in the condition are represented by solid arrows:

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

[figure: \begin{aligned}& · \\ · & e & · \\ & · \end{aligned}; \begin{aligned}& · \\ · & f & · \\ & · \end{aligned}; \begin{aligned}& · \\ · & g & · \\ & · \end{aligned}]

Consequently the asynchronous transition system T yields this net an(T):

[figure: d; e; f; ·; 1; 2; g; ·; a; ·; b; ·; c; ·]

Theorem 4 The functors an : A → N and na : N → A form an adjunction with an left adjoint to na.

1.4.2 A coreflection

Neither A nor N embeds fully and faithfully in the other category via the functors of the adjunction. This accompanies the facts that neither unit nor counit is an isomorphism (see [9] p. 88); in passing from a net N to an∘na(N) extra conditions are most often introduced; the net an ∘ na(N) is always safe even though N is not, as we will see. While passing from an asynchronous transition system T to na ∘ an(T) can, not only blow-up the number of states, but also collapse states which cannot be separated by conditions; in addition, the asynchronous transition system na ∘ an(T) is always coherent even though T is not.

A (full) coreflection between asynchronous transition systems and nets can be obtained at the cost of adding three axioms. Let A^{0} be the full subcategory of asynchronous transition systems T = (S, i, E, I, tran) satisfying the following:

Axiom 1 Every state is reachable from the initial state, i.e. for every s ∈ S there is a chain of events e_{1}, …, e_{n}, possibly empty, for which i ^{\underline{e_{1}···e_{n}}}→ s, where i is the initial state.

Axiom 2 M(u) = M(s) ⇒ u = s, for all s, u ∈ S.

Axiom 3 ^{•}e ⊆ M(s) ⇒ ∃s′. (s, e, s′) ∈ tran, for all s ∈ S, e ∈ E.

There is a close similarity to the regional axioms characterizing the case graphs of elementary net systems in terms of the regional axioms of Ehrenfeucht and Rozenberg, as presented in [17]. Axioms 2 and 3 enforce two separation properties. The contraposition of Axiom 2 says

u ≠ s ⇒ M(u) ≠ M(s)

i.e. that if two states are distinct then there is a condition of T holding at one and not the other.

Asynchronous transition systems satisfying Axiom 3 are necessarily coherent:

Proposition 5 If an asynchronous transition system T satisfies Axiom 3 then T is coherent.

Proof: Suppose e_{1}Ie_{2} and (s, e_{1}, s_{1}), (s, e_{2}, s_{2}) are transitions in T. Let b be a condition of T which e_{2} exits, so in particular (s, ∗, s) ∈ b and (s, e_{2}, s_{2}) ∉ b. As e_{1}Ie_{2}, the condition b must contain (s, e_{1}, s_{1}) and so (s_{1}, ∗, s_{1}). Thus^{•}e_{2} ⊆ M(s_{1}). Axiom 3 now provides a transition (s_{1}, e_{2}, u). Property (3) in the definition of asynchronous transition systems together with property (1) (determinacy) now ensure coherence. □

Because the conditions of an asynchronous transition system support an operation of complementation (explained in [27]), Axioms 2 and 3 hold for any asynchronous transition system na(N) got from a net N, but obviously Axiom 1 does not—we need further to make all states reachable. But here we note that the subcategory of asynchronous transition systems in which all states are reachable is coreflective in A. The right adjoint to the inclusion functor, R, defined below, restricts to reachable states. Its composition with na yields the right adjoint of the coreflection between A^{0} and N.

Definition: Let A^{R} be the full subcategory of A consisting of asynchronous transition systems (S, i, E, I, tran) satisfying Axiom 1, i.e. so that all states s are reachable.

Let R act on an asynchronous transition system T = (S, i, E, I, tran) as follows:

R(T) = (S′, i′, E′, I′, tran′)

where

S′  consists of all reachable states of T
E′ = {e ∈ E | ∃s, s′ ∈ S′. (s, e, s′) ∈ tran}
I′ = I ∩ (E′ × E′)
tran′ = tran ∩ (S′ × E′ × S′).

For a morphism (σ, η) : T → T′ of asynchronous transition systems, define R(σ, η) = (σ′, η′) where σ′ and η′ are the restrictions of σ and η to the states, respectively events, of R(T).

We need the notion of reachable extent of a condition. This consists essentially of the reachable markings and transitions at which b holds uninterruptedly.

Definition: Let N be a net. Let tran_{∗} be the transitions and idle transitions of R ∘ na(N). Define

|b|^{R} = |b| ∩ tran_{∗}.

And finally we can state the main result of this section, quoted from [27].

Theorem 6 Defining na_{0} = R∘na, the composition of functors, yields a functor na_{0} : N → A^{0} which is right adjoint to an_{0} : A^{0} → N, the restriction of an to A^{0}.

The unit at T = (S, i, E, I, tran) ∈ A^{0} is an isomorphism

(σ, 1_{E}) : T → na_{0} ∘ an_{0}(T)

where σ(s) = M(s) for s ∈ S, making the adjunction a coreflection.

The counit at a net N is

(β, 1_{E}) : an_{0} ∘ na_{0} → N

where

cβb iff ∅ ≠ c = |b|^{R}

between conditions c of na_{0}(N) and b of N.

One consequence of the coreflection is that any net N can be converted to a safe net an_{0} ∘ na_{0}(N) with the same behaviour, in the sense that there is an isomorphism between the reachable asynchronous transition systems the two nets induce under na_{0}, for details see [27]. Another is that A^{0} has products and coproducts given by the same constructions as those of A.

The coreflection A^{0} → N cuts down to an equivalence of categories by restricting to the appropriate full subcategory of nets.

Definition: Let N^{0} be the full subcategory of saturated nets, i.e. nets such that

b ↦ |b|^{R}

is a bijection between conditions of N and those of na_{0}(N).

The nets in N^{0} are saturated with conditions in the sense that they have as many conditions as is allowed by their reachable behaviour and independence (regarded as an asynchronous transition system), see [27].

Theorem 7 The functor an restricts to a functor an_{0} : A^{0} → N^{0}. The functor R ∘ na restricts to a functor na_{0} : N^{0} → A^{0}. The functors an_{0}, na_{0} form an equivalence of categories.

1.5 Unfolding

There is a well-known operation of unfolding a transition system to a tree whose branches consist of sequences of occurrence of transitions that can be performed starting from the initial state. This operation in fact arises automatically as a right adjoint, part of a coreflection, between categories of synchronisation trees and transition systems. In more detail, define S, the category of synchronisation trees, to be the full subcategory of transition systems whose objects satisfy:

• every state is reachable,

• the transitive closure of the transition relation is acyclic, and

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

The inclusion functor st : S ↪ T has as right adjoint the functor ts : T → S which on objects T = (S, i, L, tran), a transition system, yields the synchronisation tree ts(T) = (S′, i′, L, tran′) where:

• The set S′ consists of all finite, possibly empty, sequences of transitions

(t_{1}, ⋯, t_{j}, t_{j+1}, ⋯, t_{n−1})

such that t_{j} = (s_{j−1}, a_{j}, s_{j}) and t_{j+1} = (s_{j}, a_{j+1}, s_{j+1}) whenever 1 < j < n. The element i′ = (), the empty sequence.

• The set tran′ consists of all triples (u, a, v) where u, v ∈ S′ and u = (u_{1}, …, u_{k}), v = (u_{1}, …, u_{k}, (s, a, s′)), obtained by appending an a transition to u.

The transition system T unfolds to a synchronisation tree whose states and arcs represent occurrences of states and transitions.

What is the analogue of unfolding for models like Petri nets and asynchronous transition systems? This time the notion of occurrence should take account of the independence present in these more detailed models. Several answers have been proposed, Mazurkiewicz trace languages [10], occurrence nets [16] and event structures [16], though they are all closely related. Here we focus on one, event structures.

The events of an event structure are to be thought of as representing individual occurrences of actions of a system. The structural parts of an event structure are intended to capture the causal and nondeterministic aspects of such computations:

Definition: Define an event structure to be a structure (E, ≤, Con) consisting of a set E, of events which are partially ordered by ≤, the causal dependency relation, and a consistency relation Con consisting of finite subsets of events, 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 axioms on the consistency relation express that all singletons of events are consistent, and that the relation is closed under subsets and downwards with respect to the causal dependency relation.

Say an event structure E = (E, ≤, Con) is coherent if the consistency relation Con is determined by consistency on pairs of events, or alternatively if there is a, necessarily unique, binary conflict relation # on events such that

X ∈ Con ⇔ ∀e_{1}, e_{2} ∈ X. ¬e_{1}#e_{2}.

We can describe coherent event structures by a triple (E, ≤, #) where, as before, E is a set of events partially ordered by a causal dependency relation ≤, and #, the conflict relation, is a binary, symmetric, irreflexive relation on events, which satisfy

\begin{matrix}\{e′ | e′ ≤ e\} is finite, \\ e#e′ ≤ e′′ ⇒ e#e′′ \end{matrix}

for all e, e′, e′′ ∈ E. The property of #, that two events causally dependent on conflicting events are themselves in conflict, follows from those of Con. We shall take the liberty of identifying (E, ≤, #), presenting a coherent event structure, with the associated event structure (E, ≤, Con); in other words, (E, ≤, #) should be understood as referring to the event structure (E, ≤, Con) it determines.

To understand the “dynamics” of an event structure (E, ≤, Con) we show how an event structure determines a asynchronous transition system (S, i, E, I, tran). Guided by our interpretation we can formulate a notion of computation state of an event structure (E, ≤, Con). 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

—all finite subsets of events in the same computation are consistent. Let C(E, ≤, #) denote the subsets of events satisfying these two conditions, traditionally called the configurations of the event structure. We let S be the set of finite configurations and i the empty configuration.

Events manifest themselves as atomic jumps from one configuration to another. For configurations x, x′ and event e, define

(x, e, x′) ∈ tran ⇔ e ∉ x & x′ = x ∪ {e}.

We take two events to be independent in the asynchronous transition system iff they are concurrent in the event structure, i.e.

e_{1}Ie_{2} ⇔ e_{1} co e_{2}.

It is easy to see that this indeed defines an asynchronous transition system, T = (S, i, E, I, tran) from the event structure E = (E, ≤, Con). Furthermore, a coherent event structure gives rise to a coherent asynchronous transition system. The construction, which we call ea, identifying an event structure with an asynchronous transition system, extends to a functor with the following definition of morphisms for event structures:

Definition: Let E = (E, ≤, Con) and E′ = (E′, ≤′, Con′) be event structures. A morphism from E to E′ consists of a total function η : E → E′ on events which satisfies

\begin{aligned}if x ∈ C(E) then & ηx ∈ C(E′) & \\ & ∀e_{0}, e_{1} ∈ x.η(e_{0}) = η(e_{1}) ⇒ e_{0} = e_{1}. \end{aligned}

Write E for the category of event structures; composition is the usual composition of partial functions. Write E^{0} for the subcategory of coherent event structures.

The construction ea extends to a full and faithful functor: Let η : E → E′ be a morphism of event structures; it determines a morphism

ea(η) = (σ, η) : ea(E) → ea(E′)

in which σ(x) = ηx, simply the direct image of a configuration x under η. The “inclusion” functor ea : E → A has a right adjoint ae : A → E unfolding an asynchronous transition system to an event structure, forming a coreflection. We won’t go into the details of the construction of a right adjoint here, referring the reader to [27]; there it is shown how an asynchronous transition system determines a Mazurkiewicz trace language (easy) from which an event structure is obtained (harder).^{2} The coreflection cuts down to one between the subcategory of coherent even structures and the subcategory of coherent asynchronous transition systems. In fact, the coreflection also cuts down to one, ea_{0} : E^{0} → A^{0}, ae_{0} : A^{0} → E^{0}. This is because it is easy to construct a net from a coherent event structure so that both induce the same asynchronous transition system (see [16, 27]); hence, images of E^{0} under ea lie in A^{0}.

2 Labelled models and bisimulation

The coreflections of the previous sections enable us to place Petri nets within a broader picture of models for concurrency—[27] gives a fuller view. They allow us to apply to nets a general notion of bisimulation, obtained from a span of open maps, proposed in [8].

2.1 Labelled models and their relationship

Like most models for concurrency, nets [18] and asynchronous transition systems [14], or more precisely their labelled versions, have been used as models for process languages like CCS, [12]. As an illustration, following [18], the CCS expression a.nil|b.nil is represented by the labelled net:

2In truth, this is only shown in detail for coherent structures in [27], though the slight generalisation, when coherence is not assumed, is also indicated there.

[figure: ·; ·; a; b]

In contrast the (strongly bisimilar) expression a.b.nil + b.a.nil is represented by:

[figure: a; b; b; a; ·]

There is a general way of introducing labels to models in such a way that one may carry over adjunctions between unlabelled models to their labelled counterparts. Here we sketch the idea, applicable to the categories of nets, asynchronous transition systems and event structures. We assume a category X of structures each of which possesses a distinguished set of events and where morphisms have as a component a partial function between sets of events.

(i) Add to structures X an extra component of a (total) labelling function l : E → L from the structure’s set of events E to a set of labels L; we obtain labelled structure as pairs (X, l).

(ii) We assume morphisms f : X → X′ of unlabelled structures include a component η between sets of events. A morphism of labelled structures (X, l) → (X′, l′) is a pair (f, λ) where f : X → X′ is a morphism on the underlying unlabelled structures and λ : L →_{∗} L′ is a partial function on the label sets such that λ ∘ l = l′ ∘ η. Composition of morphisms is done coordinatewise.

Morphisms between labelled structures are of this generality in order to obtain operations of process calculi as universal constructions. However, for our purpose of studying bisimulation, it suffices to work with subcategories of structures having a common set of labels L, and restrict to morphisms as above, but with the extra condition that the component λ is the identity on L—this implies that the event component η is total. We call the resulting category X_{L}; this subcategory is the fibre over L with respect to the obvious functor projecting labelled structures to their label sets. For emphasis:

• The objects of X_{L} consist of structures (X, l) where X is an object of X, and l : E → L is a (total) labelling function from E the events of X to the labelling set L

• The morphisms of X_{L} from (X, l) to (X′, l′) correspond to morphisms f : X → X′ of X of which the event component η preserves labels, i.e. l′∘η = l.

Correspondingly, for a set of labels L, we denote the fibres over L in the labelled versions of our categories of nets, asynchronous transition systems and event structures by N_{L}, A_{L}, A_{L}^{0} and E_{L}^{0} respectively. Similarly the category of transition systems over label set L, with morphisms having the identity as label component, will be denoted T_{L}, and its full subcategory of synchronisaton trees S_{L}. We remark that synchronisation trees can be identified with those event structures having empty co-relation.

It follows for general reasons [27] (and is easy to see) that the adjunction and coreflection between nets and asynchronous transition systems lift to a coreflection between the labelled versions. The modified adjoints are essentially the adjoints presented in the previous sections, simply carrying the label parts across from one model to the other. Furthermore, this coreflection is part of a collection of coreflections as in the diagram below.

[figure: \begin{matrix}S_{L} & T_{L} \\ E_{L}^{0} & A_{L}^{0} & N_{L} \end{matrix}; se; st; ea_{0}; an_{0}]

These are accompanied by the coreflection ea : E_{L} → A_{L} between labelled event structures and asynchronous transition systems in general. When specifying a functor of one of the coreflections above, we adopt a convention; for example the left adjoint from S_{L} to T_{L} is denoted st while its right adjoint is ts. The left adjoints, drawn above, embed one model in another. We have deliberately overloaded notation, and, for instance, used an_{0} also for the labelled version of the embedding of A_{L}^{0} into N_{L}. For details of the other coreflections we refer to [27]. The composition of right adjoints ne = ae_{0} ∘ na_{0} yields the unfolding of nets into event structures, familiar from [16] (though the functor adds an extra marked isolated condition). Coreflections compose so the composition of left adjoints en = an_{0} ∘ ea_{0} forms a coreflection with right adjoint ne. For readers familiar with net theory, we mention that for a net N, en ∘ ne(N) is simply the saturated version of the net unfolding of N as defined in [16]. Irritatingly, there are not coreflections from transition systems T_{L} to the categories of labelled nets N_{L} or asynchronous transition systems A_{L} or A_{L}^{0}. This is simply because, unlike transition systems, both labelled nets and labelled asynchronous transition systems allow more than one transition with the same label between two states. This stops the natural bijection required for the “inclusion” of transition systems to be a left adjoint.

2.2 Path-lifting morphisms

In this section we briefly present some of the main ideas, definitions and results from [8], providing a general notion of bisimulation applicable to a wide range of models. For the missing proofs we refer to [8].

Informally, a computation path should represent a particular run or history of a process. For transition systems, 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 one maximal branch; so the objects of Bran_{L} are essentially strings over alphabet L. 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 net 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. Note that Pratt’s pomsets, with labels in L, can be identified with special kinds of labelled event structures in E_{L}, those with consistency relation consisting of all finite subsets of events. 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}. What about computation paths in nets? The left adjoint an_{0} ∘ ea_{0} of the coreflection E_{L} → N_{L} embeds labelled event structures, and so pomsets, in labelled nets. This enables us to identify pomsets P in Pom_{L} with their images an_{0} ∘ ea_{0}(P) as labelled saturated nets in N_{L}. Now, we can take a computation path in a net N, with labelling set L, to be a morphism

p : P → N

in N_{L} from a pomset P, with labelling set L—where the pomset P is understood as the corresponding labelled saturated net in N_{L}. In future, when discussing nets, we will deliberately confuse pomsets with their image in N_{L} under the embedding.

Generally, assume a category of models M (this can be any of the categories of labelled structures 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 computation 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 8 With respect to a labelling set L, the Bran_{L}-open morphisms of T_{L} are the “zig-zag morphisms” of [23], the “p-morphism” of [21], the “abstraction homomorphisms” of [4], and the “pure morphisms” of [2], 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.

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 9 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 [12].

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 10 Pullbacks of P-open morphisms are P-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 11 The categories T_{L}, S_{L}, N_{L}, A_{L}^{0}, A_{L}, and E_{L} have pullbacks.

Proof: We show that N_{L} has pullbacks. There are coreflections from all categories S_{L}, E_{L}, A_{L}^{0} into N_{L}. Using the fact that right adjoints preserve limits, and pullbacks in particular, we obtain pullbacks in any of S_{L}, E_{L}, A_{L}^{0} as images under the right adjoints of the pullback in N_{L} of diagrams transported into N_{L} by the left adjoints. Because there are not coreflections from the categories T_{L} and A_{L} into nets, they require separate (though simple) treatments (or see [8]).

We construct pullbacks in N_{L} explicitly in the following way. Suppose f_{1} = (σ_{1}, η_{1}) : N_{1} → N_{0} and f_{2} = (σ_{2}, η_{2}) : N_{2} → N_{0} are morphisms in N_{L} where

N_{i} = (B_{i}, M_{i}, E_{i}, pre_{i}, post_{i}, l_{i}), i = 0, 1, 2.

We want to construct a pullback N = (B, M, E, pre, post, l), π_{1}, π_{2}:

[figure: \begin{matrix}N & N_{2} \\ N_{1} & N_{0} \end{matrix}; π_{2}; π_{1}; f_{2}; f_{1}]

The construction of the events of N, E, is based on pullbacks in the category of sets:

E = {(e_{1}, e_{2}) ∈ E_{1} × E_{2} | η_{1}(e_{1}) = η_{2}(e_{2})}

The construction of the conditions of N, B, is based on pushouts in the category of sets with partial functions. Let R denote the equivalence relation on B_{1} ∪ B_{2} generated by R_{0}, where

b_{1} R_{0} b_{2} iff there exists b_{0} in B_{0} such that
β_{1}(b_{0}) = b_{1} and β_{2}(b_{0}) = b_{2}

We define

B = the equivalence classes, c, of R, satisfying
β_{1}^{op}(c) = β_{2}^{op}(c).

And with these events and conditions of N we let:

M = {c ∈ B | c ⊆ M_{1} ∪ M_{2}}
pre((e_{1}, e_{2})) = {c ∈ B | c ⊆ pre_{1}(e_{1}) ∪ pre_{2}(e_{2})}
post((e_{1}, e_{2})) = {c ∈ B | c ⊆ post_{1}(e_{1}) ∪ post_{2}(e_{2})}
l((e_{1}, e_{2})) = l_{1}(e_{1})(= l_{2}(e_{2}))

And finally we define the components π_{1} = (β̄_{1}, η̄_{1}) and π_{2} = (β̄_{2}, η̄_{2}) of the pullback as follows:

η̄_{i}((e_{1}, e_{2})) = e_{i}
β̄_{i}(b_{i})  = the R-equivalence class of b_{i} if this belongs to B,

undefined otherwise.

We leave it to the reader to check that these constructions indeed define a pullback in N_{L} as required. All the required properties follow by simple calculations. □

Corollary 12 For all the model categories mentioned in previous proposition, and for all path categories, P_{L}, the relation of P_{L}-bisimilarity is an equivalence.

Finally, we present a few general facts from [8] about how open morphisms and bisimilarity are preserved and reflected by functors, especially when 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 2.1 in which the two categories of models share the same choice of path category, open morphisms and bisimilarity are preserved in both directions of the adjunction.

Proposition 13 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.

Lemma 14 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.

Corollary 15 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) M_{1}, M_{2} are P-bisimilar in M iff M_{1}, M_{2} are P-bisimilar in N.

(ii) N_{1}, N_{2} are P-bisimilar in N iff R(N_{1}), R(N_{2}) are P-bisimilar in M.

Proof:

(i) Directly from (i) of Lemma 14. (ii) “only if”: By Lemma 14(iii), a span of open morphisms in N has, as image under R, a span of open morphisms in M. Thus P-bisimilarity of N_{1}, N_{2} in N implies P-bisimilarity of R(N_{1}), R(N_{2}) in M. “if”: Suppose R(N_{1}), R(N_{2}) in M are P-bisimilar in M via a span of open morphisms f_{1} : M → R(N_{1}), f_{2} : M → R(N_{2}) in M. By Lemma 14(i), f_{1}, f_{2} form a span of open morphisms in N. The components of the counits of the coreflection ϵ_{1} : R(N_{1}) → N_{1} and ϵ_{2} : R(N_{2}) → N_{2} are open by Lemma 14(ii). Hence the compositions ϵ_{1} ∘ f_{1}, ϵ_{2} ∘ f_{2} form a span of open morphisms in N showing the P-bisimilarity of N_{1}, N_{2} in N. □

2.3 Pom_{L}-bisimulation for nets

We have already seen (Lemma 8, Theorem 9) 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 nets, with nonsequential observations in the form of pomsets.

We start by characterising Pom_{L}-open morphisms on labelled asynchronous transition systems. Following our convention, we shall identify pomsets with their image under the embedding E_{L} → A_{L}.

Proposition 16 The Pom_{L}-open morphisms of A_{L} are precisely those which satisfy the “zig-zag” condition of Proposition 8 and which, in addition, reflect consecutive independence, i.e. morphisms satisfying:

η is total and label preserving

whenever (σ(s), e′, u′) ∈ tran_{2} then there exists (s, e, u) ∈ tran_{1} such that η(e) = e′ and σ(u) = u′

whenever (s, e, u), (u, e′, v) ∈ tran_{1}, with s reachable, and η(e)I_{2}η(e′)

in T_{2}, then eI_{1}e′ in T_{1}.

Proof: The proof of this proposition is a straightforward modification of the proof of the corresponding result from [8]. We are going to refer to parts of this proof later, and so present a part in some detail.

Let f = (σ, η) : T → T′ be an open morphism in A_{L}. The function η is total and label preserving from definition of morphisms in A_{L}, and by considering linear pomsets, where causal dependency is a total order, it is clear as in Proposition 22, that f satisfies the “zig-zag” condition. The only nontrivial part is the reflection of consecutive independence.

Suppose

s →^{e} u and u →^{e′} v,

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

σ(s) →^{η(e)} σ(u) and σ(u) →^{η(e′)} σ(v)

and assume η(e) and η(e′) are independent in T′. Assume further l(e) = l(η(e)) = a and l(e′) = l(η(e′)) = a′.

Because s is reachable there is a chain of transitions

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

in T from its initial state i. Assume l(e_{i}) = a_{i}. Let P be the linear pomset with n + 2 elements, ordered and labelled as indicated in the following associated labelled asynchronous transition system (only labels indicated for the transitions):

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

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

[figure: s_{0}  s_{1}  ⋯  s  u  v.; e_{1}; e_{2}; e_{n}; e; e′]

in T. Let Q be the pomset differing from P only in that the a and a′ labelled elements are unordered, i.e. the pomset associated with the following labelled asynchronous transition system:

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

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

[figure: \begin{aligned}& & & & σ(u) \\ σ(s_{0}) & σ(s_{1}) & ⋯ & σ(s) & I & σ(v) \\ & & & & • \end{aligned}; η(e′); η(e_{1}); η(e_{2}); η(e_{n}); η(e); η(e′); η(e)]

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 e and e′ are independent in T. So because f is open it satisfies the “zig-zag” condition and reflects consecutive independence.

For the proof in the other direction we refer to [8].

□

And now to the question of bisimulations. In [8] it was shown that in the case of event structures taking the path category P to be pomsets one gets a reasonable strengthening of a previously studied equivalence, that of history-preserving 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.

Definition: (Rabinovitch-Trakhtenbrot [20], van Glabeek-Goltz [6])

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.

In [8] it is shown that Pom_{L}-bisimilarity of event structures in E_{L} coincides with their being strong history-preserving bisimilar. However, this in itself does not show that Pom_{L}-bisimilarity of event structures in the smaller category E_{L}^{0} of coherent event structures also coincides with strong historypreserving bisimilarity. There might conceivably be a span of open morphisms, f_{1} : E → E_{1}, f_{2} : E → E_{2}, from a noncoherent event structure E relating two coherent event structures E_{1}, E_{2} which could never be replaced by a span of open morphisms from a coherent event structure. In fact, such is not the case, because for any event structure E in E_{L} there is an open morphism f : E′ → E from a coherent event structure E′ (Lemma 18). Hence a span of open morphisms f_{1} : E → E_{1}, f_{2} : E → E_{2} in E_{L}, with E_{1}, E_{2} coherent, can always be converted to a span of open morphisms f_{1} ∘ f : E′ → E_{1}, f_{2} ∘ f : E′ → E_{2} in E_{L}^{0}. Consequently, Pom_{L}-bisimilarity in the subcategory of coherent event structures E_{L}^{0} coincides with strong history-preserving bisimilarity. This result will also have implications for Pom_{L}-bisimilarity between Petri nets, because of the coreflection from coherent event structures to nets.

Although we have not insisted on it, a reasonable requirement on event structures (and the other objects we consider here) is that they be countable. One might view with suspicion any result which depended crucially on allowing event structures to be uncountable. For this reason, some care has been taken to give countable constructions, at the cost of a little extra argumentation.

In preparation for the key lemma, Lemma 18, we first show how any consistency relation on events can be “simulated” by a conflict relation, ignoring for the moment causal dependency and labelling. A conflict relation consists of (E, #) where # is a binary irreflexive relation on E in accord with the terminology for event structures, we say a set X ⊆ E is consistent iff

∀e_{1}, e_{2} ∈ X. ¬e_{1}#e_{2}.

A consistency relation consists of (E, Con) where Con is a family of finite subsets of E satisfying the following property familiar from event structures:

\begin{matrix}\{e\} ∈ Con, \\ Y ⊆ X ∈ Con ⇒ Y ∈ Con, \end{matrix}

for all elements e, e′ and subsets X, Y of E. Of course, a conflict relation (E, #) determines a consistency relation (E, Con) in Con which consists of the finite consistent subsets of (E, #).^{3}

Lemma 17 Let Con be a consistency relation on a set A. There is #, a conflict relation on a set B and a function f : B → A such that:

3Conflict and consistency relations play a role in models of constructive logic, where they correspond to Girard’s coherent and qualitative domains [5].

(i) If X is a finite consistent subset of (B, #), then fX ∈ Con, and

∀b_{1}, b_{2} ∈ X. f(b_{1}) = f(b_{2}) ⇒ b_{1} = b_{2}.

(ii) If X is a finite consistent subset of (B, #) and

fX ⊆ Y, for Y ∈ Con,

then there is a finite consistent subset Z of (B, #) such that

X ⊆ Z and fZ = Y.

Moreover, if A is countable/finite then B can also be chosen to be countable/finite respectively.

Proof: Assuming a consistency relation (A, Con) we first define M to consist of the minimal inconsistent subsets of A, i.e.

M = {X ⊆ A | X ∉ Con & ∀Y ⫋ X.Y ∈ Con}.

Note sets in M are always finite. For a ∈ A, define

M(a) = {X ∈ M | a ∈ X}.

Now, define the set B to consist of elements of A with a twist. Formally, define the elements of B to be pairs

(a, t)

where a ∈ A and t, a twist, is a tuple ⟨t_{X}⟩_{X∈M(a)} of integers t_{X}, indexed by X ∈ M(a), such that 0 < t_{X} < |X|—here |X| denotes the size of X. (In particular, for a ∈ A, if M(a) = ∅, then a’s only twist is the empty tuple, whereas if M(a) consists solely of (unordered) pairs then all entries of its twists will be 1). Define a conflict relation on B, by setting

(a, t)#(a′, t′) iff a = a′ & t ≠ t′

or a ≠ a′ & ∃X ∈ M(a) ∩ M(a′). t_{X} = t′_{X}.

Define f : B → A to be the projection (a, t) ↦ a. We should show (i) and (ii) above.

We first observe the following “counting property” of consistent sets of (B, #):

If X is a consistent set of (B, #) and Y ∈ M, then

|{t_{Y} | ∃a ∈ Y. (a, t) ∈ X}| = |Y ∩ (fX)|.

To justify the counting property let

S = {(a, t) ∈ X | a ∈ Y }.

Then S, being a subset of X, is consistent in (B, #). The first clause in the definition of the conflict relation # on B ensures that |S| = |fS|. Clearly, fS = Y ∩ (fX), so

|S| = |Y ∩ (fX)|.

The second clause in the definition of #, ensures that

|S| = |{t_{Y} | ∃a ∈ Y. (a, t) ∈ X}|.

This establishes the counting property.

We now prove (i) and (ii).

(i) If (i) were to fail, there would be a consistent set X of (B, #) and Y ∈ M such that Y ⊆ fX. But then by the counting property

|{t_{Y} | ∃a ∈ Y. (a, t) ∈ X}| = |Y |.

However this is impossible as each t_{Y} is bounded within the interval {k | 0 < k < |Y |}, of size |Y | − 1.

(ii) It suffices to show the following claim:

Suppose X is a consistent set of (B, #) and (fX) ∪^{·} {a′} is a consistent set of (A, Con). Then there is a twist u such that (a′, u) ∈ B and X ∪^{·} {(a′, u)} is a consistent set of (B, #). [The notation x = y ∪^{·} z means x = y ∪ z & y ∩ z = ∅.]

To construct a suitable twist u we need to find an assignment u_{Y}, for each Y ∈ M(a′), such that

u_{Y} ∉ {t_{Y} | ∃a ∈ Y. (a, t) ∈ X}.

This is impossible only if

|{t_{Y} | ∃a ∈ Y. (a, t) ∈ X}| = |Y | − 1.

By the counting property, if this were so, then

|Y ∩ (fX)| = |Y | − 1.

But then

Y ⊆ (fX) ∪^{·} {a′},

contradicting the consistency of (fX) ∪^{·} {a′}. Thus we can find a twist u = ⟨u_{Y} ⟩_{Y ∈M(a′)} such that X ∪ {(a′, u)} is consistent.

The construction of (B, #) from (A, Con) can yield an uncountable set B even though A is countable. Suppose, for instance, that there is a ∈ A for which M(a) contains infinitely may sets of size greater than 2. Then B will include uncountably many elements of the form (a, t). However there will be a countable (B, #) fulfilling the conditions of the lemma when A is countable. The argument involves a little model theory. We can express the conditions on f : B → A as a countable theory in a predicate calculus. Our construction shows the theory to be consistent. It thus has a countable model (see e.g. Proposition 2.12, P.65 of [11]), from which we can extract the required countable (B, #) and f.

In more detail, we take a predicate calculus with equality, over two sorts α and β, a single unary operation F from β to α, binary relation # on β, and for each n ≥ 0 predicates Con_{n}^{α} and Con_{n}^{β} on α and β respectively. If A is finite the construction above clearly yields a finite B, so we can restrict attention to countably infinite A enumerated as

a_{0}, a_{1}, …, a_{m}, ….

We extend our language by constants a_{0}, a_{1}, …, a_{m}, … of sort α. The theory T is to consist of:

• those atomic assertions and their negations which hold of A, i.e. those assertions a_{i} = a_{j}, ¬(a_{i} = a_{j}), Con_{n}^{α}(a_{i_{1}}, …, a_{i_{n}}), ¬Con_{n}^{α}(a_{i_{1}}, …, a_{i_{n}}), which are true interpreted as assertions of consistency.

• the properties required of #, Con_{n}^{α}, Con_{n}^{β}, e.g. assertions such as

∀x_{1}, …, x_{n} : β. Con_{n}^{β}(x_{1}, …, x_{n}) ↔ ⋀_{i,j} ¬x_{i}#x_{j}

—here ⋀_{i,j} ¬x_{i}#x_{j} abbreviates a finite conjunction

⋯ ∧ ¬x_{i}#x_{j} ∧ ⋯ where i, j ≤ n,

saying consistency in β is equivalent to conflict freeness, and others saying that consistency predicates are invariant under permutation, that consistency is closed under inclusion and contains all singletons.

• the conditions required on F, of the form

∀x_{1}, …, x_{n} : β. Con_{n}^{β}(x_{1}, …, x_{n}) →

(Con_{n}^{α}(F (x_{1}), …, F (x_{n})) & (⋀_{i,j} F (x_{i}) = F (x_{j}) → x_{i} = x_{j}))

∀x_{1}, …, x_{n} : β, y : α. Con_{n}^{β}(x_{1}, …, x_{n}) ∧ Con_{n+1}^{α}(F (x_{1}), …, F (x_{n}), y)

→ (∃x : α. F (x) = y ∧ Con_{n+1}^{β}(x_{1}, …, x_{n}, x)).

The theory T is countable, and is satisfied by our construction, so consistent. Every countable consistent first-order theory has a countable model (see e.g. Proposition 2.12, P.65 of [11]). In particular, the theory T has a countable model in which F is interpreted as a function f′ from a countable set B′ to a countable set A′ which includes A. Restricting f′ to the inverse image B = f^{′−1}A we obtain a function f : B → A fulfilling the conditions required above, but now with respect to a countable (B, #) and (A, Con). □

Lemma 18 Let A = (A, ≤, Con, l) be a labelled event structure. Then, there is a labelled coherent event structure E = (E, ≤′, #′, l′) and an open morphism g : E → A.

Moreover, if A is countable/finite then so can E be taken to be countable/finite respectively.

Proof: There is a set B with binary conflict # and a function f : B → A satisfying the conditions of Lemma 17 with respect to the consistency relation Con on A. We first construct a labelled coherent asynchronous transition system T. Its states are finite consistent subsets x of (B, #) for which the direct image fx is a configuration of A. Its set of events is B with independence relation I where

b_{1}Ib_{2} iff ¬b_{1}#b_{2} & f(b_{1})cof(b_{2}).

Its labelling function is l ∘ f. Its transitions are all (x, b, x′) where x′ = x ∪^{·} {b} for x, x′ and b ∈ B.

It can be verified that T is a labelled coherent asynchronous transition system. For example, to show property (3), assume x is a state of T with transitions (x, b_{1}, x_{1}) and (x, b_{2}, x_{2}) where b_{1}Ib_{2}. Then x ∪ {b_{1}, b_{2}} is a consistent set of (B, #). Hence because f preserves consistency, fx ∪ {f(b_{1}), f(b_{2})} ∈ Con. The two sets fx_{1} = fx∪{f(b_{1})} and fx_{2} = fx∪{f(b_{2})} are configurations of A and so ≤-downwards closed. Hence their union fx ∪ {f(b_{1}), f(b_{2})} is consistent and ≤- downwards closed, and so a configuration of A. This ensures that u = x∪{b_{1}, b_{2}} is a state of T with transitions (x_{1}, b_{2}, u), (x_{2}, b_{1}, u), as required by (3).

There is an open morphism (σ, f) : T → ea(A) in A_{L}, where σ(x) = fx. Here we have recourse to Lemma 16 characterising open morphisms in A_{L} and make essential use of the properties of f, expressed in Lemma 17. The right adjoint ae of the coreflection between E_{L} and A_{L} preserves open morphisms, by Lemma 14(iii), and there is an isomorphism h : ae∘ea(A) ≅ A, by the coreflection. Hence g = h ∘ ae(σ, f) : ae(T) → A, being the composition of an open morphism with an isomorphism, is itself an open morphism in E_{L}. Because T is coherent it unfolds under ae to an event structure of the form ae(T) = (E, ≤′, #′, l′).

Because the constructions used in this proof preserve countability and finiteness, we see from Lemma 17, that in the proof B, and so E, may be made countable or finite according to whether A is countable or finite.

[We remark that an alternative proof is obtained by recognising that the states of T form the finite elements of a coherent stable family, and so of a coherent prime algebraic domain D. The event structure E is obtained, to within isomorphism, from the complete primes of D—see [25].] □

At long last we can show that restricting the category of event structures to those which are coherent does not effect the relation of bisimilarity.

Corollary 19 Let E_{1}, E_{2} be coherent event structures with labelling sets L. The following are equivalent:

(i) E_{1}, E_{2} are Pom_{L}-bisimilar in E_{L}^{0}.

(ii) E_{1}, E_{2} are Pom_{L}-bisimilar in E_{L}.

(iii) E_{1}, E_{2} are strong history-preserving bisimilar.

Proof: The equivalence between (i) and (ii) follows by Lemma 18. A span of open morphisms f_{1} : E → E_{1}, f_{2} : E → E_{2} in E_{L}, with E_{1}, E_{2} coherent, can be converted to a span of open morphisms f_{1} ∘ f : E′ → E_{1}, f_{2} ∘ f : E′ → E_{2} in E_{L}^{0}, where f : E′ → E is the open morphism provided by Lemma 18. The equivalence between (ii) and (iii) is shown in [8]. □

Via the coreflection between event structures and Petri nets, we can draw characterisations of Pom_{L}-bisimilarity on nets.

Theorem 20 Let N_{1}, N_{2} be nets with labelling sets L. The following are equivalent:

(i) The nets N_{1}, N_{2} are Pom_{L}-bisimilar in N_{L}.

(ii) The reachable case graphs na_{0}(N_{1}), na_{0}(N_{2}) are Pom_{L}-bisimilar in A_{L}^{0}.

(iii) The case graphs na(N_{1}), na(N_{2}) are Pom_{L}-bisimilar in A_{L}.

(iv) The unfoldings to event structures ne(N_{1}), ne(N_{2}) are strong history-preserving bisimilar.

Proof: The equivalence between (i) and (ii) follows by Corollary 15 applied to the coreflection A_{L}^{0} → N_{L}. Because of the coreflection E_{L}^{0} → A_{L}^{0}, Corollary 15 yields the equivalence of (ii) with:

(iv)′ The unfoldings to event structures ne(N_{1}), ne(N_{2}) are Pom_{L}-bisimilar in E_{L}^{0}.

As we have seen (Corollary 19), we have that (iv)′ is equivalent to (iv). Finally, (ii) and (iii) are equivalent by Proposition 13 because A_{L}^{0} is a full subcategory of A_{L}. □

So, for general reasons, the notion of bisimilarity for nets agrees with the notion of bisimilarity for the associated case graphs and unfoldings (where it amounts to strong history-preserving bisimilarity). Results expressing agreements of this kind would probably be required of any notion of bisimilarity, and, without the help of some categorical machinery, would seem to require separate proofs. Of course, now we have characterised Pom_{L}-bisimilarity on nets as strong history-preserving bisimilarity of their unfoldings to event structures, we may produce a characterisation in terms of nets and their “processes” along the lines of [24].

Many attempts have been made to define bisimilarity for noninterleaving models like Petri nets. The idea of parameterizing such definitions on a notion of observation is not new, see e.g. [3]. However, there are major differences with previous approaches. To point out one, we briefly address the question of robustness of our notion of bisimilarity. Of course, the results Corollary 19 and Theorem 20 show that the notion is robust across a range of models. But another issue is the sensitivity of our notion of Pom_{L}-bisimilarity for nets to the particular choice of path category Pom_{L}. The notion of Pom_{L}-bisimilarity might seem questionable to those who view general pomsets as not observable.

However, let us define a pomset to be an almost totally ordered multiset iff it is of one of the two simple forms considered in the proof of Proposition 16, i.e. allowing at most two (maximal) elements to be unordered. Note that in the range of subclasses of pomsets considered in the literature, [19], this class is as close to Bran_{L} as one can get! Let us denote the full subcategory of Pom_{L} consisting of object of this simple form by Atom_{L}.

Corollary 21

(i) A morphism in N_{L} is Pom_{L}-open iff it is Atom_{L}-open.

(ii) Two nets are Pom_{L}-bisimilar iff they are Atom_{L}-bisimilar.

Proof: Clearly (ii) follows from (i), so we concentrate on a proof of (i).

The “only if” part of (i) follows immediately from definition of open maps. By inspecting the proof of Proposition 16, we observe that a morphism in A_{L} is Pom_{L}-open if it is Atom_{L}-open. By Proposition 13, a similar statement also holds of the category A_{L}^{0}. Finally, a similar statement (the if part of (i)) holds also in N_{L} by Lemma 14. □

Remark Similar results hold for the alternative category of Petri nets mentioned in Section 1.2. In particular because there is also a coreflection between event structures and that category, Pom_{L}-bisimiliarity of nets in that framework will also amount to strong history-preserving bisimilarity of their event-structure unfoldings—another example of the robustness of the definitions.

3 Concluding remarks

We have illustrated how to introduce bisimilarity for Petri nets following a general pattern, a pattern which automatically guarantees consistency with bisimilarity on a number of related models. This sets the scene, but many questions are left open, including a theory of our bisimulation for nets parallelling the well established theory of bisimulation for transition systems. Some initial ideas may be found in the game theoretic and logical characterizations for Pom_{L}-bisimilation for transition systems with independence given in [15], which may be transferred immediately to nets, following the results of this paper. A particular unresolved issue is that of the decidability of our Pom_{L}-bisimilarity on finite nets and asynchronous transition systems.

References

[1] Bednarczyk, M.A., Categories of asynchronous systems, PhD thesis in Computer Science, University of Sussex, report no. 1/88, 1988.

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

[3] Degano, P., De Nicola, R. and Montanari, U., Observational equivalences for concurrency models, in Wirsing, M. (ed.), Formal Description of Programming Concepts – III, IFIP, Elsevier Science Publishers B.V., pp. 105–132, 1987.

[4] Castellani, I., Bisimulation and abstraction homomorphisms. Proc. of CAAP 85, Springer Lecture Notes in CS, vol. 185 , pp. 223–238, 1985.

[5] Girard, J-Y., Linear logic. Theoretical Computer Science 50, pp. 1–102, 1987.

[6] 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, pp. 237–248, 1989.

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

[8] Joyal, A., Nielsen, M., and Winskel, G., Bisimulation from open maps. Journal version of LICS93 article. BRICS report RS-94-7, Aarhus University, 1994.

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

[10] Mazurkiewicz, A., Basic notions of trace theory, in de Bakker, de Roever and Rozenberg (eds.), Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency, Springer Lecture Notes in CS, vol. 354, pp. 285–363, 1988.

[11] Mendelson, E., Introduction to mathematical logic. Van Nostrand Reinhold Company, 1964.

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

[13] Mukund, M., Petri nets and step transition systems. International Journal of Foundations of Computer Science, Vol 3, No 4, pp. 443–478, 1992.

[14] Mukund, M. and Nielsen, M., CCS, locations and asynchronous transition systems. In Shyamasundar, R. (ed.), FST & TCS 92, Springer Lecture Notes in CS 652, pp. 328–341, 1992.

[15] Nielsen, M., and Clausen, C., Bisimulations, Games, and Logic. Proceedings of CONCUR’94, Springer Lecture Notes in CS, vol. 836, pp. 385–400, 1994.

[16] Nielsen, M., Plotkin, G. and Winskel, G., Petri nets, Event structures and Domains, part 1. Theoretical Computer Science 13, pp. 85–108, 1981.

[17] Nielsen, M., Rozenberg, G. and Thiagarajan, P.S., Elementary transistion systems, Theoretical Computer Science 96, pp. 3–33, 1992.

[18] Olderog, E. R., Nets, terms and formulas. Cambridge Tracts in Theoretical Computer Science, 1991.

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

[20] Rabinovitch, A., and Trakhtenbrot, B., Behaviour structures and nets. Fundamenta Informatica, 11(4), pp. 357–404, 1988.

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

[22] Shields, M.W., Concurrent machines. Computer Journal, vol. 28, pp. 449– 465, 1985.

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

[24] Vogler, W., Deciding history preserving bisimilarity. Proceedings of ICALP 91, Springer Lecture Notes in CS 510, pp. 495–505, 1991.

[25] Winskel,G., Event structures. Springer Lecture Notes in CS 255, pp. 325– 392, 1987.

[26] Winskel, G., Petri nets, algebras, morphisms and compositionality, Information and Computation, 72, pp. 197–238, 1987.

[27] 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 BRICS Report RS-94-12, 1994.

Recent Publications in the BRICS Report Series

RS-95-4 Mogens Nielsen and Glynn Winskel. Petri Nets and Bisimulations. January 1995. 36 pp. To appear in TCS.

RS-95-3 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part I: A Denotational Model and Its Complete Axiomatization. January 1995. 37 pp.

RS-95-2 Franc�ois Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. January 1995. 21 pp.

RS-95-1 Gudmund Skovbjerg Frandsen, Thore Husfeldt, Peter Bro Miltersen, Theis Rauhe, and S�ren Skyum. Dynamic Algorithms for the Dyck Languages. January 1995. 21 pp.

RS-94-48 Jens Chr. Godskesen and Kim G. Larsen. Synthesizing Distinguishing Formulae for Real Time Systems. December 1994. 21 pp.

RS-94-47 Kim G. Larsen, Bernhard Steffen, and Carsten Weise. A Constraint Oriented Proof Methodology based on Modal Transition Systems. December 1994. 13 pp.

RS-94-46 Amos Beimel, Anna G� al, and Mike Paterson. Lower Bounds for Monotone Span Programs. December 1994. 14 pp.

RS-94-45 J�rgen H. Andersen, K� are J. Kristoffersen, Kim G. Larsen, and Jesper Niedermann. Automatic Synthesis of Real Time Systems. December 1994. 17 pp.

RS-94-44 Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. December 1994. PhD thesis. viii+224 pp.

RS-94-43 Luca Aceto and Alan Jeffrey. A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version). December 1994. 18 pp. To appear in Theoretical Computer Science.