BRICS RS-96-18 Hildebrandt & Sassone: Comparing TS with Independence and Asynchronous TS

BRICS

Basic Research in Computer Science

Comparing Transition Systems with Independence and Asynchronous Transition Systems

Thomas Troels Hildebrandt Vladimiro Sassone

BRICS Report Series RS-96-18 ISSN 0909-0878 June 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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@brics.dk

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

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

Comparing Transition Systems with Independence and Asynchronous Transition Systems

Thomas T. Hildebrandt^{∗} Vladimiro Sassone^{⋆,∗}

* BRICS – Computer Science Dept., University of Aarhus ⋆ Dipartimento di Informatica, Università di Pisa

\underline{Abstract}. Transition systems with independence and asynchronous transition systems are noninterleaving models for concurrency arising from the same simple idea of decorating transitions with events. They differ for the choice of a derived versus a primitive notion of event which induces considerable differences and makes the two models suitable for different purposes. This opens the problem of investigating their mutual relationships, to which this paper gives a fully comprehensive answer.

In details, we characterise the category of extensional asynchronous transitions systems as the largest full subcategory of the category of (labelled) asynchronous transition systems which admits TSI, the category of transition systems with independence, as a coreflective subcategory. In addition, we introduce event-maximal asynchronous transitions systems and we show that their category is equivalent to TSI, so providing an exhaustive characterisation of transition systems with independence in terms of asynchronous transition systems.

Introduction

Following the leading idea of CCS [11] and related process calculi [10, 2, 12, 9], the behaviour of concurrent systems is often specified extensionally by describing their ‘state-transitions’ and the observable behaviours that such transitions produce. The simplest formal model of computation able to express naturally this idea is that of labelled transition systems, where the labels on the transitions are thought of as the actions of the system at its ‘external ports’, or, more generally, the observable part of its behaviour.

Transition systems are an interleaving model of concurrency, which means that they do not allow to draw a natural distinction between interleaved and concurrent execution of actions. More precisely, transition systems do not model the fact that concurrent actions can overlap in time and reduce concurrency to a nondeterministic choice of action interleavings, so loosing track of the casual dependencies between actions and, consequently, of the fact that computations that differ only for the order of independent actions represent, actually, the same behaviour. In other words, interleaving models abstract away from the difference between the factual temporal occurrence order and the more conceptual causal ordering of actions. The simplest exemplification of this situation is provided by the CCS terms a | b and a.b + b.a, both described by the following transition

1

* Basic Research in Computer Science, Centre of the Danish National Research Foundation.

⋆ This author was supported by EU Human Capital and Mobility grant ERBCHBGCT920005.

system.

[figure: •; •; b; •; a; •; a; b]  (1)

Although for many applications this level of abstraction is appropriate, for several other kinds of analysis a model may be desirable that takes full account of concurrency. For instance, apart from any philosophical consideration about the semantic relevance of cause/effect relationships, knowing that different interleavings represent the same behaviour can reduce considerably the state-space explosion problem when checking system properties such as safety properties and fairness [8, 20, 16].

Several efforts have been devoted to the search of transition-based noninterleaving models, e.g., transition systems enriched with additional features that make expressing concurrency explicitly possible (cf., e.g., [17, 4, 6, 7, 5, 3]). The present paper focuses on two such models, namely asynchronous transition systems, introduced independently by Bednarczyk [1] and Shields [19], and transitions systems with independence, proposed by Winskel and Nielsen [21]. These two competing approaches are, among the others, those building on the simplest idea: endow transition systems with some formal notion of ‘similarity’ of transitions that enables to distinguish whether or not the opposite edges in diagrams such as (1) represent the same action. Intuitively, this is achieved in both approaches by thinking of transitions as occurrences of events, two transitions representing the same event if they correspond to the same action. However, the differences induced on the models by the different choices of how to assign events to transitions are definitely not trivial. And so are the relationships that these models bear to each other.

Getting to the details, asynchronous transition systems assign events to transitions explicitly and enrich the structure further by adding an independence relation on the events which describes their causal relationships. This clearly makes distinguishing nondeterminism and concurrency possible; a.b+b.a and a|b can be represented respectively by, e.g., the following labelled asynchronous transition systems, where ∼ indicates whether or not the events e and e′ (labelled by a and b) are independent.

[figure: •; •; ^{b}e′; •; e^{a}; •; ^{a}e; _{e′_{b}}; •; •; ^{b}e′; ∼; •; e^{a}; •; ^{a}e; _{e′_{b}}]

Observe that here and in the rest of the paper we consider labelled asynchronous transition systems [1, 21], i.e., asynchronous transition systems with a further labelling of events, as the proper extension of labelled transition systems.

2

