BRICS RS-97-10 Hildebrandt & Sassone: Transition Systems with Independence and Multi-Arcs BRICS

Basic Research in Computer Science

Transition Systems with Independence and Multi-Arcs

Thomas Troels Hildebrandt Vladimiro Sassone BRICS Report Series RS-97-10 ISSN 0909-0878 April 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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 BRICS Report Series publications. 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 the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/10/

Transition Systems with Independence and Multi-Arcs

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

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

Abstract

We extend the model of transition systems with independence in order to provide it with a feature relevant in the noninterleaving analysis of concurrent systems, namely multi-arcs. Moreover, we study the relationships between the category of transition systems with independence and multi-arcs and the category of labeled asynchronous transition systems, extending the results recently obtained by the authors for (simple) transition systems with independence (cf. Proc. CONCUR’96), and yielding a precise characterisation of transition systems with independence and multi-arcs in terms of (event-maximal, diamond-extensional) labeled asynchronous transition systems.

Introduction

Following the leading idea of CCS [12] and related process calculi [11, 2, 13, 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 labeled 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 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 [8] and liveness properties [21, 17].

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., [18, 4, 6, 7, 5, 3]). The present paper focuses on two such models, namely asynchronous transition systems, introduced independently by Bednarczyk [1] and Shields [20], and transitions systems with independence, proposed by Winskel and Nielsen [22]. 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 that 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 labeled asynchronous transition systems, where ∼ indicates whether or not the events e and e′(labeled 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 labeled asynchronous transition systems [1, 22], i.e., asynchronous transition systems with a further labeling of events, as the proper extension of labeled transition systems.

The expressive power of asynchronous transition systems is clearly not limited to the example above; for instance, Bednarczyk [1] and Mukund and Nielsen [15] have shown that noninterleaving related issues for CCS processes — such as localities — can be modeled 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 nonisomorphic 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-labeled’ 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. [22]).

However, in order to be consistent with the computational intuition, the axiomatics of transition systems with independence involves (apparently necessarily [19]) 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 (due to the globally identified events) 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.

An exhaustive analysis of this question was carried out by the authors in [10], showing that transition systems with independence, besides being nicely related to a class of asynchronous transition systems called extensional, are equivalent to the so-called event-maximal asynchronous transition systems. The results of loc. cit. are summarized by the following diagram, where TSI, LATS, eLATS, and meLATS are, respectively, the categories of transitions systems with independence, labeled, extensional, and event-maximal asynchronous transitions systems, and where ↪, ⊥, and ≅ stand respectively for embeddings, coreflections, and equivalences.

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

Essentially, the extensionality condition refers to the existence of a unique way to ‘complete’ pairs of independent transitions to ‘independence-diamonds’. Also, it excludes multi-arcs, i.e., multiple transitions with the same label between the same two states. Event-maximality, on the other hand, can be seen at the same time as identifying those transition systems that make as few identifications of transitions as possible, i.e., contain no confusion about event identities, and those in which such identities are derivable from the independence relation, i.e., reduce the redundancy. 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 [22]: 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.

A question left open by [10] is whether or not the need to restrict to extensional asynchronous transition systems is a consequence of the intrinsic differences between the two notions of events considered, i.e., if in order to be able to model situations ruled out by the extensionality constraints it is necessary to assign events explicitly. This paper addresses such a question; namely, we remove the restriction to transition systems without multi-arcs, relaxing the definition of transition systems with independence, and yielding the new notion of transition systems with independence and multi-arcs (nonextensional transition systems with independence would probably be a better name, though).

This represents, in our view, an interesting enhancement of the model. In fact, in noninterleaving semantics, to be able to treat multi-arcs is clearly very relevant. In a sense, it can be seen as allowing ‘quotienting’ of the state-space while retaining full information about events and causality. As an example, consider the CCS term (a|b) + a.b, traditionally described by the transition system below to the left. It is common (see e.g. [13, 15] among others) to quotient the state-space by some structural congruence that, e.g., collapses the states b and nil|b, obtaining the more compact representation — with multi-arcs — shown to the right.

