BRICS RS-94-6 Nielsen & Clausen: Bisimulations, Games and Logic

BRICS

Basic Research in Computer Science

Bisimulations, Games and Logic

Mogens Nielsen Christian Clausen

BRICS Report Series RS-94-6 ISSN 0909-0878 April 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

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

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

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

Bisimulations, Games and Logic

Mogens Nielsen  Christian Clausen
BRICS^{∗}

Department of Computer Science University of Aarhus DK-8000 Aarhus C, Denmark

Abstract

In a recent paper by Joyal, Nielsen, and Winskel, bisimulation is defined in an abstract and uniform way across a wide range of different models for concurrency. In this paper, following a recent trend in theoretical computer science, we characterize their abstract definition game-theoretically and logically in a non-interleaving model. Our characterizations appear as surprisingly simple extensions of corresponding characterizations of interleaving bisimulation.

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

Contents

1 Introduction 1 2 An Abstract Equivalence 4 3 Game Characterizations 8

3.1 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 A Characteristic Game for Interleaving Bisimulation … 10 3.3 Allowing Opponent to Backtrack . . . . . . . . . . . . . . 12

4 A Path Logic 16 5 Conclusion 18 A Every Game Has a Winner 21 B Proofs From Section 3 22

B.1 From δ-bisimilarity to Γ-equivalence . . . . . . . . . . . . 22 B.2 Permutations as Pomsets . . . . . . . . . . . . . . . . . . 23 B.3 From Pom_{L}-bisimilarity to δ-bisimilarity . . . . . . . . . 25 B.4 From iso-δ-bisimilarity to Pom_{L}-bisimilarity . . . . . . . 26 B.5 From Γ-equivalence to iso-δ-bisimilarity . . . . . . . . . . 30

C Proofs From Section 4 33

1 Introduction

An important ingredient of the theory of concurrency is the notion of behavioral equivalence between processes; what does it mean for two systems to be equal with respect to their communication structures? There is no unique answer to this question, but, undoubtedly, one of the most popular and successful answers was given by Park [Par81]: Two processes (or states s and s′ of two transition systems) are equivalent, or bisimilar, if for all actions a, every a-derivative of s is bisimilar to some a-derivative of s′, and vice versa.

One of the measures of success for a behaviour equivalence is its accompanying theory. And here bisimulation is particularly rich in results. Let us mention just three examples of elegant and powerful characterizations.

The first classical characterization is in terms of the existence of a bisimulation relation over states of the associated transition systems: Two transition systems are bisimilar iff there is a relation S over states such that the initial states are related, and

• whenever s S s′ and s⟶^{a}s_{1}, there is a transition s′⟶^{a}s′_{1} such that s_{1} S s′_{1}, and

• whenever s S s′ and s′⟶^{a}s′_{1}, there is a transition s⟶^{a}s_{1} such that s_{1} S s′_{1}.

The process of exploring whether two transition systems are bisimilar or not can be viewed as a game between two persons, Player and Opponent, taking turns [Sti93]. This provides an operational setting in which bisimulation may be understood experimentally. Player tries to prove the systems bisimilar, whereas Opponent intends otherwise. The game is opened by Opponent who chooses a transition from the initial state of one of the systems. This transition must be matched by Player with an equally labelled transition from the initial state of the other system. The new states form the starting point for the next pair of moves, and so forth. The play continues like this forever, in which case Player wins, or until either Player or Opponent is unable to move, in which case the opposition wins. This game is characteristic for bisimulation in the sense that two transition systems are bisimilar iff Player has a winning strategy, i.e. iff Player is able to win every game starting from the initial states.

\underline{2}

[figure: \begin{aligned}& ∘ \\ • & & • \\ & • \end{aligned}; a; b; b; a]

Figure 1: A transition system representing both a ∥ b and a.b + b.a.

Another important ingredient of the theory is the associated language of logical assertions. The logic, known as Hennessy-Milner logic [HM85], is a modal logic in which the modalities are indexed by actions. As such, it captures precisely the discrimination power of bisimulation: Two systems are bisimilar iff they satisfy the same logical assertions. For verification and analysis, the Hennessy-Milner logic is most interesting in conjunction with recursion. In such logic, it is possible to express properties like deadlocks, invariants, inevitability, etc. [Sti93]. Also this very expressive logic is characteristic for bisimulation.

In the transition system model of CCS and CSP, parallelism is treated as non-deterministic interleaving of atomic actions. As a result, the CCSprocesses a ∥ b, which can do the atomic actions a and b in parallel, is bisimilar to the process a.b + b.a, which non-deterministically chooses to do either “a followed by b” or “b followed by a”. In fact, the associated transition systems are isomorphic. Abstracting away from the names of the states, both transition systems are represented by the system of Fig. 1. Due to this identification, the transition system model is usually called an interleaving model, and bisimulation is traditionally called interleaving bisimulation when confusion is possible.

Interpreted at the machine level, non-deterministic interleaving corresponds to parallel processes sharing a single CPU. Opposed to this, Petri nets [WN94] model the physical disjointness of parallel processes. The processes a ∥ b and a.b + b.a are represented by the labelled nets of Fig. 1 [Old91]. The leftmost net consists of two independent events labelled a and b, whereas the rightmost net is a purely (nondeterministic) sequential net.

Many other closely related non-interleaving models have been suggested, e.g. the asynchronous transition systems of [Bed88, Shi85] and the transitions systems with independence of [WN94].

What is now the appropriate generalization of bisimulation to these

Figure 2: Labelled Petri nets representing a ∥ b and a.b + b.a. “independence models”? Many attempts have been made to answer this question. Unfortunately, with almost just as many different answers. Moreover, many of the proposed equivalences are incomparable. (See [GG89] and [GKP92] for definitions and comparisons of some of them.)

Apparently, the problem is that the step from interleaving models to independence models opens up for variations when trying to define an equivalence at the concrete level. [JNW93] reports on a promising attempt to define bisimulation in a uniform way across a wide range of different models for concurrent computation, including those described previously. However, the abstract definition is intangible. In order to obtain a better understanding of the equivalence, it is necessary to find concrete characterizations, which are indispensable for practical purposes. As a first measure of success, it is observed in [JNW93] that the abstract definition specializes to interleaving bisimulation in the case of ordinary transition systems.

In the context of an independence model, we shall denote the abstract equivalence by Pom_{L}-bisimilarity. The thoughts behind this choice of name will become clear later. In [JNW93], a concrete characterization of Pom_{L}-bisimilarity is given in the model of event structures, which may be thought of as unfoldings of nets or transition systems with independence. Interestingly, their characterization is not equal to any previously published equivalence; in fact, it is a strengthening of the history-preserving bisimulation [GG89, RT88].

\underline{4}

In this paper, we give concrete characterizations of Pom_{L}-bisimilarity in the model of transition systems with independence. As a matter of fact, our choice of model is not essential, in the sense that our results could equally have been formulated and proved for nets or asynchronous transition systems.

It turns out that surprisingly small twists of the game [Sti93] and relation [Mil89] characterizations of interleaving bisimulation lead to characterizations of Pom_{L}-bisimilarity. On the logical side, the Hennessy-Milner logic is extended with a backwards modality. The logic is characteristic for Pom_{L}-bisimilarity, when restricted to systems without autoconcurrency, i.e. to systems where no two consecutive and independent transitions are equally labelled. This restriction is necessary and has to do with the fact that our logic is based on labels. By strengthening the language of logical assertions, we can eliminate this restriction.

2 An Abstract Equivalence

In [JNW93], a uniform definition of bisimulation across a range of different models for parallel computation is presented. The aim of this section is to rephrase briefly parts of this work.

A model of computation is represented as a category. For a specific model, M, a choice of observation is any subcategory P of M. Typically, a choice of observation is a selection of “observation objects” of M, and P is then the corresponding full subcategory.

Given a model M and a choice of observation P, where P is a subcategory of M, a morphism f : X → Y is said to be P-open in M iff whenever a square

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

commutes, i.e. f ∘ p = q ∘ m, there is a morphism p′ : Q → X such that the “triangles” in

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

commute, i.e. p′ ∘ m = p and f ∘ p′ = q.

In the familiar example of M being a category of transition systems and P being sequences of labels (see [JNW93] for details), it turns out that open maps correspond to the well-known zig-zag morphisms of [Ben84].

Definition 2.1 Assume P is a subcategory of M and define two objects X and X′ of M to be P-bisimilar, written X ∼_{P} X′, iff there is a span of P-open morphisms f and f′ with common domain Y:

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

□

Using that pullbacks of P-open maps are themselves P-open, it can be shown that P-bisimilarity is an equivalence relation provided that M has pullbacks.

The category of transition systems turns out to have pullbacks, and the notion of P-bisimilarity (P again being sequences of labels) turns out to coincide precisely with (strong) bisimilarity in the sense of [Mil89].

The interesting question is what you get when you lift this abstract characterization to non-interleaving models. One choice of model made in [JNW93] is transition systems with independence. Transition systems with independence are precisely what their name suggests, namely ordinary transition systems with an additional relation expressing when one transition is independent of another. The independence relation expresses which actions can happen in parallel.

Definition 2.2 A transition system with independence is a structure

X = (S, i, L, Tran, I)

where

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

• L is a set of labels,

• Tran ⊆ S × L × S is a set of transitions^{1}, and