The expressive power of asynchronous transition systems is clearly not limited to the example above; for instance, Bednarczyk [1] and Mukund and Nielsen [14] have shown that noninterleaving related issues for CCS processes—such as localities—can be modelled faithfully using this model. However, it can be argued that assigning both the independence relation and the decoration of transitions with events explicitly means assigning too much. In fact, this obviously introduces some redundancies in the model: there are, for instance, many non-isomorphic variations of the asynchronous transitions systems above which can still be reasonably thought as models of a|b and a.b + b.a. Moreover, although it is usually easy to tell about independence of transitions, in many important cases it is at least not immediate to assign events to transitions: it might very well be the goal of the entire semantic analysis to understand what the events of the system and their mutual relationships are. This consideration seems to indicate that asynchronous transitions systems cannot have a significant impact in Plotkin’s SOS style semantics, unless the independence relation is promoted to a greater role.

Transition systems with independence are an attempt to answer to the previous observation. Here events are not introduced explicitly. They are rather derived from the structure of the ‘simply-labelled’ transitions, upon which the independence relation is directly layered. In such a model, each of the CCS terms discussed above admits only one transition system which can faithfully represent it, viz., respectively,

[figure: •; •; b; •; a; •; a; b; •; •; b; ∼; •; a; •; a; b]

The implicit information about events can be easily deduced from the presence (or the absence) of ∼, making the achieved expressive power comparable to that of asynchronous transition systems. Moreover, avoiding a primitive notion of event makes providing a ‘noninterleaving’ operational semantics in the SOS style a relatively simple task (cf. [21]).

However, in order to be consistent with the computational intuition, the axiomatics of transition systems with independence involves (apparently necessarily [18]) one condition expressed ‘globally’ in terms of all the transitions representing occurrences of the same event. This contrasts with the ‘local’ conditions defining asynchronous transition systems and can make hard checking that a given structure is a transitions system with independence. Thus, the differences induced on the two models by the choice of a primitive versus a derived notion of event are far-reaching and seem to make them suitable for different applications. This indicates that it is not wise to choose once and for all between asynchronous transition systems and transition systems with independence, which, in turn, opens the issue of investigating formally their analogies and differences. The contribution of this paper is to answer exhaustively such

3

a question, which, actually, escaped the thorough analysis of models for concurrency carried out in [21, 15, 18]. Precisely, we prove that transition systems with independence besides being nicely related to a class of asynchronous transition systems that we call extensional, are equivalent to the so-called event-maximal asynchronous transition systems. These latter can be seen at the same time as those transition systems that make as few identifications of transitions as possible, i.e., contain no confusion about event identities, and as those in which such identities are derivable from the independence relation, i.e., reduce the redundancy. It is worth mentioning that the converse does not hold: the asynchronous transitions systems for which the independence relation is in turn derivable from the structure of events, and therefore redundant, are slightly less general. They correspond to the transitions systems with independence for which ‘independence is concurrency’ considered in [15, 18].

Concerning the organization of the paper and its technical contributions, after recalling in Section 1 the definitions of LATS and TSI, respectively the categories of labelled asynchronous transitions systems and of transitions systems with independence, in Section 2 we look for a functor adjoint to the obvious embedding TSI ↪ LATS. In particular, we identify the category of extensional asynchronous transitions systems, eLATS, as the largest subcategory of LATS which admits TSI as a coreflective subcategory. It is worth noticing here that at : eLATS → TSI, the right adjoint of the coreflection, complements and corrects a non-well-defined construction sketched in [21]: as a matter of fact, due to the greater generality of asynchronous transition systems, eLATS happens to be the largest subcategory of LATS on which such a construction makes sense. Finally, Section 3 introduces event-maximal asynchronous transitions systems and their category meLATS, providing the proof of the equivalence TSI ≅ meLATS. This yields a complete description of TSI in terms of LATS which can be useful in practise to translate back and forth between the two models when the application one has in mind requires it.

Summing up our results, this paper presents the following commutative diagram, which makes completely formal and precise the relationships between transition systems with independence and asynchronous transition systems.

[figure: TSI; ≅; LATS; meLATS; eLATS; at; ⊥]

1 Preliminaries

In this section we recall briefly the definitions of asynchronous transition systems, transition systems with independence, and their respective categories [1, 21].

As discussed in the introduction, asynchronous transition systems are simply transition systems whose transitions are decorated by events equipped with an independence relation. Four axioms (A1–A4) are needed to guarantee the intended meaning for the events and the independence relation.

4

Definition 1.1 (Labelled Asynchronous Transition Systems) A labelled asynchronous transition system (lats for short) is a structure

A = (S_{A}, i_{A}, E_{A}, Tran_{A}, I_{A}, L_{A}, ℓ_{A}),

where (S_{A}, i_{A}, E_{A}, Tran_{A}) is a transition system with set of states S_{A}, initial state i_{A} ∈ S_{A}, and transitions Tran_{A} ⊆ S_{A} × E_{A} × S_{A}, and where E_{A} is a set of events, L_{A} a set of labels, ℓ_{A}: E_{A} → L_{A} a labelling function, and I_{A} ⊆ E_{A} ×E_{A}, the independence relation, is an irreflexive, symmetric relation such that