[figure: a|nil; a; (a|b) + a.b; b; a; a; ∼; nil; nil|b; b; b; b; a|nil; a; (a|b) + a.b; b; a; a; ∼; nil; nil|b ≃ b; b]

Observe that, contrarily to the interleaving case, it is vital here to have two different a-transitions, since they rappresent different events: one is part of the independence-diamond and is, therefore, independent of b; the other is not.

In order to justify our definition, we prove that, except for the extensionality condition, the category TSI_{m} of transition systems with independence and multiarcs bears exactly the same relationships as TSI to LATS. More precisely, we prove that TSI_{m} is coreflective in the category dLATS of the diamond-extensional asynchronous transition systems — intuitively, those transition systems that make no confusion about the identities of the events carried by transitions facing each other in independence-diamonds. Similarly to the case of TSI, dLATS is the largest subcategory of LATS for which such a result holds. Moreover, among the diamond-extensional, we identify the event-maximal asynchronous transition systems and prove that they induce the largest full subcategory of LATS, mdLATS, for which the coreflection cuts down to an equivalence. This yields a precise characterisation of TSI_{m} in terms of LATS that extends the relationships between TSI and LATS discussed above: in fact, the category of eLATS and its full subcategory meLATS are, respectively, the full subcategories of dLATS and mdLATS consisting of transition systems without multi-arcs.

Summing up, this paper presents the following diagram of formal relationships between the new model of transition systems with independence and multi-arcs and asynchronous transition systems which can be useful in practise to translate back and forth between the two models when the application one has in mind requires it.

[figure: TSI_{m}; ≅; LATS; TSI; mdLATS; dLATS; am; ⊥; meLATS; eLATS; at; ⊥]

Although the technical development here goes along the lines of [10], and therefore, strictly speaking, this paper is simply an extension of loc. cit., we believe that the definition of TSI_{m} is a relevant contribution on its own.

1 Preliminaries

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

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.

Definition 1.1 (Labeled Asynchronous Transition Systems) A labeled 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 labeling 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 mimics the idea of simulation (cf. [1, 22]).

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 labeled 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 labeling, 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}).

It is immediate to see that lats and their morphisms form a category, which we shall refer to 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-classes of the relation ∼.

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}),

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.

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) if and only if
∃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 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 corresponds to A2 and axioms T2 and T3 correspond, respectively, to A3 and A4.

The following definition of morphisms for transition systems with independence resembles closely the one given above for lats.