• I ⊆ Tran^{2} is an independence relation which is irreflexive and symmetric.

Moreover, we require the following axioms to hold:

1As usual, a transition (s, a, s_{1}) ∈ Tran is written as s⟶^{a}s_{1}.

1. s⟶^{a}s_{1} ∼ s⟶^{a}s_{2} ⇒ s_{1} = s_{2}

2. s⟶^{a}s_{1} I s_{1}⟶^{b}u ⇒ ∃s_{2}. s⟶^{a}s_{1} I s⟶^{b}s_{2} I s_{2}⟶^{a}u

3. (a) s⟶^{a}s_{1} ≺ s_{2}⟶^{a}u I w⟶^{b}w′ ⇒ s⟶^{a}s_{1} I w⟶^{b}w′

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

where the relation ≺ between transitions is defined by

s⟶^{a}s_{1} ≺ s_{2}⟶^{a}u ⇔ ∃b. s_{1}⟶^{b}u I s⟶^{a}s_{1} I s⟶^{b}s_{2} I s_{2}⟶^{a}u,

and ∼ is the least equivalence relation including ≺. □

The ∼-equivalence classes should be thought of as events. Thus, Axiom 1 asserts that the occurrence of an event at a state yields a unique state. Similarly, Axiom 3 asserts that independence respects events. Axiom 2 describes the intuitive property of independence that whenever two independent transitions occur consecutively, they can also occur in the opposite order. Hence, if s⟶^{a}s_{1}⟶^{b}u are independent transitions there is an “independence square”

[figure: \begin{aligned}& s \\ s_{1} & I & s_{2} \\ & u \end{aligned}; a; b; b; a]

Moreover, Axiom 1 implies the uniqueness of s_{2}. So we are justified in saying that s_{2} (or s⟶^{b}s_{2}⟶^{a}u) is the completion of s⟶^{a}s_{1}⟶^{b}u.

Notice that an ordinary labelled transition system can be viewed as a transition system with independence having empty independence relation. Furthermore, the standard labelled case graph of a labelled (safe) net, with two transitions being independent iff they represent firings of independent (in net terminology) events, is a transition system with independence [WN94]. As an example the transition system with independence above is the representation of the CCS-expression a ∥ b or its corresponding net from 1 (following [WN94]).

For later use, we introduce some terminology. For a transition t = (s⟶^{a}s_{1}) we shall write src(t), tgt(t), and ℓ(t) for s, s_{1}, and a, respectively. The set Seqs(X) consists of those transition sequences t̄ = t_{0}t_{1} ⋯ t_{n−1} in X beginning at the initial state (src(t_{0}) = i) which are consecutive (src(t_{i+1}) = tgt(t_{i})). Transition sequences are always indexed from zero. We write (t̄)_{i} or simply t_{i} for the i’th transition in t̄. The length of t̄ is referred to as |t̄|. When nothing else is stated, a transition system with independence X is assumed to have components S, i, L, Tran, and I.

The category TI has transition systems with independence as objects. For the remaining part of this paper we fix a set L and restrict ourselves to those transition systems with independence that have labelling set L. As morphisms in the category TI_{L} we choose the fiber-morphisms of [WN94]:

Definition 2.3 Let X = (S, i, L, Tran, I) and X′ = (S′, i′, L′, Tran′, I′) be transition systems with independence. A morphism f from X to X′ is a function f : S → S′ such that

• f(i) = i′

• for all transitions s⟶^{a}s_{1} in X, f(s)⟶^{a}f(s′) in X′

• s⟶^{a}s_{1} I u⟶^{b}u_{1} in X implies f(s)⟶^{a}f(s_{1}) I′ f(u)⟶^{b}f(u_{1}) in X′ □

As observations it is naturally to take Pratt’s pomsets [Pra86]. We identify the category Pom_{L} of pomsets with its full and faithful embedding in TI_{L} (for details see [JNW93]). The category TI_{L} has pullbacks, so Pom_{L}-bisimilarity is an equivalence relation in TI_{L}. The following proposition characterizes Pom_{L}-open morphisms in TI_{L} [JNW93].

Proposition 2.4 A morphism f : Y → X in TI_{L} is Pom_{L}-open iff it is zig-zag and reflects consecutive independence, i.e. iff it has the following properties:

• whenever r is reachable and f(r)⟶^{a}s_{1} there is a state r_{1} in Y such

that r⟶^{a}r_{1} & f(r_{1}) = s_{1}, and

• whenever r is reachable, r⟶^{a}r_{1} and r_{1}⟶^{b}r_{2} are transitions in Y, and

f(r)⟶^{a}f(r_{1}) I f(r_{1})⟶^{b}f(r_{2}),

we also have r⟶^{a}r_{1} I r_{1}⟶^{b}r_{2}.

On event structures [JNW93] Pom_{L}-bisimilarity turns out to be a slight strengthening of the history-preserving bisimilarity originally defined in [GG89, RT88]. In fact, the same strengthening has been studied in [Bed91] in which the equivalence is denoted hereditary history-preserving bisimilarity. The strengthening is illustrated by the following event structures, here identified with their embeddings in TI_{L}.

Example 2.5 Consider the following “event structures”:

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

The circles indicate the initial states. These “event structures” are historypreserving bisimilar but not hereditary history-preserving bisimilar. □

One result on Pom_{L}-bisimilarity for TI_{L} mentioned in [JNW93] is the fact that two TI_{L}-objects are Pom_{L}-bisimilar iff their unfolded event structures are Pom_{L}-bisimilar. The natural question is now: Does Pom_{L}- bisimilarity for TI_{L} have characterizations in the spirit of e.g. the relational, game-theoretical, and logical characterizations of bisimulation for standard transition systems? This question is answered positively in the next sections.

3 Game Characterizations

Following a new trend in the area of program semantics, we first present a game-theoretical characterization of Pom_{L}-bisimilarity. The game defined can be viewed as a “backtracking” extension of Stirling’s game [Sti93]. We then show that the equivalence induced by the backtracking game can be characterized by the existence of a bisimulation relation over paths, satisfying a certain “backtracking property”.

3.1 Basic Definitions

The following definitions are inspired by [AJ92].

A game is a structure Γ = (C, c_{0}, >, λ, W) where • C is a set of configurations with a distinguished initial configuration

c_{0},

• > ⊆ C^{2} is a set of moves. Formally, a play of Γ is a (possibly infinite) sequence of moves

c_{0} · c_{1} · c_{2} · . . . ,

such that c_{0} > c_{1} > c_{2} > · · ·. The set Pos(Γ) of positions consists of all finite plays. The meta-variable p ranges over positions.

• λ : Pos(Γ) → {O, P } is a function indicating whose turn it is to move in a given position (an element of Pos(Γ), defined below) of a play, and

• W ⊆ Pos(Γ) is a set of winning positions.

We require all plays to be alternating, i.e. we require > and λ together to satisfy that if λ(p·c) = Q and c >c′ then λ(p·c·c′) = \overline{Q}, where \overline{P} = O and \overline{O} = P. Furthermore, Opponent should start every play. This is expressed by demanding λ(c_{0}) = O.

In defining when a game is won we take Player’s point of view: A play p is won (by P) if one of the following conditions hold:

• p is infinite,

• p is finite and λ(p) = O, or

• p ∈ W.

If p is not won, it is lost.

A strategy is a partial function σ : Pos(Γ) ⇀ C such that

σ(p · c) = c′ implies c > c′.

We reserve the words strategy for Player and counter-strategy for Opponent and use σ and τ to range over strategies and counter-strategies, respectively. Player is said to follow her strategy σ in a play c_{0} · c_{1} · . . . · c_{n} · c_{n+1} · . . . iff λ(c_{0} · c_{1} · . . . · c_{n}) = P implies c_{n+1} = σ(c_{0} · c_{1} · . . . · c_{n}). Similarly, we can define when Opponent follows his strategy.

The intuition behind W is the following. As soon as Player can force Opponent to a position p ∈ W, she has won p and all extensions of p. We reflect this intuition by demanding that W is closed under >, i.e. that p · c ∈ W whenever p ∈ W. To avoid a play p ∈ W to continue forever, we require all strategies to be undefined on winning positions, i.e. σ(p) is undefined whenever p ∈ W.

The set Plays(σ, τ) of plays in which both Player and Opponent follow their strategies is easily seen to be prefix-closed. This leads to the following definition of the play of a strategy σ against a counter-strategy τ:

⟨σ|τ⟩ = ⨆{p | p ∈ Plays(σ, τ)},

where the least upper bound refers to the prefix-ordering. Finally, σ is said to be a winning strategy iff ⟨σ|τ⟩ is won for any counter-strategy τ. Similarly, we define τ to be a winning counter-strategy iff ⟨σ|τ⟩ is lost for any σ.

Any game of the above kind possesses the nice property that there can be no ties, and hence there is either a winning strategy or a winning counter-strategy.

Proposition 3.1 For any game, there is a winning strategy iff there is no winning counter-strategy.

Proof See Appendix A. □

3.2 A Characteristic Game for Interleaving Bisimulation