A1. e ∈ E_{A} ⇒ ∃s_{1}, s_{2} ∈ S_{A}. (s_{1}, e, s_{2}) ∈ Tran_{A};

A2. (s, e, s_{1}), (s, e, s_{2}) ∈ Tran_{A} ⇒ s_{1} = s_{2};

A3. e_{1} I_{A} e_{2} & (s, e_{1}, s_{1}), (s, e_{2}, s_{2}) ∈ Tran_{A} ⇒

∃u. (s_{1}, e_{2}, u), (s_{2}, e_{1}, u) ∈ Tran_{A};

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

A4. e_{1} I_{A} e_{2} & (s, e_{1}, s_{1}), (s_{1}, e_{2}, u) ∈ Tran_{A} ⇒

∃s_{2}. (s, e_{2}, s_{2}), (s_{2}, e_{1}, u) ∈ Tran_{A}.

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

In the rest of the paper we shall let I(e) denote the set {e′ | e I_{A} e′} and, for convenience, use (s, e^{a}, s′) as a shorthand for a transition (s, e, s′) with ℓ_{A}(e) = a.

The following is the standard definition of morphisms for lats, which essentially captures the idea of simulation (cf. [1, 21]).

Definition 1.2 (Asynchronous Transition System Morphisms) For A and A′ lats, a morphism from A to A′ is a triple of (partial) functions^{1} (σ: S_{A} → S_{A′}, η: E_{A} ⇀ E_{A′}, λ: L_{A} ⇀ L_{A′}), where (σ, η) is a morphism of labelled transition systems, i.e.,

▷ σ(i_{A}) = i_{A′};

▷ (s_{1}, e, s_{2}) ∈ Tran_{A} & η(e)↓ ⇒ (σ(s_{1}), η(e), σ(s_{2})) ∈ Tran_{A′}; (s_{1}, e, s_{2}) ∈ Tran_{A} & η(e)↑ ⇒ σ(s_{1}) = σ(s_{2});

which preserves the labelling, i.e., makes the following diagram commutative

[figure: E_{A}; η; ℓ_{A}; E_{A′}; ℓ_{A′}; L_{A}; λ; L_{A′};]

and the independence, i.e.,

e_{1} I_{A} e_{2} & η(e_{1})↓, η(e_{2})↓ ⇒ η(e_{1}) I_{A′} η(e_{2}).
5

1We use, respectively, f: A → B and f: A ⇀ B to indicate total and partial functions. For f a partial function, f(x)↓ (f(x)↑) means that f is (un)defined at x.

It is immediate to see that lats and their morphisms form a category, which we shall refer as LATS.

Starting from Definition 1.1, transition systems with independence attempt to simplify the structure retaining explicitly only the independence, now layered directly on the transitions. As already mentioned, the notion of event becomes implicit, determined by the independence relation through the equivalence ∼.

Definition 1.3 (Transition Systems with Independence) A transition system with independence (tsi for short) is a structure

T = (S_{T} , i_{T} , L_{T} , Tran_{T} , I_{T}),

where (S_{T} , i_{T} , L_{T} , Tran_{T}) is a transition system and I_{T} ⊆ Tran_{T} × Tran_{T}, the independence relation, is an irreflexive, symmetric relation, such that, denoting by ≺ the binary relation on transitions given as

(s, a, s_{1}) ≺ (s_{2}, a, u) ⇔
∃b ∈ L_{T} . (s, a, s_{1}) I_{T} (s, b, s_{2}) &
(s, a, s_{1}) I_{T} (s_{1}, b, u) & (s, b, s_{2}) I_{T} (s_{2}, a, u)

and by ∼ the least equivalence on transitions which includes it, we have

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

T2. (s, a, s_{1}) I_{T} (s, b, s_{2}) ⇒ ∃u. (s, a, s_{1}) I_{T} (s_{1}, b, u) & (s, b, s_{2}) I_{T} (s_{2}, a, u);

T3. (s, a, s_{1}) I_{T} (s_{1}, b, u) ⇒ ∃s_{2}. (s, a, s_{1}) I_{T} (s, b, s_{2}) & (s, b, s_{2}) I_{T} (s_{2}, a, u);

T4. (s, a, s_{1}) ≺ ∪ ≻ (s_{2}, a, u) I_{T} (w, b, w′) ⇒ (s, a, s_{1}) I_{T} (w, b, w′).

The ∼-equivalence classes, in the following denoted by [(s, a, s′)], for (s, a, s′) a representative of the class, are to be thought of as events, i.e., t_{1} ≺ t_{2} means that t_{1} and t_{2} are part of a ‘concurrency diamond’, whilst t_{1} ∼ t_{2} means that they are occurrences of the same event. Concerning the axioms, notice then that T1 (the global condition mentioned earlier) corresponds to A2 and axioms T2 and T3 correspond, respectively, to A3 and A4. The role of T4 is to ensure that the independence relation is actually well defined as a relation on events. In the rest of the paper we shall see that this view of [(s, a, s′)] agrees with the notion of events for lats and that, in fact, it identifies an interesting subclass of them.