Definition 1.4 (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.5 (Morphisms map Events to Events) For (σ,λ): T → T′a morphism of tsi, (s_{1},a,s_{2}) and (s′_{1},a,s′_{2}) transitions of T, (σ(s_{1}),λ(a),σ(s_{2})) ∼ (σ(s′_{1}),λ(a),σ(s′_{2})) whenever (s_{1},a,s_{2}) ∼ (s′_{1},a,s′_{2}) and λ(a)↓, i.e., lats morphisms preserve ∼.

2 Comparing LATS with TSI: Considering multi-arcs

In this section we first recall the results of the comparison of TSI and LATS carried out by the authors in [10], and then, reconsidering a restriction used in loc. cit., we introduce the notion of transition systems with independence and multi-arcs — i.e., tsi in which multiple transitions carrying the same label are allowed between the same two states. In the next section we shall then perform an analysis matching that of [10], investigating the relationship between such a category and LATS, and showing that, in a precise sense, our definition provides a minimal, conservative way to extend tsi with multi-arcs.

The starting point of the analysis in [10] is the obvious inclusion ta: TSI → LATS which acts on objects by decorating each transition with the event identified by the ∼-class the transition belongs to, and by inheriting the independence relation directly from the tsi. On the opposite direction, we considered the ‘abstraction’ at from LATS to TSI that forgets the events and brings the independence from the events down to the transitions. However, a simple argument shows that the presence of multi-arcs in LATS makes it impossible for at to be well-defined as a map to TSI. Thus, the very first step of [10] is to consider only those lats A satisfying

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

whose purpose is to forbids multi-arcs. This allows to prove that the diamondextensional asynchronous transition systems, whose definition follows, are exactly those lats A such that at(A) belongs to TSI.

Definition 2.1 (Diamond-Extensional lats) A diamond extensional labeled asynchronous transition system (dlats for short) is a lats that satisfies

A!3. e_{1} I_{A}e_{2}(s,e_{1}^{a},s_{1}),(s,e_{2}^{b},s_{2}) ∈ Tran_{A} ⇒ ∃! pair (s_{1},x_{2}^{b},u),(s_{2},x_{1}^{a},u) ∈ Tran_{A}. e_{1} I_{A}x_{2}e_{2} I_{A}x_{1}x_{1} I_{A}x_{2};

A!4. e_{1} I_{A}e_{2}(s,e_{1}^{a},s_{1}),(s_{1},e_{2}^{b},u) ∈ Tran_{A} ⇒ ∃! pair (s,x_{2}^{b},s_{2}),(s_{2},x_{1}^{a},u) ∈ Tran_{A}. e_{1} I_{A}x_{2}e_{2} I_{A}x_{1}x_{1} I_{A}x_{2}.

The category dLATS is the full subcategory of LATS consisting of the diamondextensional lats.

We call extensional the diamond-extensional lats that in addition satisfy (Ex), and we denote by eLATS the full subcategory of dLATS that they determine. We can now give the formal definitions of the functors ta: TSI → LATS and at: eLATS → TSI.

Definition 2.2 (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.

For (σ,λ): T → T′a morphism of tsi, let ta((σ,λ)) be (σ,η,λ), where

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

The proof that ta is well defined follows easily from Lemma 1.5. Actually, ta is a full and faithful functor, i.e., an embedding of TSI in LATS. In the following, when no confusion is possible, we may occasionally omit the index ∼ from the notation for ∼-classes.

Definition 2.3 (eLATS ↪ TSI) For A a lats, let at(A) be the structure

(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}.

For (σ,η,λ): A → A′a morphism of lats, let at((σ,η,λ)) be (σ,λ).

The result of [10] is that ta and at form a coreflection of TSI in eLATS.

Proposition 2.4 (ta ⊣ at: TSI ⇀ eLATS) TSI is coreflective in eLATS. Proof: Subsumed by that of the forthcoming Proposition 3.8. ✓

The lats corresponding to tsi are characterised as the event-maximal lats. 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. In other words, the identity of the events in event-maximal lats is forced by the independence relation. This will provide a direct characterisation of tsi in terms of lats Definition 2.5 (Event-Maximal lats) For A a lats, ē∈ E_{A}, and T ⊂ Tē, where Tē= {(s,e,s′) ∈ Tran_{A}| e = ē}, 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}∪ I_{T}∪ I_{T}^{−1} , I_{T} = {(ẽ,e) | ēI_{A}e};

▶ ℓ(e) = \{ \begin{matrix}ℓ_{A}(e) & ife ∈ E_{A}, \\ ℓ_{A}(ē) & ife = ẽ. \end{matrix}

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 mdLATS is the full subcategory of LATS consisting of the diamondextensional, event-maximal lats.

The definition above, stating that any structure obtained by ‘rearranging’ events non-trivially must fail to be a lats, is our way to express that — as remarked before — the identity of the events in event-maximal lats is forced by the independence relation.

Now, if we denote by meLATS the restriction of mdLATS to the full subcategory induced by the objects satisfying (Ex), we can state the final result of [10].

Proposition 2.6 (meLATS ≅ TSI) meLATS is equivalent to TSI. Proof: Subsumed by that of the forthcoming Proposition 3.9. ✓

Technically, the contribution of this paper is to re-address the choice of condition (Ex) which forbids multiple transitions with the same label between the same two states. Namely, instead of restricting lats in order to get a well-defined functor at to TSI, we relax the definition of tsi to allow multi-arcs, proposing below the notion of transition systems with independence and multi-arcs. This represents an interesting evolution of tsi, whose relevance goes beyond the comparison of tsi and lats; morally, it constitutes the main contribution of this paper. In other words, we propose here transition systems with independence and multi-arcs and justify their definition by showing how their multi-arcs relates to those of lats.

Formally, we extend tsi in the simplest possible way: transitions are represented by a map assigning to each element of a set Tran of transitions a triple consisting of its source, label, and target. This allows to have more transitions between the same two states with the same label simply by having more elements of Tran mapped to the same triple. The independence relation and the defining axioms are the obvious translations of those of tsi.

Definition 2.7 (tsi with Multi-Arcs) A transition system with independence and multi-arcs (tsi_{m} for short) is a structure

T = (S_{T},i_{T},L_{T},Tran_{T},⟨− ⟩_{T} ,I_{T}),

where ⟨− ⟩_{T} : Tran_{T} → S_{T}× L_{T}× S_{T} and (S_{T},i_{T},L_{T},⟨Tran_{T}⟩_{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

t ≺ t′ if and only if ⟨t⟩_{T} = (s,a,s_{1})⟨t′⟩_{T} = (s_{2},a,u)
∃t_{1},t_{2} ∈ Tran_{T}. ⟨t_{1}⟩_{T} = (s,b,s_{2})⟨t_{2}⟩_{T} = (s_{1},b,u)
witht I_{T} t_{1}t I_{T} t_{2}t_{1} I_{T} t′,

and by ∼ the least equivalence on transitions that includes ≺, we have

T_{m}1. t ∼ t′, ⟨t⟩_{T} = (s,a,s_{1}), ⟨t′⟩_{T} = (s,a,s_{2}) ⇒ t = t′;

T_{m}2. t I_{T} t′, ⟨t⟩_{T} = (s,a,s_{1}), ⟨t′⟩_{T} = (s,b,s_{2}) ⇒ ∃t_{1},t_{2}. ⟨t_{1}⟩_{T} = (s_{2},a,u)⟨t_{2}⟩_{T} = (s_{1},b,u)t I_{T} t_{2}t′I_{T} t_{1};

T_{m}3. t I_{T} t′, ⟨t⟩_{T} = (s,a,s_{1}), ⟨t′⟩_{T} = (s_{1},b,u) ⇒ ∃t_{1},t_{2}. ⟨t_{1}⟩_{T} = (s_{2},a,u)⟨t_{2}⟩_{T} = (s,b,s_{2})t I_{T} t_{2}t_{1} I_{T} t_{2};

T_{m}4. t ≺ ∪ ≻ t′I_{T} t′′ ⇒ t I_{T} t′′.

As for tsi, the ∼-equivalence classes — in the following denoted by [t]_{∼}, for t a representative of the class — are to be thought of as events. The axioms are recast to fit with the indirect way of assigning source, label, and target to transitions. Notice that a global axiom like T_{m}1 is still necessary, since the intended notion of events still cannot be determined locally. Axiom T_{m}4 ensures that the independence relation determines a well-defined relation on events.

In the rest of the paper we shall see that this view of [t]_{∼} agrees with the notion of events for lats and that, in fact, tsi_{m} relates well to the category of diamondextensional lats.

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}, i = 1,... ,3, to denote the composition of ⟨− ⟩_{T} with the appropriate projection, i.e., if ⟨t⟩_{T} = (s,a,s′), then ⟨t⟩_{1} = s, ⟨t⟩_{2} = a, and ⟨t⟩_{3} = s′.

Lemma 2.8 Axiom T_{m}4 is equivalent to

(T^{m}4′)  t_{1} ∼ t_{2} ⇒ I(t_{1}) = I(t_{2}).

Proof: Easy, by induction. ✓

The definition of morphisms for transition systems with independence and multi-arcs necessarily involves a (partial) function on transitions, which, of course, must respect the mapping of states and labels.

Definition 2.9 (tsi_{m} Morphisms) For T and T′ tsi_{m}, a morphism from T to T′ consists of a triple of (partial) functions

(σ: S_{T} → S_{T′},λ: L_{T} ⇀ L_{T′},τ: Tran_{T} ⇀ Tran_{T′})

that respects sources, targets, and labels, i.e., that makes the following diagram commute

[figure: T ran_{T}; τ; ⟨−⟩_{T}; T ran_{T′}; ⟨−⟩_{T′}; S_{T}× L_{T}× S_{T}; <σ,λ,σ>; S_{T′}× L_{T′}× S_{T′},]

preserves independence, i.e.,

t I_{T} t′τ(t)↓, τ(t′)↓ ⇒ τ(t) I_{T′}τ(t′),

and preserves the ‘diamond relation’ ⪯, i.e.,

t ⪯ t′τ(t)↓ (or τ(t′)↓) ⇒ τ(t) ⪯ τ(t′).

We shall use TSI_{m} to denote the category of tsi_{m} and their morphisms.

Observe that in the definition above it is necessary to consider the reflexive closure ⪯ of the relation ≺, since morphisms can be partial and, therefore, collapse diamonds.

Concerning the relationships between TSI and TSI_{m}, every tsi can be regarded as a tsi_{m} simply by defining the map ⟨− ⟩_{T} to act as the ‘identity’, i.e., interpreting transitions as themselves. Such a mapping extends to an inclusion functor tm: TSI ↪ TSI_{m} by defining tm((σ,λ)) to be (σ,λ,τ), where τ((s,a,s′)) = (σ(s),λ(a),σ(s′)). It follows immediately from the last condition in Definition 2.9 that τ is well defined as a map of events, a fact that we shall use in later on to embed TSI_{m} into LATS.

Lemma 2.10 (Morphisms map Events to Events) For (σ,λ,τ): T → T′a morphism of tsi_{m} and t ∼ t′equivalent transitions of T, if τ(t)↓, then τ(t) ∼ τ(t′), i.e., tsi_{m} morphisms preserve ∼.

In general, it is not possible to define a map from TSI_{m} to TSI that forgets multi-arcs and preserves independence. This is shown by the following example in which collapsing the a-multi-arcs would make the two a-labeled transitions sticking out of s break axiom T1

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

This means that the embedding tm: TSI ↪ TSI_{m} does not have a right adjoint. Dually, it can be proved that tm cannot have a left adjont either (a proof that we shall omit, though). Thus, TSI is neither reflective nor coreflective in TSI_{m}.

3 From LATS to TSI_{m}: A coreflection

Now that all the bricks are in play, we can complete the picture showing how to extend the functors ta and at to a pair of adjoint functors ma and am forming a coreflection between TSI_{m} and dLATS. There is only one reasonable way to define the embedding ma.

Definition 3.1 (TSI_{m} ↪ dLATS) For T a tsi, let ma(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 2.7,

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

▶ Tran = {(⟨t⟩_{1},[t]_{∼} ,⟨t⟩_{3}) | t ∈ Tran_{T}};

▶ [t]_{∼} I [t′]_{∼} if and only if t I_{T} t′;

▶ ℓ([t]_{∼} ) = ⟨t⟩_{2}.

It follows from Lemma 2.8 and the definition of ∼ that the definition of the independence and labels on the events of ma(T) is well given. It is now easy to verify the following.

Proposition 3.2 The transition system ma(T) is a dlats. Proof: Axiom A1 is trivially satisfied. Axiom A2 is satisfied because of T_{m}1, for, by definition of ma, 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 T_{m}2 and T_{m}3, and the uniqueness criteria imposed by A!3 and A!4 are a direct consequence of T1. ✓

In order to define ma as a functor, we need to define its action on the morphisms of TSI_{m}.

Definition 3.3 (TSI_{m} ↪ dLATS) For (σ,λ,τ): T → T′ a morphism of tsi_{m}, let ma((σ,λ,τ)) be (σ,η,λ), where

η([t]_{∼} ) = \{ \begin{matrix}[t′]_{∼} & ifτ(t) = t′, \\ undefined & ifτ(t)↑. \end{matrix}

That Definition 3.3 is well given follows from Lemma 2.10; it is also easy to check that ma is a full and faithful functor, i.e., an embedding of TSI_{m} in dLATS.

The obvious way to define the ‘abstraction’ am to TSI_{m} on the objects of LATS is, for a lats A, to make the transitions Tran_{A} the elements of the transition set Tran_{am(A)}and then interpret them (via ⟨− ⟩_{am(A)}) simply by replacing the event with its label. We shall prove that this gives a well-defined object-map from the category of diamond-extensional lats to TSI_{m}, and that dLATS is actually the largest full subcategory of LATS whose every object is mapped by am to a tsi_{m}.

Definition 3.4 (dLATS ↪ TSI_{m}) For A a lats, let am(A) be the structure

(S_{A},i_{A},L_{A},Tran,⟨− ⟩,I),

where,

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

▶ ⟨(s,e^{a},s′)⟩= (s,a,s′),

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

Proposition 3.5 For A a lats, am(A) belongs to TSI_{m} if and only if A belongs to dLATS. Proof: The pairs of transitions in A!3 and A!4 exist because of axioms A3 and A4. If am(A) ∈ TSI_{m}, their uniqueness is needed in order for am(A) to satisfy axiom T_{m}1. Suppose that, on the contrary, in the case of A!3 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. Assume, without loss of generality, that y_{2} ≠ x_{2}. Then we have (s_{1},y_{2}^{b},w) ≠ (s_{1},x_{2}^{b},u), but we also have that (s,e_{2}^{b},s_{2}) ≺ (s_{1},y_{2}^{b},w) (as transitions of am(A)) and (s,e_{2}^{b},s_{2}) ≺ (s_{1},x_{2}^{b},u), i.e., that (s_{1},x_{2}^{b},u) ∼ (s_{1},y_{2}^{b},w), which contradicts T_{m}1. The case for A!4 can be proved along the same lines, thus showing the necessity of the uniqueness conditions.

Concerning their sufficiency, the property of symmetry and irreflexivity for I_{am(A)}is inherited from I_{A}. It remains to check that the axioms T_{m}1–T_{m}4 defining tsi_{m} hold for am(A). Axioms A3, A4 and A!3, A!4 ensure that if (s,e_{1}^{a},s_{1}) ≺ (s_{2},e_{2}^{a},s_{3}), then e_{1} = e_{2}. It follows then by induction that (s,e_{1}^{a},s_{1}) ∼ (s_{2},e_{2}^{a},s_{3}) implies e_{1} = e_{2}, for all (s,e_{1}^{a},s_{1}),(s_{2},e_{2}^{a},s_{3}) ∈ Tran_{am(A)}. If in addition s = s_{2}, then axiom A2 implies that s_{1} = s_{3}, and so (s,e_{1}^{a},s_{1}) = (s_{2},e_{2}^{a},s_{3}), i.e., T_{m}1 is satisfied. Actually, this also implies that T_{m}4 holds. For, since the independence in am(A) is inherited from that on the events in A, we have that (s,e_{1}^{a},s_{1}) ∼ (s_{2},e_{2}^{a},s_{3}) implies I((s,e_{1}^{a},s_{1})) = I((s_{2},e_{2}^{a},s_{3})). This, as proved by Lemma 2.8, is equivalent to T_{m}4. Finally, T_{m}2 and T_{m}3 hold because of the corresponding A3 and A4. ✓

The definition of am on morphisms depends on the fact that LATS morphisms preserve independence on events.

Definition 3.6 (dLATS ↪ TSI_{m}) For (σ,η,λ): A → A′ a morphism of lats, let am((σ,η,λ)) be (σ,λ,τ), where

τ((s,e^{a},s′)) = \{ \begin{matrix}(σ(s),η(e)^{λ(a)},σ(s′)) & ifη(e)↓, \\ undefined & ifη(e)↑. \end{matrix}

By inspecting Definition 3.4, it is easy to verify that the above definition makes the diagram in Definition 2.9 commute. Moreover, it preserves ⪯, since axioms A!3 and A!4 ensure that e_{1} = e_{2}, whenever (s,e_{1}^{a},u) ⪯ (s′,e_{2}^{a},u′), i.e., since η preserve independence, am((σ,η,λ)) is well defined.

In order to prepare for our main proof, we first prove the following lemma.

Lemma 3.7 For any T in TSI_{m}, we have that am∘ ma(T) is isomorphic to T. Proof: (Sketch) We show that there is a bijection θ between T ran_{T} and T ran_{am∘ma(T)} such that (id_{S},id_{L},θ) and (id_{S},id_{L},θ^{−1} ) are morphisms of TSI_{m}, respectively from T to am∘ ma(T) and vice versa, inverses of each other. The obvious choice for θ(t) is (⟨t⟩_{1},[t]^{⟨t⟩_{2}},⟨t⟩_{3}). Observe that this gives an injective map because of axiom T_{m}1. ✓

The isomorphisms of 3.7 directly extends to a natural transformation

η = {(id_{S},id_{L},θ): T → am∘ ma(T)}_{T ∈TSI_{m}}: 1_{TSI_{m}} ⟹ am∘ ma.

We shall prove now that such a transformation is the unit of an adjunction involving ma and am, i.e., that am is right adjoint to ma: TSI_{m} ↪ dLATS.

Proposition 3.8 (ma ⊣ am: TSI_{m} ⇀ dLATS) For any A ∈ dLATS and any morphism m: T → am(A) in TSI_{m}, there exists a unique morphism m^{T}: ma(T) → A in dLATS such that am(m^{T}) ∘ η_{T} = m. Proof: Let m be (σ,λ,τ). Clearly, by definition of am, m^{T} must be of the form (σ,γ,λ) for some γ: E_{ma(T)}→ E_{A}. It is easy to realize that the only possible choice for γ is the following: for t ∈ Tran_{T} and τ(t)↓, let γ([t]) = e, if τ(t) = (s,e^{a},s′). This is a well given definition, for Lemma 2.10 ensures that m maps all transitions in [t] to the same ∼-class of Tran_{am(A)}, and the proof of Proposition 3.5 shows that if two transitions belong to the same ∼-class of Tran_{am(A)}, they originate from transitions in Tran_{A}carrying the same event. This proves both existence and uniqueness of m^{T}. Finally, it immediate to check that am(m^{T}) ∘ η_{T} = m. ✓

Since η is an isomorphism, by standard results in category theory, we have that the adjunction ma⊣ am: TSI_{m} ⇀ dLATS is a coreflection, i.e., TSI_{m} is coreflective in dLATS.

Concerning the coreflection described in the previous section, it is immediate to verify that the functors obtained by composing ma and am with the inclusion tm: TSI ↪ TSI_{m} and with the obvious inclusion of eLATS into dLATS coincide, respectively, with ta followed by eLATS ↪ dLATS and with at followed by tm, as illustrated in the following diagram.

[figure: TSI_{m}; ma; dLATS; am; TSI; ta; eLATS; at]

This supports our claim of TSI_{m} being a conservative and minimal extension of TSI, since regarding tsi_{m} as lats, the extension corresponds exactly to removing the constraint (Ex).

To complete our analysis, we identify the replete image of main LATS, i.e., the full subcategory mdLATS of dLATS consisting of the objects isomorphic to ma(T), for some T ∈ TSI_{m}.

Recall from basic category theory that mdLATS is determined by the coreflection: it consists of those A ∈ dLATS for which the corresponding component ϵ_{A} of the counit of ma ⊣ am 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}}): ma∘ am(A) → A}_{A∈dLATS}: ma∘ am ⟹ 1_{dLATS},

where, for (s,e^{a},s′) ∈ Tran_{am(A)}, γ([(s,e^{a},s′)]) = e. Clearly, ϵ_{A} is iso if and only if γ is such, i.e.,

(s,e_{1},s_{1}),(s_{2},e_{2},s_{3}) ∈ Tran_{A}, e_{1} = e_{2} ⇒ (s,e_{1},s_{1}) ∼ (s_{2},e_{2},s_{3}) ∈ Tran_{am(A)},

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_{m}). Expressed purely in terms of LATS, this is, as it was the case for TSI, exactly the event-maximal LATS. Observe that in Definition 2.5 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].