The first game considered is a “sequence variant” of the game defined by Stirling [Sti93]. Given two ordinary transition systems X and X′ we take as configurations (ordered) pairs of transition sequences with the pair consisting of empty sequences as initial configuration. Informally, a play progresses as follows. Opponent starts out by first choosing either X or X′ and then a transition from the initial state of the system chosen. If Player can’t match the move with an equally labelled transition from the initial state of the other system, she loses. Otherwise, she chooses such a matching transition, and it’s again Opponent’s turn to move. He chooses a system, not necessarily the same as before, and a transition of that system leading out of the state arrived at in the previous pairs of moves. Again, Player is required to match with an equally labelled transition in the other system. The play continues like this forever, in which case Player wins, or until either Player or Opponent is stuck (unable to move), in which case the other participant wins.

The above description is now formalized to fit the basic definitions of games. We define the interleaving game between transition systems X and X′ to be Γ(X, X′) = (C, c_{0}, >, λ, W) where

• C = Seqs(X) × Seqs(X′). As a convention, writing configurations (t̄, t̄′), (t̄t, t̄′), and (t̄, t̄′t′) implicitly means that |t̄| = |t̄′|.

• c_{0} = (ε, ε).

• λ : Pos(Γ(X, X′)) → {O, P } is defined by taking

λ(t̄, t̄′) = O and λ(t̄t, t̄′) = λ(t̄, t̄′t′) = P.

• W = ∅.

• > ⊆ C^{2} is defined by the rules

(t̄, t̄′) > (t̄t, t̄′) if t̄t ∈ Seqs(X)
(t̄, t̄′) > (t̄, t̄′t′) if t̄′t′ ∈ Seqs(X′)
(t̄t, t̄′) > (t̄t, t̄′t′) if t̄′t′ ∈ Seqs(X′) & ℓ(t′) = ℓ(t)
(t̄, t̄′t′) > (t̄t, t̄′t′) if t̄t ∈ Seqs(X) & ℓ(t) = ℓ(t′)

Just like Stirling’s game, the game Γ(X, X′) is characteristic for interleaving bisimulation in the following sense.

Theorem 3.2 Two transition systems X and X′ are bisimilar iff Player has a winning strategy in Γ(X, X′).

Proof Small modifications of the reasoning of Stirling [Sti93]. □

The game presented above has the property that if X and X′ exhibit infinite behaviour, then there exist infinite plays, even if both systems are finite state. For some purposes this property is undesirable, and can indeed can be eliminated by choosing the set W of winning positions appropriately. To be concrete, we might in Γ(X, X′) have chosen W to consist of those positions p which are duplicate-free in the sense that no two configurations (t̄, t̄′), (r̄, r̄′) in p have tgt(t̄) = tgt(r̄) and tgt(t̄′) = tgt(r̄′). By the pigeonhole principle this modification of Γ(X, X′) would bound the length of any play by 2 · |S| · |S′| + 1 where |S| and |S′| are the number of states in X and X′, respectively. Furthermore, it is quite easy to see that the characterization result also holds for the modified game.

3.3 Allowing Opponent to Backtrack

Throughout this paper we shall take “backtrack” to mean trace backwards within the present observation.

With this interpretation, backtracking in an ordinary transition system means to trace backwards along the transition sequence observed. In terms of games, we can express this by allowing Opponent to do backwards moves like

(t̄t, t̄′t′) > (B, t̄, t̄′t′),

where the B is a directive to Player to play backwards on the longer of the sequences. Player must match with the move

(B, t̄, t̄′t′) > (t̄, t̄′).

It is easy to see that these additional rules do not give Opponent more opportunities to beat Player, nor the other way around.

Proposition 3.3 Two transition systems are bisimilar iff Player has a winning strategy in their associated game with backtracking.

Backtracking in an independence model is much more interesting. Consider a simple transition system with independence X

[figure: \begin{aligned}& i \\ s_{1} & I & s_{2} \\ & u \end{aligned}; a; b; b; a]

consisting of a single independence square. Since i⟶^{a}s_{1} and s_{1}⟶^{b}u are independent, the sequence t̄= i⟶^{a}s_{1}⟶^{b}u in X represents the observation “a and b in parallel”. Another representative of this observation is the sequence i⟶^{b}s_{2}⟶^{a}u, so this gives us two ways to backtrack within t̄: Either along s_{1}⟶^{b}u, leaving behind the sequence i⟶^{a}s_{1}, or along s_{2}⟶^{a}u leaving behind the sequence i⟶^{b}s_{2}.

In terms of the net representation of a ∥ b from Section 1 this amounts to the following: After firing the a-transition followed by the b-transition you may naturally backtrack on the a-transition, since the firing of the b-transition has in no way affected the post-conditions of the a-transition.

In the above example the event represented by i⟶^{a}s_{1} has an occurrence – namely s_{2}⟶^{a}u – ending in u. We say that i⟶^{a}s_{1} is backwards enabled in the sequence i⟶^{a}s_{1}⟶^{b}u. In general, a transition t_{i} of a sequence t̄ is said to be backwards enabled iff it by repeated use of Axiom 2 of Definition 2.2 can be “pushed to last position in t̄.” By Axiom 3, this is equivalent to requiring t_{i} to be independent of all transitions t_{j} in t̄ with j > i. This leads to the following formal definition.

Definition 3.4 For t̄= t_{0} ⋯ t_{n−1}, a sequence in a transition system with independence X, and i ∈ {0, …, n − 1}, we define

t_{i} ∈ BEn(t̄) iff ∀j ∈ {i + 1, …, n − 1}. t_{j} I t_{i},

where I is the independence relation in X. If t_{i} ∈ BEn(t̄) we define δ(i, t̄) to be the result of deleting the event corresponding to t_{i}, i.e.

δ(i, t̄) = t_{0} ⋯ t_{i−1}s_{i+1} ⋯ s_{n−1},

where s_{i+1} ≺ t_{i+1}, …, s_{n−1} ≺ t_{n−1} as in the following figure in which the squares are the unique completions defined in Section 2.

[figure: \begin{aligned}∘ & • & • & • & • & • & • \\ & & & • & • & • & • \end{aligned}; t_{0}; …; t_{i−1}; t_{i}; s_{i+1}; …; s_{n−1}; s_{i}; t_{i+1}; …; t_{n−1}]

□

The backtracking game on transition systems with independence is a simple extension of the previously defined (forward) game. By introducing rules like

(t̄, t̄′) > (i, δ(i, t̄), t̄′) if t_{i} ∈ BEn(t̄)

we allow Opponent to backtrack on transitions which are backwards enabled. The index i is a request to Player to play backwards on the i’th transition of the longer of the sequences. So the only way Player can respond to such moves is to use the rule

(i, δ(i, t̄), t̄′) > (δ(i, t̄), δ(i, t̄′)) if t′_{i} ∈ BEn(t̄′),

provided, of course, that t′_{i} is backwards enabled in t̄′. Formally, we define the backtracking game Γ(X, X′) on transition systems with independence X and X′ to be the structure (C, c_{0}, >, λ, W):

• C = ω ×Seqs(X)×Seqs(X′)∪Seqs(X)×Seqs(X′). Conventionally, writing configurations (i, δ(i, t̄), t̄′) and (i, t̄, δ(i, t̄′)) implicitly means that |t̄| = |t̄′|.

• c_{0} = (ε, ε).

• λ : Pos(Γ(X, X′)) → {O, P } is defined by taking λ(t̄, t̄′) = O and λ(t̄t, t̄′) = λ(t̄, t̄′t′) = λ(i, δ(i, t̄), t̄′) = λ(i, t̄, δ(i, t̄′)) = P.

• W = ∅.

• > ⊆ C^{2} is defined by the following rules:

(t̄, t̄′) > (t̄t, t̄′)  if t̄t ∈ Seqs(X)
(t̄, t̄′) > (t̄, t̄′t′)  if t̄′t′ ∈ Seqs(X′)
(t̄t, t̄′) > (t̄t, t̄′t′)  if t̄′t′ ∈ Seqs(X′) & ℓ(t′) = ℓ(t)
(t̄, t̄′t′) > (t̄t, t̄′t′)  if t̄t ∈ Seqs(X) & ℓ(t) = ℓ(t′)
(t̄, t̄′) > (i, δ(i, t̄), t̄′)  if t_{i} ∈ BEn(t̄)
(t̄, t̄′) > (i, t̄, δ(i, t̄′))  if t′_{i} ∈ BEn(t̄′)
(i, δ(i, t̄), t̄′) > (δ(i, t̄), δ(i, t̄′)) if t′_{i} ∈ BEn(t̄′)
(i, t̄, δ(i, t̄′)) > (δ(i, t̄), δ(i, t̄′)) if t_{i} ∈ BEn(t̄)

Definition 3.5 Two transition systems with independence X and X′ are Γ-equivalent, written X ∼_{Γ} X′, iff Player has a winning strategy in Γ(X, X′). □

With a simple example we will now illustrate how backtracking distinguishes parallelism from non-deterministic interleaving.

Example 3.6 Consider the transition systems with independence representing the CCS-processes a ∥ b and a.b + b.a:

[figure: \begin{aligned}& i \\ s_{1} & I & s_{2} \\ & u \end{aligned}; a; b; b; a; \begin{aligned}& i′ \\ s′_{1} & & s′_{2} \\ & u′ \end{aligned}; a; b; b; a]

These systems are interleaving bisimilar but not Γ-equivalent, as we are able to define a winning counter-strategy τ as follows (here, p ranges over all appropriate positions):