Using I(t) to denote the set {t′ | t I_{T} t′}, we can state the following lemma which will be useful later on. As a matter of notations, we shall use π_{i} to denote projections, i.e., if t is (s, a, s′), then π_{1}(t) = s, π_{2}(t) = a and π_{3}(t) = s′.

Lemma 1.4 Axiom T4 is equivalent to

t_{1} ∼ t_{2} ⇒ I(t_{1}) = I(t_{2}).  (T4′)

Proof. Easy, by induction. ✓

6

The following definition of morphisms for transition systems with independence resembles closely that given earlier for lats.

Definition 1.5 (Transition System with Independence Morphisms) For T and T′ tsi, a morphism from T to T′ consists of a pair of (partial) functions (σ: S_{T} → S_{T′}, λ: L_{T} ⇀ L_{T′}) which is a morphism of transition systems and, in addition, preserves independence, i.e.,

\begin{matrix}(s_{1}, a, s_{2}) I_{T} (s′_{1}, b, s′_{2}) & λ(a)↓, λ(b)↓ ⇒ \\ (σ(s_{1}), λ(a), σ(s_{2})) I_{T′} (σ(s′_{1}), λ(b), σ(s′_{2})). \end{matrix}

We shall use TSI to denote the category of tsi and their morphisms.

The following lemma states that tsi morphisms are well defined as maps of events, an easy consequence of the fact that they preserve independence that we shall use in order to embed TSI into LATS.

Lemma 1.6 (Morphisms map Events to Events) For (σ, λ): T → T′ a morphism of tsi and (s_{1}, a, s_{2}) ∼ (s′_{1}, a, s′_{2}) equivalent transitions of T, if λ(a)↓, then (σ(s_{1}), λ(a), σ(s_{2})) ∼ (σ(s′_{1}), λ(a), σ(s′_{2})), i.e., lats morphisms preserve ∼.

2 From LATS to TSI: a coreflection

The scene is now set to expose the adjunction between TSI and a full subcategory of LATS. First, we define an inclusion ta : TSI ↪ LATS in the obvious way.

On the objects, ta acts by decorating each transition with the event identified by the ∼-class the transition belongs to. The label of such an event is, of course, the label originally carried in the tsi by the transition. Observe that, in force of Definition 1.3 of ∼, this labelling is well defined. Finally, the independence relation of ta(T) is inherited directly from the one of T. The formal definition is as follows.

Definition 2.1 (TSI ↪ LATS) For T a tsi, let ta(T) be the structure (S_{T} , i_{T} , E, Tran, I, L_{T} , ℓ), where, denoting by ∼ the equivalence relation induced by I_{T} as in Definition 1.3,

▷ E = Tran_{T} /∼, the set of ∼-classes of Tran_{T};

▷ Tran = {(s_{1}, [(s_{1}, a, s_{2})], s_{2}) | (s_{1}, a, s_{2}) ∈ Tran_{T} };

▷ [(s_{1}, a, s_{2})] I [(s′_{1}, a, s′_{2})] if and only if (s_{1}, a, s_{2}) I_{T} (s′_{1}, a, s′_{2});

▷ ℓ([(s_{1}, a, s_{2})]) = a.

It follows from Lemma 1.4 that the definition of the independence on the events of ta(T) is well given. It is now easy to verify the following.

Proposition 2.2 The transition system ta(T) is a lats.

7

Proof. Axiom A1 is trivially satisfied. Axiom A2 is satisfied because of T1, for, by definition of ta, two transitions carry the same event if and only if they belong to the same ∼-class in T. Concerning A3 and A4, they correspond directly to T2 and T3. ✓

In order to define ta as a functor, we need to assign its action on the morphisms in TSI.

Definition 2.3 (TSI ↪ LATS) For (σ, λ): T → T′ a morphism of tsi, let ta((σ, λ)) be (σ, η, λ), where

η([(s, a, s′)]) = \begin{cases}[(σ(s), λ(a), σ(s′))] & if λ(a)↓, \\ undefined & if λ(a)↑. \end{cases}

That Definition 2.3 is well given follows from Lemma 1.6; it is then easy to check that ta is a full and faithful functor, i.e., an embedding of TSI in LATS.

The obvious idea for a map at left inverse to ta, as hinted also in [21], is to forget the events and bring the independence from the events down to the transitions, i.e., for A a lats, to take at(A) to be (S_{A}, i_{A}, L_{A}, Tran, I), where

▷ (s, a, s′) ∈ Tran if and only if (s, e^{a}, s′) ∈ Tran_{A},

▷ (s, a, s_{1}) I (s_{2}, b, s_{3}) if and only if (s, e_{1}^{a}, s_{1}), (s_{2}, e_{2}^{b}, s_{3}) ∈ Tran_{A} & e_{1} I_{A} e_{2}.