Proposition 3.9 (mdLATS ≅ TSI_{m}) mdLATS is equivalent to TSI_{m}. Proof: Let A be a diamond-extensional lats. We prove that the counit ϵ_{A}is iso if and only if A belongs to mdLATS. To this purpose, let γ be the event component of ϵ_{A}.

If γ is iso, i.e., for all (s,e_{1},s_{1}),(s_{2},e_{2},s_{3}) ∈ Tran_{A} we have that e_{1} = e_{2} implies (s,e_{1},s_{1}) ∼ (s_{2},e_{2},s_{3}), for any choice of ē∈ E_{A} and any ∅ ⊂ T ⊂ Tē, then the condition in Definition 2.5 is satisfied, since, by the diamond-extensionality of A, either A3 or A4 must fail for A[T]. In fact, in order for A[T] to be a LATS, diamond-extensionality implies that we must have (s,e_{1},s_{1}) ∈ T whenever a (s,e_{1},s_{1}) ∼ (s_{2},e_{2},s_{3}) for some (s_{2},e_{2},s_{3}) ∈ T, i.e., by the hypothesis on γ, T should be Tē. So A is event-maximal.

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

4 Conclusion

Based on a comparison between the model of asynchronous transition systems (a model with explicitly defined events) and the model of transition systems with independence (a more abstract model, with a derived notion of events) carried out by the authors in [10], we have introduced the transition systems with independence and multi-arcs — a conservative and minimal extension of transition systems with independence that features multi-arcs — showing that the ability of asynchronous transition systems to model multi-arcs does not depend inherently on the choice of having explicitly given events.