τ(ε, ε) = (i⟶^{a}s_{1}, ε)
τ(p · (i⟶^{a}s_{1}, i′⟶^{a}s′_{1})) = (i⟶^{a}s_{1}⟶^{b}u, i′⟶^{a}s′_{1})
τ(p · (i⟶^{a}s_{1}⟶^{b}u, i′⟶^{a}s′_{1}⟶^{b}u′)) = (0, i⟶^{b}s_{2}, i′⟶^{a}s′_{1}⟶^{b}u′)

The point is, of course, that Player is unable to backtrack on index 0 in the sequence i′⟶^{a}s′_{1}⟶^{b}u′, as these transitions are dependent. □

Distinguishing the transition systems with independence of Example 3.6 is, in fact, a minimum demand on any reasonable generalization of bisimulation to independence models. And following the reasoning of Example 3.6, the reader should not be surprised that backtracking may be used by Opponent to detect the partial order structures of configurations. However, it is more surprising that Γ-equivalence coincides exactly with the abstractly derived Pom_{L}-bisimilarity of Section 2. As a more interesting example, the reader may check that Opponent has a winning counterstrategy in the game associated with the systems of Example 2.5.

Theorem 3.7 Γ-equivalence coincides with Pom_{L}-bisimilarity.

Proof See Appendix B. □

We also have a relational characterization of Pom_{L}-bisimilarity.

Definition 3.8 A relation T ∈ Seqs(X) × Seqs(X′) is a δ-bisimulation between X and X′ iff it satisfies the following axioms:

A_{init}: ε T ε A_{bisim}:

1. t̄ T t̄′ & t̄t ∈ Seqs(X) ⇒ ∃t′. (ℓ′(t′) = ℓ(t) & t̄t T t̄′t′)
2. t̄ T t̄′ & t̄′t′ ∈ Seqs(X′) ⇒ ∃t. (ℓ(t) = ℓ′(t′) & t̄t T t̄′t′)