This construction, however, contrarily to the claims of [21], is not well defined on the whole LATS, since the interplay between the explicitly given independence and events in lats allows rather complicated situations—of dubious computational significance—which cannot be expressed with tsi. A counterexample is illustrated by the following lats.

The independent events are e I_{A} e_{1}, [figure: v; u; s_{3}; e_{1}^{b}; s_{1}; e_{1}^{b}; e_{2}^{b}; s_{1}; e^{a}; e_{3}^{a}; s_{4}; e^{a}; s; e_{3}^{a}; e^{a}; e_{2}^{b}; e_{1}^{b}]

e_{3} I_{A} e_{1}, e I_{A} e_{2}, and e_{2} I_{A} e_{3}, i.e., the system consists of three independency diamonds ‘on top of each other’. It is easy to check that this is an object of LATS. However, by applying at we create a ‘ghost’ independency diamond (the one highlighted by the dotted lines), so violating condition T1. In fact, (s, a, s_{3}) ∼ (s, a, s_{1}) with s_{1} ≠ s_{3}. This demonstrates that the combi-

nation of independence and events makes it hard to define ‘uniformly’ a map from LATS to TSI to act as left inverse to ta : TSI ↪ LATS.

However, it is not hard to check that things go smoothly for those lats belonging to the image of ta. In such a case, at lands in TSI and, of course, we have the following result.

Lemma 2.4 For any T in TSI, we have at ∘ ta(T) = T.

8

At this point, the issue arises of identifying suitable conditions which, imposed on lats, constrain them down to a category which bears good relationships with TSI. Possibly, one should also like to find a nice characterisation of the image of ta in LATS. We shall do so next, by focusing on extensional asynchronous transition systems.

We start by considering lats A satisfying

(s_{1}, e_{1}^{a}, s_{2}) ≠ (s_{1}, e_{2}^{b}, s_{2}) ∈ Tran_{A} ⇒ a ≠ b.  (Ex)

In words, these are lats where no two transitions between the same states can carry the same label. This is a kind of extensionality condition that, in view of Definition 1.3, is clearly necessary for our purposes. In fact, without (Ex), the one-to-one correspondence between morphisms of the kinds ta(T) → A and T → at(A)—required by the adjointness conditions—would not exist. Next, we let the counterexample discussed above guide us to identify two simple additional conditions—strengthening A3 and A4 with uniqueness criteria—that we shall prove to be necessary and sufficient in order for at to be well defined on lats satisfying (Ex). As a notation, for (s, e^{a}, s′) ∈ Tran_{A}, we shall use at(s, e^{a}, s′) to refer to the (unique) transition (s, a, s′) ∈ Tran_{at(A)} it corresponds to.

Proposition 2.5 For A a lats satisfying (Ex), at(A) belongs to TSI if and only if

i) for e_{1} I_{A} e_{2} and (s, e_{1}^{a}, s_{1}), (s, e_{2}^{b}, s_{2}) ∈ Tran_{A}, there exists a unique pair (s_{1}, x_{2}^{b}, u), (s_{2}, x_{1}^{a}, u) ∈ Tran_{A} such that e_{1} I_{A} x_{2}, e_{2} I_{A} x_{1}, and x_{1} I_{A} x_{2}.

ii) for e_{1} I_{A} e_{2} and (s, e_{1}^{a}, s_{1}), (s_{1}, e_{2}^{b}, u) ∈ Tran_{A}, there exists a unique pair (s, x_{2}^{b}, s_{2}), (s_{2}, x_{1}^{a}, u) ∈ Tran_{A} such that e_{1} I_{A} x_{2}, e_{2} I_{A} x_{1}, and x_{1} I_{A} x_{2}.

Proof. If at(A) ∈ TSI, the pairs of transitions in i) and ii) exist because of axioms A3 and A4. Their uniqueness is needed in order for at(A) to satisfy axiom T1. Suppose that, on the contrary, in case ii) there are two pairs (s_{1}, x_{2}^{b}, u), (s_{2}, x_{1}^{a}, u) and (s_{1}, y_{2}^{b}, w), (s_{2}, y_{1}^{a}, w) satisfying the condition. Since A satisfies (Ex), we have w ≠ u, which implies that at(s, e_{2}^{b}, s_{2}) ≺ at(s_{1}, y_{2}^{b}, w) and at(s, e_{2}^{b}, s_{2}) ≺ at(s_{1}, x_{2}^{b}, u), i.e., that at(s_{1}, x_{2}^{b}, u) ∼ at(s_{1}, y_{2}^{b}, w), which contradicts T1. The case for ii) can be proved along the same lines, thus showing the necessity of the conditions.