Adding multi-arcs to transition systems with independence constitutes a valuable enhancement to the model, which allows to model important situations in which multiple transitions between the same states represent different events with different causal histories.

Investigating the relationship between the category of transition systems with independence and multi-arcs and the category of labeled asynchronous transition systems that matches the one in [10], we have shown that the former is coreflective in the category of diamond-extensional labeled asynchronous transition systems, which intuitively are those transition systems that make no confusion about the identities of the events carried by transitions facing each other in independencediamonds. This coreflection provides a way to translate semantics forth and back between the two models. Finally, we have identified the event-maximal labeled asynchronous transition systems as the largest class of asynchronous transition systems for which the coreflection cuts down to an equivalence, so providing a precise characterisation of transition systems with independence and multi-arcs in terms of labeled asynchronous transition systems.

The analysis carried out in this paper helps in deciding when it is necessary to move to a more ‘intensional’ framework (a lower level of abstraction) in which further distinctions of events are introduced by assigning them explicitly. The definition of transition systems with independence and multi-arcs raises the threshold by allowing a derived notion of event also when multi-arcs are required.

References

[1] M.A. Bednarczyk, Categories of Asynchronous Systems. PhD thesis in Computer Science, University of Sussex (1988), report n. 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. Cattani and V. Sassone, Higher Dimensional Transition Systems, Proceedings of LICS’96, IEEE Computer Society Press (1996), 55–62.

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

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