A_{δ}: t̄ T t̄′ ⇒ \{ \begin{matrix}(t_{i} ∈ BEn(t̄) ⇔ t′_{i} ∈ BEn(t̄′)) & \\ (t_{i} ∈ BEn(t̄) ⇒ δ(i, t̄) T δ(i, t̄′)) \end{matrix}

Two transition systems with independence X and X′ are δ-bisimilar, written X ∼_{δ} X′, iff there exists a δ-bisimulation between them. □

The axiom A_{bisim} is the usual “bisimulation axiom”, here formulated on sequences rather than states. So this formulation is also a simple extension of a well-known concept.

Theorem 3.9 δ-equivalence coincides with Pom_{L}-bisimilarity.

Proof See Appendix B. □

4 A Path Logic

Just as interleaving bisimulations can be characterized as a relation over paths, we can interpret the Hennessy-Milner logic over paths rather than states. Following [HS85], we may add a past tense modality ◯ a , where a is a label, and obtain a logic which still characterizes bisimulation for ordinary transition systems. However, interpreted over transition systems with independence, we obtain a logic which is easily shown to be sound for Pom_{L}-bisimilarity. Furthermore, the logic is complete if we restrict to systems which do not exhibit auto-concurrency, i.e. systems in which no two consecutive and equally labelled transitions are independent.

Let Assn be the following language of assertions:

A ::= ¬A | _{j∈J}^{⋀} A_{j} | ⟨a⟩A | ◯ a A.

By convention, true is the conjunction over the empty set.

Definition 4.1 Let X be a transition system with independence and suppose t̄, r̄ ∈ Seqs(X). Define

r̄⟶^{a}t̄ iff r̄(s⟶^{a}s_{1}) = t̄
r̄ ⇝^{a} t̄ iff ∃i. (t_{i} ∈ BEn(t̄) & ℓ(t_{i}) = a & r̄ = δ(i, t̄))
□

In ordinary transition systems, ◯ a A is interpreted as “it was the case at the last moment – just before a – that A”. It seems natural for transition systems with independence to interpret ◯ a A as “a could have been the last action, and at the moment before a it was the case that A”.

Formally, let X be a transition system with independence and define the satisfaction relation ⊧_{X}⊆ Seqs(X) × Assn by structural induction on assertions:

t̄⊧_{X} ¬A iff t̄|̸=_{X} A
t̄⊧_{X} ⋀_{j∈J} A_{j} iff ∀j ∈ J. t̄⊧_{X} A_{j}
t̄⊧_{X} ⟨a⟩A iff ∃r̄. (t̄⟶^{a}r̄ & r̄ ⊧_{X} A)
t̄⊧_{X} ◯ a A iff ∃r̄. (r̄ ⇝^{a} t̄ & r̄ ⊧_{X} A)

An assertion is satisfied by X, written ⊧_{X} A, iff ε ⊧_{X} A.

Definition 4.2 Two transition systems with independence X and X′ are Assn-equivalent iff they satisfy the same assertions, i.e. iff

∀A ∈ Assn. (⊧_{X} A ⇔ ⊧_{X′} A).
□

For ordinary transition systems (without independence) this logic is characteristic for bisimulation.

Theorem 4.3 Two transition systems are bisimilar iff they are Assnequivalent.

Proof See [HS85]. □

Example 4.4 To see the logic in action on transition systems with independence, let us return to Example 2.5. An assertion distinguishing the two systems is ⟨a⟩(⟨c⟩true ∧ ⟨b⟩◯ a ⟨d⟩). This assertion is satisfied by the right-hand system, but not by the left-hand system. □

As usual, the soundness proof is straightforward.

Proposition 4.5 If two transition systems with independence are Pom_{L}- bisimilar, then they are also Assn-equivalent.

Proof See Appendix C. □

Restriction to systems without auto-concurrency is essential for completeness.

Example 4.6 Consider two systems X and X′

[figure: \begin{aligned}& ∘ \\ • & I & • \\ & • \end{aligned}; a; a; a; a; \begin{aligned}& ∘ \\ • & & • \\ & • \end{aligned}; a; a; a; a]

which are identical except that the square in X is an independence square, whereas the square in X′ is not. These systems satisfy the same assertions, but are certainly not Pom_{L}-bisimilar. □

Proposition 4.7 If two non-auto-concurrent transition systems with independence are Assn-equivalent, then they are also Pom_{L}-bisimilar.

Proof See Appendix C. □

As mentioned in the introduction, the restriction to systems without auto-concurrency has to do with the logic being based on labels. Replacing the backwards modalities ◯ a , where a is label, with modalities ◯ i , where i is an index, and defining

t̄⊧_{X} ◯ i A iff t_{i} ∈ BEn(t̄) & δ(i, t̄) ⊧_{X} A,

we obtain a logic which is complete for Pom_{L}-bisimilarity without restrictions.

5 Conclusion

We have given concrete characterizations of Pom_{L}-bisimilarity on transition systems with independence. Our characterizations are easy to understand and appear as conservative extensions of the corresponding characterizations of interleaving bisimulation.

The present work leaves open the decidability of Pom_{L}-bisimilarity for finite state systems. One approach would be to look for set W of winning positions, generalizing the notion of duplicates in our argument for decidability of bisimulation for ordinary transition systems. However, it is not quite clear what the appropriate generalization should be in the setting of transition systems with independence.

References

[AJ92] S. Abramsky and R. Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic. DoC 92/24, Imperial College of Science, Technology and Medicine, 1992.

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

[Bed91] M. A. Bednarczyk. Heredity History Preserving Bisimulations. Unpublished, Draft of 1991.

[Ben84] J. Van Bentham. Correspondence theory. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 2. Reidel, 1984.

[GG89] R. van Glaabek and U. Goltz. Equivalence Notions for Concurrent Systems and Refinement of Actions. In MFCS ’89. Springer-Verlag LNCS 379, 1989.

[GKP92] U. Goltz, R. Kuiper, and W. Penczek. Propositional Temporal Logics and Equivalences. In Concur ’92. Springer-Verlag LNCS 630, 1992.

[HM85] M. C. Hennessy and A. J. R. G. Milner. Algebraic Laws for Non-determinism and Concurrency. Journal of ACM, 32(1), 1985.

[HS85] M. Hennessy and C. P. Stirling. The power of the future perfect in program logics. In A. R. Meyer, editor, Information and Control, volume 67. Academic Press, Inc. , 1985.

[JNW93] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation and open maps. In LICS ’93, 1993. To appear in Information and Computation.

[Mil89] A. J. R. G. Milner. Communication and Concurrency. Prentice Hall, 1989.

[Old91] E.-R. Olderog. Nets, Terms and Formulas. Cambridge University Press, 1991.

[Par81] D. M. R. Park. Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science, 5th GL-conference. Springer-Verlag LNCS 104, 1981.

[Pra86] V. R. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Programming, 15(1), 1986.

[RT88] A. Rabinoritch and B. Traktenbrot. Behaviour structures and nets. Fundamenta Informatica, 11(4), 1988.

[Shi85] M. W. Shields. Concurrent machines. Computer Journal, 88, 1985.

[Sti93] C. Stirling. Modal and Temporal Logics for Processes, 1993. Notes for Summer School in Logic Methods in Concurrency, Department of Computer Science, Aarhus University.

[WN94] G. Winskel and M. Nielsen. Models for Cuncurrency. In S. Abramsky and D. Gabbay, editors, Handbook of Logic in Computer Science, volume 3. Oxford University Press, 1994.

A Every Game Has a Winner

Proposition A.1 (Proposition 3.1 restated) For any game, there is a winning strategy iff there is no winning counter-strategy.

Proof Let Γ be a game. Obviously, if there is a winning strategy in Γ, there can be no winning counter-strategy.

For the converse direction, assume there is no winning counter-strategy. Say τ a winning counter-strategy from (wcsf) p ∈ Pos(Γ) iff

λ(p) = O & ∀σ. (p ∈ Plays(σ, τ) ⇒ ⟨σ|τ⟩ is lost).

Suppose now that λ(p) = O. It can then be shown that if Opponent has no winning counter-strategy from p, then

∀p · c ∈ Pos(Γ). ( \begin{matrix}p · c ∈ W, or \\ ∃p · c · c′ ∈ Pos(Γ). (O has no wcsf p · c · c′). \end{matrix} )

Using this property, we define a strategy σ as follows. Whenever Opponent has no winning counter-strategy from p ∈ Pos(Γ), and p · c ∈ Pos(Γ) \ W, we choose a configuration c′ such that p · c · c′ ∈ Pos(Γ) and Opponent has no winning counter-strategy from p · c · c′. Define σ(p · c) = c′.

By definition, σ is a strategy. In order to argue that σ is winning, let τ be an arbitrary counter-strategy. Inductively in the length of p, it is easy to show the following property:

∀p ∈ Plays(σ, τ). ( \begin{matrix}λ(p) = O & Opponent has no wcsf p, or \\ λ(p) = P & (σ is defined on p or p ∈ W) \end{matrix} ) .

(Notice that our assumption that Opponent has no winning counterstrategy amounts to the fact that Opponent has no winning counterstrategy from the initial configuration c_{0}.) But then, since σ is defined whenever it it Player’s turn to move, the play ⟨σ|τ⟩ must be won. This finishes the proof of the proposition. □

B Proofs From Section 3

As an intermediate step we introduce yet another equivalence, denoted iso-δ-bisimilarity. The main theorems 3.7 and 3.9 will be established by completing the following picture in which ↪ denotes set inclusion:

[figure: \begin{aligned}∼_{δ} & ∼_{Pom_{L}} \\ ∼_{Γ} & ∼_{iso-δ} \end{aligned}; B.1; B.10; B.15; B.13]

The inclusions are labeled with references to corresponding propositions.

B.1 From δ-bisimilarity to Γ-equivalence

Proposition B.1 ∼_{δ} ⊆ ∼_{Γ}.

Proof Let T ⊆ Seqs(X) × Seqs(X′) be a δ-bisimulation between X and X′, and define a partial function σ : Pos(Γ(X, X′)) → C in the following way:

• Whenever t̄ T t̄′ and t̄t ∈ Seqs(X), choose t′ such that t̄′t′ ∈ Seqs(X′) and t̄t T t̄′t′. Then, for all p · (t̄t, t̄′) ∈ Pos(Γ(X, X′)), define

σ(p · (t̄t, t̄′)) = (t̄t, t̄′t′).

In a similar way, σ is defined to respond to moves on the right-hand side.

• Whenever t̄ T t̄′ and t_{i} ∈ BEn(t̄), we know, since T satisfies A_{δ}, that t′_{i} ∈ BEn(t̄′) and δ(i, t̄) T δ(i, t̄′). For all p · (i, δ(i, t̄), t̄′) ∈ Pos(Γ(X, X′)) we define

σ(p · (i, δ(i, t̄), t̄′)) = (δ(i, t̄), δ(i, t̄′)).

Here, too, there is a symmetric definition. By construction, σ is a strategy. We now argue that σ is winning: For all counter-strategies τ it follows by induction in the length of p that

p · (t̄, t̄′) ∈ Plays(σ, τ) & λ(p · (t̄, t̄′)) = O ⇒ t̄ T t̄′.

Hence, from construction it follows that ⟨σ|τ⟩ is won. □

B.2 Permutations as Pomsets

An iso-δ-bisimulation is a δ-bisimulations which furthermore respect isomorphisms between observations, i.e. between pomsets. Actually, we present iso-δ-bisimulations without mentioning pomsets at all. Instead, we use permutations of transition sequences. As we shall soon see, these permit us to reason inductively.

If two consequtive transitions t_{i} and t_{i+1} of a transition sequence t̄ are independent, they can – due to Axiom 2 of Definition 2.2 – be swapped, resulting in the (unique) sequence

t_{0} ⋯ t_{i−1}s_{i+1}s_{i}t_{i+2} ⋯ t_{n−1},

where s_{i+1}s_{i} is the unique completion of t_{i}t_{i+1}. A permutation is a series of such “swappings”.

Formally, we define a permutation (in a given transition system with independence X) to be a partial function • : ω^{∗} × Seqs(X) ⇀ Seqs(X), where ω^{∗} is the set of natural numbers (here, including 0). We shall use infix notation for •, and for π ∈ ω^{∗} and t̄ ∈ Seqs(X) we define π • t̄ recursively in the length |π| of π:

ε • t̄ is always defined and equals t̄.

iπ •t̄is defined iff π •t̄is defined, i ∈ {0, …, |t̄|−2}, and r_{i} I r_{i+1}, where π • t̄= r̄. If defined, iπ • t̄ equals r_{0} ⋯ r_{i−1}s_{i+1}s_{i}r_{i+2} ⋯ r_{n−1}, where

s_{i+1}s_{i} is the unique completion of r_{i}r_{i+1}:
[figure: \begin{aligned}& & & & • \\ ∘ & • & • & • & & • & • & • & • \\ & & & & • \end{aligned}; s_{i}; r_{0}; …; r_{i−1}; s_{i+1}; r_{i}; r_{i+2}; …; r_{n−1}; r_{i+1}]

It is straightforward to show that • possesses the “group action property” ππ′ • t̄= π • (π′ • t̄)

Definition B.2 A sequence π ∈ ω^{∗} is a permutation of a sequence t̄ ∈ Seqs(X) provided π•t̄is defined. Write Π_{X}(t̄) for the set of permutations of t̄.

Given a permutation π of a sequence t̄, we want ⟨π, t̄⟩(i) = j to express that the i’th transition of t̄ by π is swapped to position j. This intuition is captured in the following definition.

Definition B.3 Suppose π is a permutation of t̄. Then, we define ⟨π, t̄⟩ : {0, …, |t̄| − 1} → {0, …, |t̄| − 1} inductively in |π|.

⟨ε, t̄⟩ is the identity function.

⟨kπ, t̄⟩(i) = \{ \begin{matrix}k + 1 & if k = ⟨π, t̄⟩(i) \\ k & if k + 1 = ⟨π, t̄⟩(i) \\ ⟨π, t̄⟩(i) & otherwise \end{matrix}

It is easy to see that ⟨π, t̄⟩ is a bijection. The inverse function is ⟨π^{−1}, π•t̄⟩, where π^{−1} is π reversed.

The following lemmata express two very natural properties of permutations.

Lemma B.4 Let t̄∈ Seqs(X) and assume ⟨π, t̄⟩(i) = j for some permutation π and indices i and j. Then t_{i} ∈ BEn(t̄) iff (π • t̄)_{j} ∈ BEn(π • t̄).

Proof By induction on |π| it can be shown that

⟨π, t̄⟩(i) = j & t_{i} ∈ BEn(t̄) implies (π • t̄)_{j} ∈ BEn(π • t̄). (1)

For the converse direction, we simply apply (1) to ⟨π^{−1}, π•t̄⟩(j) = i & (π• t̄)_{j} ∈ BEn(π • t̄). □

When two sequences t̄ and t̄′ have the same length, are equally labelled, and have the same permutations, they obviously represent isomorphic pomsets. This leads to the following definition.

Definition B.5 For t̄∈ Seqs(X) and t̄′ ∈ Seqs(X′) we define

t̄ iso t̄′ iff |t̄| = |t̄′| & ∀i. (ℓ(t_{i}) = ℓ′(t′_{i})) & Π_{X}(t̄) = Π_{X′}(t̄′).

Definition B.6 Let t̄, r̄ ∈ Seqs(X). Define t̄ ≃ r̄ iff there exists a permutation π such that π • t̄ = r̄. Furthermore, if t̄′, r̄′ ∈ Seqs(X′) and π • t̄′ = r̄′, we write (t̄, t̄′) ≃ (r̄, r̄′).

Lemma B.7 Suppose π • t̄ = r̄ and π • t̄′ = r̄′, and assume ⟨π, t̄⟩(i) = j and, similarly, ⟨π, t̄′⟩(i) = j. Then

(δ(i, t̄), δ(i, t̄′)) ≃ (δ(j, r̄), δ(j, r̄′)),

provided all deletions are well-defined.

Proof Induction in |π|. □

Corollary B.8 With the assumptions of the previous lemma,

δ(i, t̄) iso δ(i, t̄′) implies δ(j, r̄) iso δ(j, r̄′).

A Pom_{L}-open morphism f : X → X′ extends to a function Seqs(X) → Seqs(X′) in the obvious way. By abuse of notation, this function will also be denoted by f. We can now state the fact that Pom_{L}-open maps respect permutations.

Lemma B.9 If f : X → X′ is Pom_{L}-open, t̄ ∈ Seqs(X), and π ∈ ω^{∗}, then

π • t̄ is defined iff π • f(t̄) is defined,

and when both are defined,

f(π • t̄) = π • f(t̄).

Proof The two statements are proved simultaneously by induction on |π| using the group action property of •. The kernel of the argument is that open maps respect completion of independence squares. □

B.3 From Pom_{L}-bisimilarity to δ-bisimilarity

Before turning to the proof that ∼_{Pom_{L}} ⊆ ∼_{δ}, we notice that backwards enablings can be expressed in terms of permutations. Using Axiom 3 of Definition 2.2 it is easy to see that t_{i} ∈ BEn(t̄) iff [n − 2, …, i + 1, i] is a permutation of t̄. Furthermore, δ(i, t̄) is the one-step prefix of [n − 2, …, i + 1, i] • t̄.

Proposition B.10 ∼_{Pom_{L}} ⊆ ∼_{δ}.

Proof Suppose X and X′ are Pom_{L}-bisimilar. Then there is a transition system with independence Y and a span of Pom_{L}-open maps:

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

26  B.4 From iso-δ-bisimilarity to Pom_{L}-bisimilarity

Using the extensions of f and f′ to sequences, we now define a relation T ⊆ Seqs(X) × Seqs(X′) by

T = {(f(r̄), f′(r̄)) | r̄ ∈ Seqs(Y)}.

The claim is now that T is a δ-bisimulation. There are three axioms to check.

A_{init}: Trivial.

A_{bisim}: Suppose t̄ T t̄′ and t̄t ∈ Seqs(X). Then there exists r̄ ∈ Seqs(Y) such that t̄ = f(r̄) and t̄′ = f′(r̄). Since f is zig-zag and src(t) = tgt(t̄) = tgt(f(r̄)) = f(tgt(r̄)) there is a transition r such that r̄r ∈ Seqs(Y) and f(r) = t. Define t′ = f′(r). Then f(r̄r) = t̄t and f′(r̄r) = t̄′t′ so we conclude that t̄t T t̄′t′. Obviously, ℓ′(t′) = ℓ(t). The proof of the second part of the axiom is similar and therefore omitted.

A_{δ}: Let t̄ T t̄′ and assume t_{i} ∈ BEn(t̄). Choose r̄ such that t̄= f(r̄) and t̄′ = f′(r̄). Using the above characterization of t_{i} ∈ BEn(t̄) we see that π = [n − 2, …, i + 1, i] is a permutation of t̄. Lemma B.9 now states that

\begin{matrix}f(π • r̄) = π • f(r̄) = π • t̄ and \\ f′(π • r̄) = π • f′(r̄) = π • t̄′. \end{matrix}

Especially, π • t̄′ is defined, ensuring t′_{i} ∈ BEn(t̄′). Moreover, we see that π•t̄T π•t̄′ and since T is obviously closed under simultaneous prefix, we conclude that δ(i, t̄) T δ(i, t̄′), as required. By symmetry, this completes the proof of A_{δ}.

□

B.4 From iso-δ-bisimilarity to Pom_{L}-bisimilarity

As earlier mentioned, an iso-δ-bisimulation is just a δ-bisimulation which also respects isomorphism:

Definition B.11 A relation T ∈ Seqs(X) × Seqs(X′) is an iso-δ-simu-lation between X and X′ iff it is a δ-bisimulation which satisfies the following axiom:

A_{iso} t̄ T t̄′ ⇒ t̄ iso t̄′ We write X ∼_{iso-δ} X′ iff there is an iso-δ-bisimulation between X and X′, and say that X and X′ are iso-δ-bisimilar.

In the proof that an iso-δ-bisimulation induces a span of Pom_{L}-open maps, we need the iso-δ-bisimulation to be ≃-closed. But this is no problem, as the ≃-closure of any iso-δ-bisimulation is itself an iso-δ-bisimulation.

Lemma B.12 Let T be an iso-δ-bisimulation. Then the ≃-closure

{(r̄, r̄′) | ∃(t̄, t̄′) ∈ T . (t̄, t̄′) ≃ (r̄, r̄′)}

is an iso-δ-bisimulation, too.

Proof Only the axiom A_{δ} can cause troubles. But fortunately, we are rescued by Lemma B.4 and Lemma B.7. □

Proposition B.13 ∼_{iso-δ} ⊆ ∼_{Pom_{L}}.

Proof Let T ⊆ Seqs(X)×Seqs(X′) be an iso-δ-bisimulation. According to Lemma B.12 we can without loss of generality assume that T is ≃- closed. As a candidate for a common domain of a span of Pom_{L}-open maps, we define the following structure which will be proved to be a transition system with independence. Define

Y = (S_{Y} , i_{Y} , L, Tran_{Y} , I_{Y}),

where

• S_{Y} = {[(t̄, t̄′)]_{≃} | t̄ T t̄′}, i.e. ≃-equivalence classes^{2},

• i_{Y} = [(ε, ε)], and

• Tran_{Y} is defined by

y_{0}⟶^{a}y_{1} iff ∃t̄, t̄′, s_{1}, s′_{1}. (y_{0} = [(t̄, t̄′)] & y_{1} = [(t̄(s_{0}⟶^{a}s_{1}), t̄′(s′_{0}⟶^{a}s′_{1}))]).

Before defining I_{Y} we introduce “projection” morphisms f : Y → X and f′ : Y → X′ as follows:

f([(t̄, t̄′)]) = tgt(t̄) and f′([(t̄, t̄′)]) = tgt(t̄′).

2For convenience we shall from now on drop subscripts ≃.

Thus, every transition [(t̄, t̄′)]⟶^{a}[(t̄(s_{0}⟶^{a}s_{1}), t̄′(s′_{0}⟶^{a}s′_{1}))] = y_{0}⟶^{a}y_{1} of Y

induces transitions s_{0}⟶^{a}s_{1} = f(y_{0})⟶^{a}f(y_{1}) and s′_{0}⟶^{a}s′_{1} = f′(y_{0})⟶^{a}f′(y_{1})

of X and X′, respectively. Since also f([ε, ε)]) and f′([ε, ε)]) denote the initial states of X and X′, respectively, f and f′ are clearly well-defined morphisms. Using the extensions of f and f′ to transitions we are now able to express when two transitions in Y are independent:

• r_{0} I_{Y} r_{1} iff f(r_{0}) I_{X} f(r_{1}) & f′(r_{0}) I_{X′} f′(r_{1}).

When it is clear from the context which transition system we refer to, we will drop the subscripts. It should be noticed that exactly T being ≃-closed ensures the well-definedness of the components of Y.

We now show that Y is a transition system with independence and that f and f′ are Pom_{L}-open morphisms.

Y is a transition system with independence: Before proving the characterizing axioms we notice that the relations ≺_{Y} and ∼_{Y} between transitions in Y can be expressed by the corresponding relations in X and X′: For any transitions r_{0} and r_{1} in Y, we have

r_{0} ≺_{Y} r_{1} iff f(r_{0}) ≺_{X} f(r_{1}) & f′(r_{0}) ≺_{X′} f′(r_{1}),  (2)

and similarly for ∼_{Y}:

r_{0} ∼_{Y} r_{1} iff f(r_{0}) ∼_{X} f(r_{1}) & f′(r_{0}) ∼_{X′} f′(r_{1}).  (3)

We are now ready to prove the axioms.

1. is a consequence of (3) in conjunction with Axiom (1) holding for X and X′.

2. Assume two independent consequtive transitions in Y,

\begin{matrix}[(t̄, t̄′)] ⟶^{a} [(t̄(s⟶^{a}s_{1}), t̄′(s′⟶^{a}s′_{1}))] \\ ⟶^{b} [(t̄(s⟶^{a}s_{1})(s_{1}⟶^{b}u), t̄′(s′⟶^{a}s′_{1})(s′_{1}⟶^{b}u′))]. \end{matrix}

Since independence in Y is defined component-wise, there are independence squares

[figure: \begin{aligned}& s \\ s_{1} & I & s_{2} \\ & u \end{aligned}; a; b; b; a] and [figure: \begin{aligned}& s′ \\ s′_{1} & I & s′_{2} \\ & u′ \end{aligned}; a; b; b; a]

in X and X′, respectively. By definition of S_{Y}, we see that

t̄(s⟶^{a}s_{1})(s_{1}⟶^{b}u) T t̄′(s′⟶^{a}s′_{1})(s′_{1}⟶^{b}u′),

and since T is δ-closed, it must be the case that

t̄(s⟶^{b}s_{2}) T t̄′(s′⟶^{b}s′_{2})

where s_{2} and s′_{2} are determined uniquely above. Hence the equivalence class [(t̄(s⟶^{b}s_{2}), t̄′(s′⟶^{b}s′_{2}))] is a state of Y and, obviously, there are transitions

\begin{matrix}[(t̄, t̄′)] ⟶^{b} [(t̄(s⟶^{b}s_{2}), t̄′(s′⟶^{b}s′_{2}))] \\ ⟶^{a} [(t̄(s⟶^{b}s_{2})(s_{2}⟶^{a}u), t̄′(s′⟶^{b}s′_{2})(s′_{2}⟶^{a}u′))]. \end{matrix}

Now, since s⟶^{a}s_{1} I s_{1}⟶^{b}u and s′⟶^{a}s′_{1} I s′_{1}⟶^{b}u′, it follows that

\begin{matrix}(t̄(s⟶^{a}s_{1})(s_{1}⟶^{b}u), t̄′(s′⟶^{a}s′_{1})(s′_{1}⟶^{b}u′)) \\ ≃ (t̄(s⟶^{b}s_{2})(s_{2}⟶^{a}u), t̄′(s′⟶^{b}s′_{2})(s′_{2}⟶^{a}u′)). \end{matrix}

This completes the square in Y. The required independencies follow immediately, as I_{Y} is defined component-wise.

3. Both axioms are easy to establish using (2) and the definition of I_{Y}.

This finishes the proof that Y is a transition system with independence. It remains to show that f and f′ are Pom_{L}-open morphisms. The arguments are identical, so we present only the proof that f is Pom_{L}-open.

f is zig-zag: Let f([(t̄, t̄′)])⟶^{a}s be a transition in X where, by definition, f([(t̄, t̄′)]) = tgt(t̄). Since t̄ T t̄′, there exists a transition tgt(t̄′)⟶^{a}s′ for some s such that

t̄(tgt(t̄)⟶^{a}s) T t̄′(tgt(t̄′)⟶^{a}s′).

30  B.5 From Γ-equivalence to iso-δ-bisimilarity

Thus [(t̄(tgt(t̄)⟶^{a}s), t̄′(tgt(t̄′)⟶^{a}s′))] is a state of Y which by f is mapped to s. Moreover, there is an a-transition from [(t̄, t̄′)] into it. This proves that f is zig-zag. f reflects consecutive independence: Suppose

\begin{matrix}[(t̄, t̄′)] ⟶^{a} [(t̄(s⟶^{a}s_{1}), t̄′(s′⟶^{a}s′_{1}))] \\ ⟶^{b} [(t̄(s⟶^{a}s_{1})(s_{1}⟶^{b}u), t̄′(s′⟶^{a}s′_{1})(s′_{1}⟶^{b}u′))] \end{matrix}

and assume s⟶^{a}s_{1} I_{X} s_{1}⟶^{b}u. Since

t̄(s⟶^{a}s_{1})(s_{1}⟶^{b}u) T t̄′(s′⟶^{a}s′_{1})(s′_{1}⟶^{b}u′)

and T respects iso, we also have s′⟶^{a}s′_{1} I_{X′} s′_{1}⟶^{b}u′. Then, by definition of I_{Y}, the above transitions in Y must be independent, too.

We have now constructed a transition system with independence and equipped it with Pom_{L}-open morphisms to X and X′. This finishes the proof of the proposition. □

B.5 From Γ-equivalence to iso-δ-bisimilarity

The key observation underlying this result is that any winning strategy in the backtracking game Γ(X, X′) maintains isomorphisms between observations of the two systems.

Lemma B.14 A winning strategy σ in Γ(X, X′) respects iso in the sense that if p · (t̄, t̄′) is a play respecting σ, then t̄ iso t̄′.

Proof Assume towards contradiction that there are plays p · (t̄t, t̄′t′) respecting σ such that ¬(t̄t iso t̄′t′). Choose p, t̄t, t̄′t′ with this property and such that t̄t is of minimal length with that property. Since every play respects length and labels, there are sequences iπ ∈ ω^{∗} such that

iπ • t̄t defined & iπ • t̄′t′ undefined  (4)

(or vice versa). Choose iπ of minimal length with this property. Then, furthermore,

π • t̄t defined & π • t̄′t′ defined.  (5)

Suppose |t̄t| = n and write

\begin{matrix}π • t̄t = r_{0}r_{1} ⋯ r_{i}r_{i+1} ⋯ r_{n−1} and \\ π • t̄′t′ = r′_{0}r′_{1} ⋯ r′_{i}r′_{i+1} ⋯ r′_{n−1}, \end{matrix}  (6)

where, by (4) and (5), r_{i} I r_{i+1} and ¬(r′_{i} I r′_{i+1}).

We will now argue that in (6), i = n − 2, meaning that r_{i+1} and r′_{i+1} are the last transitions. Assume towards contradiction that i < n − 2 and let k be such that ⟨π, t̄t⟩(k) = n − 1 and hence ⟨π, t̄′t′⟩(k) = n − 1. Then, by Lemma B.4, (t̄t)_{k} is backwards enabled in t̄t making it possible for Opponent to do the backwards move

(t̄t, t̄′t′) > (k, δ(k, t̄t), t̄′t′).

Since σ is winning, Player is able match this move, and we end up in (δ(k, t̄t), δ(k, t̄′t′)). Now, since t̄t was chosen minimal, we see that δ(k, t̄t) iso δ(k, t̄′t′). Since r_{i} I r_{i+1} and ¬(r′_{i} I r′_{i+1}), the only values of s for which δ(s, r̄) iso δ(s, r̄′) can be true, are i and i+1. By Corollary B.8, δ(n − 1, r̄) iso δ(n − 1, r̄′), so we conclude that n − 1 ∈ {i, i + 1}. But n − 1 = i contradicts i + 1 being a legal index of r̄. Hence, n − 1 = i + 1 or, equivalently, i = n − 2.

Finally we can now rewrite (6) using the information that i = n − 2:

\begin{matrix}π • t̄t = r_{0}r_{1} ⋯ r_{i}r_{i+1} and \\ π • t̄′t′ = r′_{0}r′_{1} ⋯ r′_{i}r′_{i+1}. \end{matrix}

Let now l be such that ⟨π, t̄t⟩(l) = i and hence ⟨π, t̄′t′⟩(l) = i. Since r_{i} I r_{i+1}, it follows from Lemma B.4 that (t̄t)_{l} is backwards enabled in t̄t. Hence, Opponent can do the backwards move

(t̄t, t̄′t′) > (l, δ(l, t̄t), t̄′t′).

But, since ¬(r′_{i} I r′_{i+1}), it follows from Lemma B.4 that (t̄′t′)_{l} is not backwards enabled in t̄′t′, so Player is stuck. This contradicts σ being winning. □

The proof of the proposition below is now straightforward.

Proposition B.15 ∼_{Γ} ⊆ ∼_{iso-δ}.

Proof Let σ be a winning strategy in Γ(X, X′) and assume, in accordance with Lemma B.14, that σ respects iso. Define a relation T ⊆ Seqs(X) × Seqs(X′) by

t̄ T t̄′ iff p · (t̄, t̄′) ∈ P lays(σ, τ) for some play p and counter-strategy τ.

We show that T is an iso-δ-bisimulation:

A_{iso}: t̄ T t̄′ ⇒ t̄ iso t̄′ follows directly from the fact that σ respects iso.

A_{bisim}: Suppose t̄ T t̄′ and t̄t ∈ Seqs(X). Let p and τ be such that p · (t̄, t̄′) ∈ Plays(σ, τ) and define

τ′ = [(t̄t, t̄′)/p · (t̄, t̄′)],

which is the function equal to τ everywhere except at p · (t̄, t̄′) at which it yields (t̄t, t̄′). Now^{3},

p′ = p · (t̄, t̄′) · (t̄t, t̄′) ∈ Plays(σ, τ′),

forcing σ to be defined on p′. Inspecting the rules of Γ(X, X′) we see that σ(p′) equals (t̄t, t̄′t′) for some t′. But then t̄t T t̄′t′, as required.

A_{δ}: Let t̄ T t̄′ and assume t_{i} ∈ BEn(t̄). Choose p and τ such that p · (t̄, t̄′) ∈ Plays(σ, τ) and define

τ′′ = [(i, δ(i, t̄), t̄′)/p · (t̄, t̄′)].

Observe that

p′′ =^{def} p · (t̄, t̄′) · (i, δ(i, t̄), t̄′) ∈ Plays(σ, τ′′).

Being winning, σ is able to respond to this move with σ(p′′) = (δ(i, t̄), δ(i, t̄′)). Hence, t′_{i} ∈ BEn(t̄′), by the definition of Γ(X, X′). Furthermore, δ(i, t̄) T δ(i, t̄′), since p′′·(δ(i, t̄), δ(i, t̄′)) ∈ Plays(σ, τ). By a symmetric argument, this finishes the proof. □

3Here we use that strategies are defined on positions rather that configurations.

C Proofs From Section 4

Proposition C.1 (Proposition 4.5 restated) If two transition systems with independence are Pom_{L}-bisimilar, then they are also Assn-equivalent.

Proof Let T be a δ-bisimulation between X and X′. By structural induction on assertions we show that for all A ∈ Assn, t̄∈ Seqs(X), and t̄′ ∈ Seqs(X′),

t̄ T t̄′ ⇒ (t̄⊧_{X} A ⇔ t̄′ ⊧_{X′} A).  (7)

¬A:

t̄ T t̄′ ⇒ (t̄⊧_{X} A ⇔ t̄′ ⊧_{X′} A)  (inductively)
⇔ (t̄|̸=_{X} A ⇔ t̄′ |̸=_{X′} A)
⇔ (t̄⊧_{X} ¬A ⇔ t̄′ ⊧_{X′} ¬A) (by definition)

⋀_{j∈J} A_{j}:

t̄ T t̄′ ⇒ ∀j ∈ J. (t̄⊧_{X} A_{j} ⇔ t̄′ ⊧_{X′} A_{j})  (inductively)
⇒ (∀j ∈ J. (t̄⊧ A_{j}) ⇔ ∀j ∈ J. (t̄′ ⊧_{X′} A_{j}))
⇔ (t̄⊧_{X} ⋀_{j∈J} A_{j} ⇔ t̄′ ⊧_{X′} ⋀_{j∈J} A_{j})  (by definition)

⟨a⟩A: Suppose t̄ T t̄′ and t̄ ⊧_{X} ⟨a⟩A. Then there exists r̄ such that t̄⟶^{a}r̄ and r̄ ⊧_{X} A. Since t̄ T t̄′ there exists r̄′ such that t̄′⟶^{a}r̄′ and r̄ T r̄′. By the induction hypothesis, r̄′ ⊧_{X′} A, so we conclude that t̄′ ⊧_{X′} ⟨a⟩A.

◯ a A: Suppose t̄ T t̄′ and t̄ ⊧_{X} ◯ a A. Then there exists t_{i} ∈ BEn(t̄) such that ℓ(t_{i}) = a and δ(i, t̄) ⊧_{X} A. Since t̄ T t̄′ we also have t′_{i} ∈ BEn(t̄′) and δ(i, t̄) T δ(i, t̄′), so inductively, δ(i, t̄′) ⊧_{X′} A. Since T respects labels, t̄′ ⊧_{X′} ◯ a A, as required.

This finishes the proof of (7). The proposition follows by taking t̄= t̄′ = ε. □

Lemma C.2 Suppose X has no auto-concurrency and let t̄ ∈ Seqs(X). Then, if t_{i}, t_{j} ∈ BEn(t̄) and ℓ(t_{i}) = ℓ(t_{j}), the transitions are equal, i.e. i = j.

Proof Assume towards contradiction that i ≠ j. Without loss of generality we may assume that i < j. Since t_{i} ∈ BEn(t̄), by definition, t_{i} I t_{k} for all k > i. This clearly contradicts X having no auto-concurrency. □

For non-auto-concurrent systems, there is a simpler game, Γ′, characterizing Pom_{L}-bisimilarity. Backtracking on indices can be substituted by backtracking on labels, yielding rules like

(t̄, t̄′) > (a, r̄, t̄′) if r̄ ⇝^{a} t̄,

where the a is a directive to Player to play backwards with an a-move in the longer of the sequences. More concretely, Player must reply with an application of the rule

(a, r̄, t̄′) > (r̄, r̄′) if r̄′ ⇝^{a} t̄′.

Say that two transition systems with independence X and X′ are Γ′- equivalent iff Player has a winning strategy in Γ′(X, X′).

Proposition C.3 Two non-auto-concurrent transition systems with independence are Γ′-equivalent iff they are Γ-equivalent.

Proof Let X and X′ be transition systems with independence. First we notice that there is a bijection C : Pos(Γ(X, X′)) → Pos(Γ′(X, X′)) defined inductively in length of the position:

C(ε, ε) = (ε, ε)
C(p · (t̄, t̄′)) = C(p) · (t̄, t̄′)
C(p · (t̄t, t̄′)) = C(p) · (t̄t, t̄′)
C(p · (t̄, t̄′t′)) = C(p) · (t̄, t̄′t′)
C(p · (t̄, t̄′) · (i, δ(i, t̄), t̄′)) = C(p · (t̄, t̄′)) · (ℓ(t_{i}), δ(i, t̄), t̄′)
C(p · (t̄, t̄′) · (i, t̄, δ(i, t̄′))) = C(p · (t̄, t̄′)) · (ℓ(t′_{i}), t̄, δ(i, t̄′))

Using that the plays of Γ(X, X′) respect labels (i.e. that whenever (t̄, t̄′) ∈ Pos(Γ(X, X′)), ∀i. (ℓ(t_{i}) = ℓ(t′_{i}))), it is easy to show that C is well-defined. The inverse function C^{−1} of C is given inductively by very similar clauses. As an example, let us see how C^{−1}(p · (t̄, t̄′) · (a, r̄, t̄′)) (where r̄ ⇝^{a} t̄) is defined. By definition 4.1, there is an index i such that t_{i} ∈ BEn(t̄), ℓ(t_{i}) = a, and r̄ = δ(i, t̄). Moreover, this index is unique. We can thus define

C^{−1}(p · (t̄, t̄′) · (a, r̄, t̄′)) = C^{−1}(p · (t̄, t̄′)) · (i, δ(i, t̄), t̄′)).

The well-definedness of C^{−1} follows from Lemma C.2 using that plays of Γ(X, X′) respect labels. It is straightforward to show that C and C^{−1} are each others inverse.

For one direction, assume that σ is a winning strategy in Γ(X, X′). We then define a winning strategy σ′ in Γ(X, X′) as follows: For each p ∈ Pos(Γ′(X, X′)), let

σ′(p) = σ(C^{−1}(p)).

Using the bijection, it can be shown that σ′ is a winning strategy. The other direction is managed in a similar way. □

Proposition C.4 (Proposition 4.7 restated) If two non-auto-concur-rent transition systems with independence are Assn-equivalent, then they are also Pom_{L}-bisimilar.

Proof Assume towards contradiction that X and X′ are Assn-equivalent but not Pom_{L}-bisimilar. Then there can be no winning strategy in the modified game Γ′(X, X′). Hence, by Proposition 3.1, there is a winning counter-strategy τ in Γ′(X, X′). Using τ, we construct an assertion A(p) for any play p such that

• p respects τ, and

• λ(p) = O.

Define the following partial order on such plays:

p′ ≺ p iff ∃c, c′. (p′ = p · c · c′).

As τ is winning, there can be no infinite plays respecting τ. Hence, ≺ is well-founded. We now define A(p) by well-founded recursion on p. Let p be a play of the above kind and suppose A(p′) is defined for all p′ ≺ p. Since p respects τ, and λ(p) = O, τ(p) must be defined – otherwise τ would not be winning. Assuming the last configuration of p is (t̄, t̄′), consider now the following cases of τ(p):

τ(p) = (r̄, t̄′) where t̄⟶^{a}r̄:

A(p) = ⟨a⟩(⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)})

τ(p) = (t̄, r̄′) where t̄′⟶^{a}r̄′:

A(p) = ¬⟨a⟩(⋀{¬A(p′) | ∃r̄. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)})

τ(p) = (a, r̄, t̄′) where r̄ ⇝^{a} t̄:

A(p) = ◯ a (⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)})

τ(p) = (a, t̄, r̄′) where r̄′ ⇝^{a} t̄′:

A(p) = ¬◯ a (⋀{¬A(p′) | ∃r̄. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)})

The claim is now that if p is a play of the above kind, and the last configuration of p is (t̄, t̄′), then

t̄⊧_{X} A(p) & t̄′ ⊧_{X′} ¬A(p).  (8)

Instantiating p to (ε, ε) yields ⊧_{X} A(ε, ε) and ⊧_{X′} ¬A(ε, ε) which contradicts the assumption X ∼_{Assn} X′.

The proof of the claim is by well-founded induction on p. We consider the following four cases of τ(p):

τ(p) = (r̄, t̄′) where t̄⟶^{a}r̄: To establish t̄⊧_{X} A(p) we show

r̄ ⊧_{X} ⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)}.

Assume p′ = p · τ(p) · (r̄, r̄′) ≺ p for some r̄′. We are then required to show r̄ ⊧_{X} A(p′). But this follows inductively, since p′ respects τ and the last configuration of p′ is (r̄, r̄′). To establish t̄′ ⊧_{X′} ¬A(p) we assume towards contradiction that t̄′ ⊧_{X′} A(p). Then there exists a transition sequence r̄′ such that

t̄′⟶^{a}r̄′ and

r̄′ ⊧_{X′} ⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)}.

Now there is a move τ(p) >(r̄, r̄′), so p′ = p·τ(p)·(r̄, r̄′) ≺ p. Hence, r̄′ ⊧_{X′} A(p′), but this contradicts the induction hypothesis.

τ(p) = (t̄, r̄′) where t̄′⟶^{a}r̄′: Similar to the previous case.

τ(p) = (a, r̄, t̄′) where r̄ ⇝^{a} t̄: To establish t̄⊧_{X} A(p) we simply show

r̄ ⊧_{X} ⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)}.

Suppose p′ = p · τ(p) · (r̄, r̄′) ≺ p. We are then required to show r̄ ⊧_{X} A(p′), but this follows directly from the induction hypothesis.

We still need to show t̄′ ⊧_{X′} ¬A(p). Assume towards contradiction that t̄′ ⊧_{X′} A(p). Then there exists r̄′ such that r̄′ ⇝^{a} t̄′ and

r̄′ ⊧_{X′} ⋀{A(p′) | ∃r̄′. (p′ = p · τ(p) · (r̄, r̄′) ≺ p)}.

Now there is a move τ(p) >(r̄, r̄′), so, in fact, p′ = p·τ(p)·(r̄, r̄′) ≺ p. Hence, r̄′ ⊧_{X′} A(p′), which contradicts the induction hypothesis.

τ(p) = (a, t̄, r̄′) where r̄′ ⇝^{a} t̄′: Symmetric. □

Recent Publications in the BRICS Report Series

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

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

RS-94-3 Uffe H. Engberg and Glynn Winskel. Linear Logic on Petri Nets. February 1994, 54 pp.

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

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

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