Concerning their sufficiency, the extensionality guarantees that I_{at(A)} is irreflexive, whilst the property of symmetry for I_{at(A)} is inherited from I_{A}. It remains check that the axioms T1–T4 defining tsi hold for at(A). Axioms A3, A4 and conditions i) and ii) above ensure that if at(t) ≺ at(t′), then π_{2}(t) = π_{2}(t′), i.e., t and t′ represent the same event. It follows then by induction that at(t) ∼ at(t′) implies π_{2}(t) = π_{2}(t′), for all at(t), at(t′) ∈ Tran_{at(A)}. If in addition π_{1}(at(t)) = π_{1}(at(t′)), then also π_{1}(t) = π_{1}(t′) and axiom A2 implies that π_{3}(at(t)) = π_{3}(at(t′)). So T1 is satisfied. Actually, this also implies that T4 holds. For, since the independence in at(A) is inherited from that on the events in A, and t and t′ carry the same event, we have that at(t) ∼ at(t′) implies I(at(t)) = I(at(t′)). This, as proved by Lemma 1.4, is equivalent to T4. Finally, T2 and T3 hold because of the corresponding A3 and A4. ✓

9

We call extensional the lats satisfying (Ex) and the conditions of Proposition 2.5, and we denote by eLATS the full subcategory of LATS they determine.

Clearly, at can be extended to a functor from eLATS to TSI which simply ‘forgets’ the event component of LATS morphisms, i.e., for (σ, η, λ): A → A′, take at((σ, η, λ)) to be (σ, λ). We shall see next that such a functor is right adjoint to ta : TSI ↪ eLATS.

Proposition 2.6 (ta ⊣ at : TSI ⇀ eLATS) For any A ∈ eLATS and any morphism m: T → at(A) in TSI, there exists a unique morphism m^{T} : ta(T) → A such that at(m^{T}) = m.

Proof. Let m be (σ, λ). Clearly, by definition of at, m^{T} must be of the form (σ, γ, λ) for some γ: E_{ta(T)} → E_{A}. It is easy to realize that the only possible choice for γ is the following: for (s, a, s′) ∈ Tran_{T} and λ(a)↓, let γ([(s, a, s′)]) be the event e ∈ E_{A} of the unique transition (σ(s), e^{λ(a)}, σ(s′)) ∈ Tran_{A}. This is a well given definition, for Lemma 1.6 ensures that m maps all transitions in [(s, a, s′)] to the same ∼-class of Tran_{at(A)}, and the proof of Proposition 2.5 shows that if two transitions belong to the same ∼-class of Tran_{at(A)}, they originate from transitions in Tran_{A} carrying the same event. This proves both existence and uniqueness of m^{T}. ✓

Proposition 2.6 proves that the identity natural transformation

η = {id_{T} : T → at ∘ ta(T)}_{T ∈TSI}

is the unit of an adjunction involving ta and at. Moreover, since η is an isomorphism, by standard results in category theory, we have that the adjunction ta ⊣ at : TSI ⇀ eLATS is a coreflection, i.e., TSI is coreflective in eLATS. This, together with Proposition 2.5 and the discussion at the beginning of the present section, shows that eLATS is the largest subcategory of LATS on which at can be defined as a functor to TSI, yielding a right adjoint to ta.

3 meLATS: A category of LATS equivalent to TSI

In this section we identify the replete image of ta in LATS, i.e., the full subcategory meLATS of eLATS consisting of the objects isomorphic to ta(T), for some T ∈ TSI. In addition, we characterise those lats for which the independence can be recovered from the structure of events, and relate them to a relevant subcategory of TSI considered in [15, 18].

Recall from basic category theory that meLATS is determined by the coreflection: it consists of those A ∈ eLATS for which the corresponding component ϵ_{A} of the counit of ta ⊣ at is iso. Applying standard categorical results to derive ϵ from (−)^{T} and η, we find that it is the natural transformation

ϵ = {(id_{S_{A}}, γ, id_{L_{A}}): ta ∘ at(A) → A}_{A∈eLATS},

where for (s, a, s′) ∈ Tran_{at(A)}, γ([(s, a, s′)]) =_{def} e, for e ∈ E_{A} the event of the unique (s, e^{a}, s′) ∈ Tran_{A}. Clearly, ϵ_{A} is iso if and only if γ is such, i.e.,

∀t, t′ ∈ Tran_{A}, π_{2}(t) = π_{2}(t′) ⇒ at(t) ∼ at(t′),
10

which means that two transitions carry the same event if and only if they belong to the same ∼-class of A (viewed as a tsi). Although this characterises meLATS ⊂ LATS equivalent to TSI, it would of course be better to find a more direct description of it, one not referring to at(A). This is the purpose of the notion of event-maximal asynchronous transitions systems introduced next.

Intuitively, a lats is event-maximal if its events and independence are ‘tightly coupled’, so that one cannot ‘split’ events without destroying the global lats structure. More precisely, A is event-maximal if for any ē ∈ E_{A} and any subset T of transitions carrying ē, the structure resulting from replacing ē on the transitions in T by a fresh event ẽ is no longer a lats.

Definition 3.1 (Event-Maximal Asynchronous Transition Systems) For A a LATS, ē ∈ E_{A}, and T ⊂ Tē = {t ∈ Tran_{A} | π_{2}(t) = ē}, let A[T] denote the replacement of ē on the transitions in T for a fresh event ẽ ∉ E_{A}, i.e., A[T] = (S_{A}, i_{A}, E_{A} ∪ {ẽ}, Tran, I, L_{A}, ℓ), where

▷ Tran = (Tran_{A} ∖ T ) ∪ {(s_{1}, ẽ, s_{2}) | (s_{1}, ē, s_{2}) ∈ T };

▷ I = I_{A} ∪ {(ẽ, e) | ē I_{A} e};

▷ ℓ(e) = \begin{cases}ℓ_{A}(e) & if e ∈ E_{A}, \\ ℓ_{A}(ē) & if e = ẽ. \end{cases}

A lats A is event-maximal if for each ē ∈ E_{A} and each nonempty T ⊂ Tē, the transition systems A[T] is not a lats. The category meLATS is the full subcategory of LATS consisting of the extensional, event-maximal lats.

Observe that the interesting, nontrivial choices for T are those such that ∅ ⊂ T ⊂ Tē, i.e., those in which at least one ẽ-transition is added and at least one ē-transition is kept in A[T]. The definition above, stating that any such structure must fail to be a lats, is our way to express that—as remarked in the introduction—the identity of the events in event-maximal lats is forced by the independence relation. This provides us with the direct characterisation of TSI in terms of LATS that we sought.

Proposition 3.2 (meLATS ≅ TSI) meLATS is equivalent to TSI.

Proof. Let A be an extensional lats. We prove that the counit ϵ_{A} is iso if and only if A belongs to meLATS. To this purpose, let γ be the event component of ϵ_{A}. If γ is iso, i.e., for all t, t′ ∈ Tran_{A} we have that π_{2}(t) = π_{2}(t′) implies at(t) ∼ at(t′), for any choice of ē ∈ E_{A} and any ∅ ⊂ T ⊂ Tē, then the condition in Definition 3.1 is satisfied, since, by the extensionality of A, either A3 or A4 must fail for A[T]. In fact, in order for A[T] to be a LATS, extensionality implies that t′ ∈ T whenever a at(t′) ∼ at(t) for some t ∈ T, i.e., by the hypothesis on γ, T should be Tē. So A is event-maximal.

11

If γ is not iso, i.e., if there exist t and t′ such that which at(t) ≁ at(t′) but π_{2}(t) = π_{2}(t′), then T = {t′′ | at(t′′) ∼ at(t)} ⊂ T_{π_{2}(t)} is a nonempty set for which the ‘splitting’ of π_{2}(t) yields a lats, i.e., A is not event-maximal. ✓

To conclude this exposition, we observe that the independence relation in event-maximal lats is not uniquely determined by rest of the structure. This is due to the fact that the independence on events is still rather intensional notion: events may be independent and still never occur in the same path, i.e., intuitively, be mutually exclusive. Observing that such situations have little computational relevance, one may consider on lats the property

e_{1} I_{A} e_{2} ⇒ ∃(s, e_{1}, s_{1}), (s, e_{2}, s_{2}) ∈ Tran_{A},  (E)

which can be seen as an extensionality condition on I_{A}. It is easy to prove that, if A ∈ meLATS satisfies (E), then e_{1} I_{A} e_{2} if and only if there exists a square in A involving e_{1} and e_{2}, i.e.,

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

Thus, for such lats the independence is completely redundant and can be omitted: all the information is already contained in (S_{A}, i_{A}, E_{A}, Tran_{A}, L_{A}, ℓ_{A}).

It is worth remarking here that a condition corresponding to (E) for TSI— viz., whenever t I_{T} t′, there exist (s, a, s′) ∼ t and (s, b, s′′) ∼ t′ in Tran_{T} —was identified in [15, 18] while investigating the tight relationships between tsi and event structures. Such a condition yields TSI_{E}, a very good-behaved full subcategory of TSI for which we can state the following corollary of Proposition 3.2, which concludes the paper. Here we use meLATS_{E} to denote the full subcategory of meLATS consisting of the structures satisfying (E).

Proposition 3.3 ( meLATS_{E} ≅ TSI_{E}) meLATS_{E} is equivalent to TSI_{E}.

References

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

[2] J.M.C. Baeten and W.P. Weijland. Process Algebra Cambridge Tracts in Theoretical Computer Science, 18 (1990), Cambridge University Press.

[3] G-L. Cattani and V. Sassone. Higher Dimensional Transition Systems, To appear in Proceedings of LICS 96 (1996), IEEE Computer Society Press.

[4] R. van Glabbeek. Bisimulations for higher dimensional automata, email message sent to the Concurrency mailing list on July 7, 1991. Available at

    http://theory.stanford.edu/people/rvg/hda.

12

[5] R. van Glabbeek and G. Plotkin. Configuration Structures. In Proceedings of LICS’95, D. Kozen (Ed.), IEEE Computer Society Press (1995), 99–109.

[6] E. Goubault. Domains of Higher-Dimensional Automata. In Proceedings of CONCUR’93, E. Best (Ed.), LNCS 715 (1993), Springer-Verlag, 293–307.

[7] E. Goubault and T. Jensen. Homology of Higher-Dimensional Automata. In Proceedings of CONCUR’92, W.R. Cleaveland (Ed.), LNCS 630 (1992), Springer-Verlag, 254–268.

[8] P. Godefroid and P. Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, In Proceedings of CAV’91, K.G. Larsen et al. (Eds.), LNCS 575 (1991), Springer-Verlag, 332–342.

[9] M. Hennessy. Algebraic Theory of Processes. Series in the Foundations of Computing (1988), The MIT Press.

[10] C.A.R. Hoare. Communicating Sequential Processes. Series in Computer Science (1985), Prentice-Hall.

[11] R. Milner. Communication and Concurrency. Series in Computer Science (1989), Prentice Hall.

[12] R. Milner. The polyadic π-calculus: a tutorial. In Logic and Algebra of Specification, F.L. Bauer et al. (Eds.), Springer-Verlag, (1993).

[13] M. Mukund. Petri Nets and Step Transition Systems. International Journal of Foundations of Computer Science, vol. 3, n. 4 (1992), 443–478.

[14] M. Mukund and M. Nielsen. CCS, Locations and Asynchronous Transition Systems In Proceedings of FST & TCS’92, R. Shyamasundar (Ed.), LNCS n. 652 (1992), Springer-Verlag, 328–341.

[15] M. Nielsen, V. Sassone and G. Winskel. Relationships between Models of Concurrency, In Proceedings of REX’93. A Decade of Concurrency: Reflections and Perspectives, LNCS n. 803, (1994), J.W. de Bakker et al. (Eds.), Springer-Verlag, 425–476.

[16] D. Peled. All from One, One for All: On Model Checking Using Representatives, In Proceedings of CAV’93, C. Courcoubetis (Ed.), LNCS n. 697 (1993), Springer-Verlag, 409–423.

[17] V. Pratt. Modelling Concurrency with Geometry. In Proceedings of 18th ACM Symposium on Principles of Programming Languages, ACM Press, (1991), 311–322.

[18] V. Sassone, M. Nielsen, and G. Winskel. Models for Concurrency: Towards a Classification. To appear in Theoretical Computer Science. An extended abstract appears as ‘A Classification of Models for Concurrency’ in Proceedings of CONCUR’93, E. Best (Ed.), LNCS 715 (1993), Springer-Verlag, 82–96.

[19] M.W. Shields. Concurrent machines Theoretical Computer Science n .28 (1985), 449–465.

13

[20] A. Valmari. A Stubborn attack on state explosion, In Proceedings of CAV’90, DIMACS Series n. 3 (1991), 25–42.

[21] G. Winskel and M. Nielsen. Models for Concurrency In Handbook of Logic and the Foundations of Computer Science, vol. IV, S. Abramsky et al. (Eds.), Oxford University Press, 1995.

14

Recent Publications in the BRICS Report Series

RS-96-18 Thomas Troels Hildebrandt and Vladimiro Sassone. Comparing Transition Systems with Independence and Asynchronous Transition Systems. June 1996. 14 pp. To appear inConcurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS, 1996.

RS-96-17 Olivier Danvy, Karoline Malmkj�r, and Jens Palsberg. Eta-Expansion Does The Trick (Revised Version). May 1996. 30 pp. To appear in ACM Transactions on Programming Languages and Systems (TOPLAS).

RS-96-16 Lisbeth Fajstrup and Martin Rau�en. Detecting Deadlocks in Concurrent Systems. May 1996. 10 pp.

RS-96-15 Olivier Danvy. Pragmatic Aspects of Type-Directed Partial Evaluation. May 1996. 27 pp.

RS-96-14 Olivier Danvy and Karoline Malmkj�r. On the Idempotence of the CPS Transformation. May 1996. 15 pp.

RS-96-13 Olivier Danvy and Ren� e Vestergaard. Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation. May 1996. 28 pp.

RS-96-12 Lars Arge, Darren E. Vengroff, and Jeffrey S. Vitter. External-Memory Algorithms for Processing Line Segments in Geographic Information Systems. May 1996. 34 pp. An shorter version of this paper was presented at the Third Annual European Symposium on Algorithms, ESA ’95.

RS-96-11 Devdatt Dubhashi, David A. Grable, and Alessandro Panconesi. Near-Optimal, Distributed Edge Colouring via the Nibble Method. May 1996. 17 pp. Invited to be published in in a special issue of Theoretical Computer Science devoted to the proceedings of ESA ’95.

RS-96-10 Torben Bra� uner and Valeria de Paiva. Cut-Elimination for Full Intuitionistic Linear Logic. April 1996. 27 pp. Also available as Technical Report 395, Computer Laboratory, University of Cambridge.