[6] E. Goubault, Domains of Higher-Dimensional Automata, 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, 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, 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] T.T. Hildebrandt and V. Sassone, Comparing Transition Systems with Independence and Asynchronous Transition Systems, Proceedings of CONCUR’96, U. Montanari and V. Sassone (Eds.), LNCS 1119 (1996), Springer-Verlag, 84–97.

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

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

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

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

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

[16] M. Nielsen, V. Sassone and G. Winskel, Relationships between Models of Concurrency, 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.

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

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

[19] 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.

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

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

[22] 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).

Recent BRICS Report Series Publications

RS-97-10 Thomas Troels Hildebrandt and Vladimiro Sassone. Transition Systems with Independence and Multi-Arcs. April 1997. 20 pp. Appears in Peled, Pratt and Holzmann, editors, DIMACS Workshop on Partial Order Methods in Verification, POMIV ’96, pages 273–288.

RS-97-9 Jesper G. Henriksen and P. S. Thiagarajan. A Product Version of Dynamic Linear Time Temporal Logic. April 1997. 18 pp. To appear in Concurrency Theory: 7th International Conference, CONCUR ’97 Proceedings, LNCS, 1997.

RS-97-8 Jesper G. Henriksen and P. S. Thiagarajan. Dynamic Linear Time Temporal Logic. April 1997. 33 pp.

RS-97-7 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article to appear in the Journal of Functional Programming.

RS-97-6 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article to appear in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), Amsterdam, The Netherlands, June 1997.

RS-97-5 Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-4 Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation.