Foundations of Software Technology and Theoretical Computer Science: 22nd Conference, Proceedings, M. Agrawal, A. Seth (eds.) Springer Lecture Notes in Computer Science 2556 (2002) 289–300.

Hereditary history preserving bisimulation is decidable for trace-labelled systems^{⋆}

Madhavan Mukund

Chennai Mathematical Institute, 92 GN Chetty Road, Chennai 600017, India

                         Email: madhavan@cmi.ac.in

Abstract. Hereditary history preserving bisimulation is a natural extension of bisimulation to the setting of so-called “true” concurrency. Somewhat surprisingly, this extension turns out to be undecidable, in general, for finite-state concurrent systems. In this paper, we show that for a substantial and useful class of finite-state concurrent systems— those whose semantics can be described in terms of Mazurkiewicz traces— hereditary history preserving is decidable.

1 Introduction

While branching time semantics is relatively well understood in the interleaved approach to the semantics of concurrent systems, the situation is not so clear when labelled partial orders are used to record the behaviour of such systems. If no restriction is placed on the structure of a concurrent system, the interplay between nondeterminism and concurrency results in many seemingly simple problems becoming computationally intractable.

An example of this is the problem of checking whether two finite-state systems are equivalent with respect to the concurrency-preserving branching-time behavioural equivalence known as hereditary history preserving bisimulation. Hereditary history preserving bisimulation is a natural extension of bisimulation, as defined by Park and Milner [11, 13], from a setting where concurrency is equated with nondeterministic interleaving to a richer setting where nondeterminism and concurrency are represented explicitly and independently. Hereditary history preserving bisimulation was first defined by Bednarczyk [1], but became more well known when it reappeared as a natural construction in a general, categorical approach to nondeterminism and concurrency arising out of the work of Winskel and Nielsen[7, 17].

Hereditary history preserving bisimulation requires two concurrent systems to retain the same nondeterministic choices as they evolve, as in conventional bisimulation. In addition, at every state, each of the systems also has to faithfully simulate all steps—sets of pairwise independent actions—performed by other system. Although this seems to be a fairly innocuous extension, the repercussions are quite severe. It turns out that history preserving bisimulation is, in general, undecidable for finite-state concurrent systems [8].

⋆ Partially supported by IFCPAR Project 2102-1 (ACSMV).

A few positive results have been obtained regarding hereditary history preserving bisimulation. In [12], a game-theoretic formulation is presented, along with a characterization in terms of a Hennessy-Milner style modal logic with past modalities. The decidability question was investigated in [5] where some very restricted positive results were obtained.

Earlier, a weaker notion of history preserving bisimulation had been proposed in [3, 15, 16]. Here, too, the two systems have to progressively simulate each others’ concurrent steps. However, the bisimulation is built up one action at a time, so each interleaving of a concurrent step in one system may be simulated by a different, incompatible, step in the other system. Thus, from the standpoint of faithfully preserving concurrency and nondeterminism, this notion is slightly unsatisfactory. The decidability of this variety of bisimulation was established in [6].

In this paper, we examine the decidability question afresh for a restricted class of concurrent systems—those whose behaviours can be described by Mazurkiewicz traces. Our main result is that hereditary history preserving bisimulation is decidable for this class of systems.

Mazurkiewicz traces [10] are labelled partial orders generated by independence alphabets of the form (Σ, I), where I is a static independence relation over Σ. If (a, b) ∈ I, a and b are deemed to be independent actions that may occur concurrently in any context where they are jointly enabled. Traces are a natural formalism for describing the behaviour of various static networks of communicating finite-state agents as modelled by Petri nets [14] or communicating finite-state automata [18]. Hence, our positive result is applicable to a substantial and useful subclass of finite-state concurrent systems.

The paper is organized as follows. We begin with some basic definitions about labelled Petri nets, the system model that we work with in this paper. In Section 3 we define hereditary history preserving bisimulation. In the next section, we identify the subclass of systems that we focus on—those whose semantics can be defined using Mazurkiewicz traces. In Section 5, we show that hereditary history preserving bisimulation is equivalent to a notion of step bisimulation on step transition systems. This characterization is used to derive the main decidability result in Section 6. We conclude with a brief discussion.

2 Preliminaries

We use labelled 1-safe Petri nets as our basic model of finite-state concurrent systems. This choice of model is not important: we could have, instead, worked with any other model that has an explicit notion of independence or concurrency built in, such as labelled asynchronous transition systems [2], asynchronous automata [18] or transition systems with independence [17]. Nets A net is a quadruple (S, T, F, M_{in}) where:

– S is a finite, non-empty set of places.

– T is a finite, non-empty set of transitions.

– F ⊆ (S × T) ∪ (T × S) is the flow relation.

– M_{in} : S → ℕ_{0} is the initial marking, where ℕ_{0} = {0, 1, 2, …}.

As usual, for x in S ∪ T, we use ^{•}x to denote the set {y ∈ S ∪ T | (y, x) ∈ F } and x^{•} to denote the set {y ∈ S ∪ T | (x, y) ∈ F }. Reachable markings A marking of (S, T, F, M_{in}) is a function M : S → ℕ_{0} and corresponds to a global state of the system. A transition t is enabled at marking M, denoted M ⟶^{t}, if M(s) > 0 for all s ∈ ^{•}t. When t occurs, M evolves to a new marking M′, written M ⟶^{t} M′, where

∀s ∈ S. M′(s) = \{ \begin{matrix}M(s) − 1 & if s ∈ (^{•}t − t^{•}), \\ M(s) + 1 & if s ∈ (t^{•} −^{•}t), \\ M(s) & otherwise. \end{matrix}

Notice that M′ is uniquely fixed by M and t. Let w = t_{1}t_{2} … t_{k}. We write

M ⟶^{w} M′ to indicate that M ⟶^{t_{1}} M_{1} ⟶^{t_{2}} M_{2} ⋯ M_{k−1} ⟶^{t_{k}} M′. Similarly,

M ⟶^{w} denotes that there exists M′ such that M ⟶^{w} M′.

Let M_{0} be a marking of (S, T, F, M_{in}). The set of markings reachable from M_{0}, denoted R(M_{0}) is defined inductively as follows:

– M_{0} ∈ R(M_{0}).

– If M ∈ R(M_{0}) and M ⟶^{t} M′, then M′ ∈ R(M_{0}).

1-safe nets The net (S, T, F, M_{in}) is said to be 1-safe if for all M ∈ R(M_{in}), for all s ∈ S, M(s) ≤ 1. Clearly, if N is 1-safe, then its global state space is finite since the number of distinct markings in R(M_{in}) is bounded by 2^{|T |}. In this paper, we assume that every net we consider is 1-safe. Labelled nets Let Σ be a set of actions. A Σ-labelled net is a structure N = (S, T, F, M_{in}, λ) where (S, T, F, M_{in}) is a (1-safe) net and λ : T → Σ is a labelling function. Independence of transitions We say that transitions t_{1} and t_{2} are independent if they have disjoint neighbourhoods—that is, (^{•}t_{1} ∪ t_{1}^{•}) ∩ (^{•}t_{2} ∪ t_{2}^{•}) = ∅. We write t_{i}I_{N}t_{j} to denote that t_{i} and t_{j} are independent in N. If ¬(t_{i}I_{N}t_{j}) we write t_{i}D_{N}t_{j}, denoting that t_{i} and t_{j} are dependent. Independent transitions satisfy forward and sideways diamond properties. Let t_{1} and t_{2} be independent. If M ⟶^{t_{1}} M_{1} and M ⟶^{t_{2}} M_{2} then there exists M′ such that M_{1} ⟶^{t_{2}} M′ and M_{2} ⟶^{t_{1}} M′. Further, if M ⟶^{t_{1}} M_{1} ⟶^{t_{2}} M′ then there exists M_{2} such that

M ⟶^{t_{2}} M_{2} ⟶^{t_{1}} M′.

Runs Let N = (S, T, F, M_{in}, λ) be a labelled net. Each transition sequence w = t_{1}t_{2} … t_{k} such that M_{0} ⟶^{w} M_{w} gives rise to a labelled partial order that we call a run. The run po(w) associated with w is a triple (E, ≤, τ) where E is a set of events partially ordered by ≤ and τ : E → T is a labelling function. Each event in E corresponds to a transition from w and is labelled by the underlying transition. The partial order ≤ is the reflexive, transitive closure of the relation e_{i} ≺ e_{j} ⇔ i < j ∧ t_{i}D_{N}t_{j}, where τ(e_{i}) = t_{i} and τ(e_{j}) = t_{j}.

More formally, let w = t_{1}t_{2} … t_{k}. Then, po(w) = (E, ≤, τ) such that:

(i) E = {1, 2, …, k}. (ii) For each i ∈ E, τ(i) = t_{i}. (iii) For i, j ∈ E, if i and j are unordered in po(w) then t_{i}I_{N}t_{j}. (iv) For i, j ∈ E, if i ⋖ j then t_{i}D_{N}t_{j}, where ⋖ = < \ <^{2} is the immediate

successor relation in po(w).

Let Runs(N) = {po(w) | w ∈ T^{∗}, M_{in} ⟶^{w}} denote the set of runs of N. With each run r ∈ Runs(N), we can associate a unique marking M_{r}, the global state of N after the computation r.

If r = po(w) and r′ = po(wt)—that is, r′ extends r by adding an event corresponding to the transition t—we denote r′ as r + t. If u = {t_{1}, t_{2}, …, t_{k}} is a set of pairwise independent transitions enabled at M_{r}, then we denote the run r + t_{1} + t_{2} + ⋯ + t_{k} by r + u.

For a run r = (E, ≤, τ), max(r) denotes the set of maximal events in E. Let r = po(w), where w = t_{1}t_{2} … t_{k}, and let j ∈ max(r). Then r − j denotes the run obtained by deleting the event j from r—that is, r − j = po(w′), where w′ = t_{1}t_{2} … t_{j−1}t_{j+1} … t_{k}.

Two runs are said to be isomorphic if they are isomorphic as labelled partial orders. We write r ≃ r′ to indicate that r and r′ are isomorphic runs.

For each net, the empty sequence of transitions ε gives rise to the empty run (∅, ∅, ∅). We use r_{∅} uniformly to denote the empty run for all nets.

3 History Preserving Bisimulations

For the rest of this section, fix a pair of labelled nets N_{i} = (S_{i}, T_{i}, F_{i}, M_{in}^{i}, λ_{i}), i ∈ {1, 2}, whose transitions are labelled by a common set of actions Σ. A history preserving bisimulation is a relation between the runs of N_{1} and the runs of N_{2} which asserts that the two systems have equivalent observable capabilities, even when we take concurrency into account.

We define history preserving bisimulations in terms of matched runs. Matched runs Let ρ = (E, ≤, τ_{1}, τ_{2}) be a partial order equipped with two labelling functions such that τ_{i} : E → T_{i}, i ∈ {1, 2}, labels each event in E with a transition from T_{i}. The structure (E, ≤, τ_{1}, τ_{2}) is a matched run of N_{1} and N_{2} if it satisfies the following conditions:

– ρ_{1} = (E, ≤, τ_{1}) is a run of N_{1} and ρ_{2} = (E, ≤, τ_{2}) is a run of N_{2}.

– For all e ∈ E, λ_{1}(τ_{1}(e)) = λ_{2}(τ_{2}(e)).

Let ρ and ρ′ be matched runs such that ρ′ extends ρ by k events with ρ′_{1} = ρ+u_{1} and ρ′_{2} = ρ_{2} + u_{2}, where u_{1} and u_{2} are pairwise disjoint subsets of size k of T_{1} and T_{2}, respectively. We denote ρ′ by ρ + ⟨u_{1}, u_{2}⟩. If u_{1} = {t_{1}} and u_{2} = {t_{2}} are singletons, we write ρ + ⟨t_{1}, t_{2}⟩ rather than ρ + ⟨{t_{1}}, {t_{2}}⟩.

Let e be a maximal event in the matched run ρ. Then ρ′ = ρ−e is the matched run obtained by deleting e from ρ. If u = {e_{1}, e_{2}, …, e_{k}} is a subset of maximal events in ρ, we write ρ − u to denote the run (((ρ − e_{1}) − e_{2}) − ⋯ − e_{k−1}) − e_{k} obtained by deleting all the events from u (clearly, the events in u may be removed in any order). Hereditary history preserving bisimulation A hereditary history preserving bisimulation between N_{1} = (S_{1}, T_{1}, F_{1}, M_{in}^{1}, λ_{1}) and N_{2} = (S_{2}, T_{2}, F_{2}, M_{in}^{2}, λ_{2}) is a set H of matched runs of the two nets such that:

(i) The empty matched run (∅, ∅, ∅, ∅) belongs to H. (ii) Let ρ = (E, ≤, τ_{1}, τ_{2}) ∈ H. For each transition t_{1} ∈ T_{1} enabled at M_{ρ_{1}}, there

is a transition t_{2} in T_{2} such that ρ + ⟨t_{1}, t_{2}⟩ ∈ H. (iii) Let ρ = (E, ≤, τ_{1}, τ_{2}) ∈ H. For each transition t_{2} ∈ T_{2} enabled at M_{ρ_{2}}, there

is a transition t_{1} in T_{1} such that ρ + ⟨t_{1}, t_{2}⟩ ∈ H. (iv) For each maximal event e in ρ, the matched run ρ − {e} is in H.

The first three clauses correspond to the weaker definition of history preserving bisimulations [3, 15, 16]. The last clause strengthens the definition by ensuring that the bisimulation extends concurrent steps in a uniform way, regardless of the order in which the concurrent step is executed. The weaker definition permits different interleavings of the same concurrent step to be simulated in different ways. (The original definition of hereditary history preserving bisimulation required all prefixes of a matched run to belong to the relation H. However, it was shown in [12] that is suffices to check the condition for the substructures obtained by deleting each of the maximal events in the given matched run.) Figure 1, taken from [5], illustrates the difference between the two definitions.

[figure: •; •; a; t_{2}; c; t_{3}; a; t_{1}; •; •; b; t_{4}; d; t_{6}; b; t_{5}; •; •; a; t′_{2}; c; t′_{3}; a; t′_{1}; •; •; b; t′_{4}; d; t′_{6}; b; t′_{5}] Fig. 1.

In this example, consider the step {t_{1}, t_{4}} in the net on the left. If we execute t_{1} before t_{4}, we can simulate this by t′_{1} followed by t′_{4}, preserving forward choices at each point. Similarly, if we execute t_{4} before t_{1}, we can simulate it by t′_{5} followed by t′_{2}. However, neither simulation is faithful to the original step and this is caught by the last clause in the definition of hereditary history preserving bisimulations—for instance, if we simulate t_{1}t_{4} by t′_{1}t′_{4}, we can “undo” the maximal events t_{1} and t′_{1} to reach markings in which a d-labelled transition is enabled on the right but not on the left.

The difficulty with establishing whether two labelled nets are hereditary history-preserving bisimilar is that the bisimulation is defined at the level of matched runs, which correspond to the infinite “unfolded” behaviours of the two nets. For normal sequential bisimulation, given a pair of finite transition systems, a bisimulation relation exists between their unfoldings if and only if a (finite) bisimulation relation exists between the states of the original system.

Every Petri net can be regarded as a labelled transition system whose states correspond to the (reachable) markings of the net. In general, a hereditary history preserving bisimulation at the level of matched runs cannot be “folded” down to a relation the level of markings, as demonstrated in Figure 2. These two nets are hereditary history preserving bisimilar. The markings {s_{3}, s_{4}} and {s′_{4}, s′_{5}} are not equivalent after executing {t_{2}, t_{3}} and {t′_{1}, t′_{3}}. However, if we reach the same markings after executing {t_{2}, t_{3}, t_{4}, t_{5}} and {t′_{2}, t′_{3}, t′_{4}, t′_{5}}, the markings do become equivalent.

[figure: •; s_{2}; •; s_{1}; b; t_{3}; a; t_{2}; a; t_{1}; s_{4}; s_{3}; c; t_{4}; s_{5}; c; t_{5}; •; s′_{2}; •; s′_{1}; b; t′_{3}; a; t′_{2}; a; t′_{1}; s′_{4}; s′_{3}; c; t′_{4}; s′_{5}; c; t′_{5}] Fig. 2.

4 Trace-labelled systems

Trace alphabets A trace alphabet is a pair (Σ, I), where I ⊆ Σ × Σ is an irreflexive and symmetric independence relation. The complement of I is denoted D and called the dependence relation.

The independence relation I induces a natural equivalence relation ∼ on words over Σ. Intuitively, two words are related by ∼ if we can go from one to another by repeatedly swapping adjacent independent letters. More formally, let ∼_{0} be the relation {(wabw′, wbaw′) | w, w′ ∈ Σ^{∗}, aIb}. Then ∼ is the reflexive, transitive closure of ∼_{0}. The equivalence classes generated by ∼ are called (Mazurkiewicz) traces. We denote the trace containing the word w by [w].

Trace-labelled nets Let (Σ, I) be a trace alphabet. A labelled net N = (S, T, F, M_{in}, λ) with λ : T → Σ is said to be trace-labelled if t_{i}I_{N}t_{j} ⇔ λ(t_{i})Iλ(t_{j}) for all pairs of transitions t_{i}, t_{j} ∈ T.

For trace-labelled nets, the partial order structure of a run is determined solely by the labelling on the underlying transition sequence. Formally, we have the following result.

Proposition 1. Let N = (S, T, F, M_{in}, λ) be a trace-labelled net and let ρ(w) and ρ(w′) be two runs of N such that w = t_{1}t_{2} … t_{k}, w′ = t′_{1}t′_{2} … t′_{k} and λ(t_{i}) = λ(t′_{i}) for each i ∈ {1, 2, …, k}. Then, ρ(w) ≃ ρ(w′).

We omit the proof this result, which is a reformulation of a standard result of trace theory that any linearization of a trace fixes its underlying partial order representation [4].

Observe that the nets in Figure 2 are not trace-labelled. For instance, in the net on the left, the transition sequences t_{1}t_{3}t_{5} and t_{2}t_{3}t_{4} both generate the same labelled sequence, abc, but give rise to non-isomorphic runs.

In Figure 2, one reason that we could not fold down the hereditary history preserving bisimulation relation to a relation on markings was because the independence between actions b and c is context-dependent. This problem is eliminated if we work with trace-labelled nets. Nevertheless, even for trace-labelled nets, we cannot always translate a hereditary history preserving bisimulation relation into a relation on markings. Figure 3 shows the reachable markings of a pair of trace-labelled nets that are hereditary history preserving bisimilar, where aIb. Here, if we initially execute M_{in} ⟶^{b} M_{1} and M′_{in} ⟶^{b} M′_{1}, the markings are not equivalent, but after the sequences M_{in} ⟶^{a} M_{2} ⟶^{b} M_{7} ⟶^{e} M_{1} and M′_{in} ⟶^{a} M′_{3} ⟶^{b} M′_{6} ⟶^{e} M′_{1}, the markings are in fact equivalent.

[figure: M_{in}; M_{1}; M_{2}; M_{3}; M_{4}; M_{5}; M_{6}; M_{7}; M_{8}; M_{9}; a; a; a; a; a; a; b; b; b; b; b; b; d; e; e; M′_{in}; M′_{1}; M′_{2}; M′_{3}; M′_{4}; M′_{5}; M′_{6}; M′_{7}; M′_{8}; M′_{9}; a; a; a; a; a; a; b; b; b; b; b; b; d; e; e] Fig. 3.

5 Synchronized step transition systems

Step transition systems Let (A, I) be a trace alphabet. A step transition system over (A, I) is a structure T S = (Q, δ, q_{in}) where Q is a set of states with an initial state q_{in} ∈ Q and δ : Q × 2^{A} → Q is a step transition function satisfying the following conditions:

(i) If δ(q, u) = q′, then for each distinct pair a_{i}, a_{j} ∈ u, a_{i}Ia_{j}. (ii) If δ(q, u) = q′, then for all v ⊆ u, there exists q_{v} such that δ(q, v) = q_{v} and

δ(q_{v}, u \ v) = q′.

Thus, transitions in a step transition system are labelled by sets of pairwise independent actions in such a way that every step can be broken up into all possible substeps. This definition of step transition systems is equivalent to deterministic distributed transition systems, as defined in [9].

Notice that for independent actions a and b, it is possible to have transitions δ(q, a) = q_{a}, δ(q, b) = q_{b} and δ(q_{a}, b) = δ(q_{b}, a) = q′, but not have the step transition δ(q, {a, b}) = q′. A step transition system that does not exhibit such anomalies is said to be coherent. Coherent step transition systems A step transition system T S = (Q, δ, q_{in}) over (A, I) is said to be coherent if the following holds: whenever δ(q, a) = q_{a} and δ(q_{a}, b) = q′ for aIb, it is the case that δ(q, {a, b}) = q′.

Proposition 2. Let T S = (Q, δ, q_{in}) be a coherent step transition system over (A, I) and let q ∈ Q be a state that is reachable from the initial state q_{in}. Let w ∈ A^{∗} be a word such that δ(q_{in}, w) = q. For every w′ ∼ w, δ(q_{in}, w′) = q (recall that ∼ is the trace equivalence relation induced by I).

The proof, which we omit, is by induction on the number of times we have to apply the immediate trace equivalence ∼_{0} to go from w to w′. Synchronous step transition systems Let N_{i} = (S_{i}, T_{i}, F_{i}, M_{in}^{i}, λ_{i}), i ∈ {1, 2} be a pair of labelled Petri nets. We can extend the independence relations I_{N_{1}} on T_{1} and I_{N_{2}} on T_{2} to an independence relation I_{N_{12}} on T_{1} × T_{2} as follows: (t_{1}, t_{2})I_{N_{12}}(t′_{1}, t′_{2}) if and only if t_{1}I_{N_{1}}t′_{1} and t_{2}I_{N_{2}}t′_{2}.

A joint step transition system for N_{1} and N_{2} is a step transition system T S = (Q, δ, q_{in}) over (T_{1} × T_{2}, I_{N_{12}}) where:

– Q = {(r_{1}, r_{2}) | r_{1} ∈ Runs(N_{1}), r_{2} ∈ Runs(N_{2}), r_{1} ≃ r_{2}}.

– q_{in} = (r_{∅}, r_{∅}) (recall that for any net, r_{∅} denotes the empty run).

– If δ((r_{1}, r_{2}), (u_{1}, u_{2})) = (r′_{1}, r′_{2}) then r_{1} + u_{1} = r′_{1} and r_{2} + u_{2} = r′_{2}.

A synchronous step transition system for N_{1} and N_{2} is a joint step transition system T S = (Q, δ, q_{in}) for N_{1} and N_{2} that satisfies the following conditions:

– T S is coherent.

– If (r_{1}, r_{2}) ∈ Q and there is a run r′_{1} ∈ Runs(N_{1}) and a subset u_{1} ⊆ T_{1} such that r′_{1} = r_{1} + u_{1}, then there exists r′_{2} ∈ Runs(N_{2}) and u_{2} ⊆ T_{2} such that δ((r_{1}, r_{2}), (u_{1}, u_{2})) = (r′_{1}, r′_{2}).

– If (r_{1}, r_{2}) ∈ Q and there is a run r′_{2} ∈ Runs(N_{2}) and a subset u_{2} ⊆ T_{2} such that r′_{2} = r_{2} + u_{2}, then there exists r′_{1} ∈ Runs(N_{1}) and u_{1} ⊆ T_{1} such that δ((r_{1}, r_{2}), (u_{1}, u_{2})) = (r′_{1}, r′_{2}).

Intuitively, a synchronous step transition system for N_{1} and N_{2} corresponds to a bisimulation between the unfoldings of the two nets in which each step in one net is simulated uniformly by a step from the other net.

Lemma 3. Let N_{i} = (S_{i}, T_{i}, F_{i}, M_{in}^{i}, λ_{i}), i ∈ {1, 2} be a pair of trace-labelled Petri nets. There is hereditary history preserving bisimulation between N_{1} and N_{2} if and only if there is a synchronous step transition system for N_{1} and N_{2}.

Proof. (⇒) Let H be a hereditary history preserving bisimulation between N_{1} and N_{2}. We construct a synchronous step transition system T S = (Q, δ, q_{in}) for N_{1} and N_{2} as follows:

– Q = {(ρ_{1}, ρ_{2}) | ρ ∈ H}.

– q_{in} = (r_{∅}, r_{∅}).

– δ((ρ_{1}, ρ_{2}), (u_{1}, u_{2})) = (ρ′_{1}, ρ′_{2}) if ρ, ρ′ ∈ H with ρ + ⟨u_{1}, u_{2}⟩ = ρ′.

We first verify that T S is coherent. Suppose that δ((ρ_{1}, ρ_{2}), (t′_{1}, t′_{2})) = (ρ′_{1}, ρ′_{2}) and δ((ρ′_{1}, ρ′_{2}), (t′′_{1}, t′′_{2})) = (ρ′′_{1}, ρ′′_{2}) such that t′_{1}I_{1}t′′_{1} and t′_{2}I_{2}t′′_{2}. Then, ρ′′ = ρ + ⟨{t′_{1}, t′′_{1}}, {t′_{2}, t′′_{2}}⟩ so, by the definition of δ, δ((ρ_{1}, ρ_{2}), ({t′_{1}, t′′_{1}}, {t′_{2}, t′′_{2}})) = (ρ′′_{1}, ρ′′_{2}), as required by coherence.

Next, we check forward extensibility. Suppose that (ρ_{1}, ρ_{2}) in T S and ρ_{1} + u_{1} = ρ′_{1} ∈ Runs(T S). Let u_{1} = {t_{1}, t_{2}, …, t_{k}}. Since ρ ∈ H, there must exist transitions t′_{1}, t′_{2}, …, t′_{k} ∈ T_{2} such that ρ + ⟨t_{1}, t′_{1}⟩ + ⟨t_{2}, t′_{2}⟩ + ⋯ + ⟨t_{k}, t′_{k}⟩ = ρ′′ ∈ H. Setting u_{2} = {t′_{1}, t′_{2}, …, t′_{k}}, it follows that δ((ρ_{1}, ρ_{2}), (u_{1}, u_{2})) = (ρ′′_{1}, ρ′′_{2}). Clearly, ρ′′_{1} = ρ′_{1}, so the required transition is present in δ.

(⇐) Conversely, let T S = (Q, δ, q_{in}) be a synchronous step transition for N_{1} and N_{2}. Without loss of generality, we assume that every state (r_{1}, r_{2}) ∈ Q is reachable from the initial state (r_{∅}, r_{∅})—if there is an unreachable state, we can remove it from T S without affecting either the coherence or the bisimulation characteristics of T S.

Let H = {ρ | (ρ_{1}, ρ_{2}) ∈ Q}. We claim that H is a hereditary history preserving bisimulation. It is easy to verify that H satisfies the two forward extensibility conditions for hereditary history preserving bisimulations.

What we need to establish is the backward closure condition—if ρ ∈ H and e is a maximal event in ρ, we must argue that ρ − e also belongs to H. The state (ρ_{1}, ρ_{2}) in T S corresponding to ρ is reachable from (r_{∅}, r_{∅}). Let w = (t_{1}^{1}, t_{1}^{2}), (t_{1}^{2}, t_{2}^{2}), …, (t_{1}^{k}, t_{2}^{k}) be a sequence of transitions such that δ((r_{∅}, r_{∅}), w) = (ρ_{1}, ρ_{2}). The maximal event e in ρ corresponds to some pair of transitions (t_{1}^{j}, t_{2}^{j}) in this sequence. Since T S is coherent, by Proposition 2, for every reordering w′ of w that is consistent with I_{N_{12}}, δ((r_{∅}, r_{∅}), w′) = (ρ_{1}, ρ_{2}). Since e is a maximal event in ρ, there is a reordering of w of the form w′ = u · (t_{1}^{j}, t_{2}^{j}). Let (r_{1}^{u}, r_{2}^{u}) = δ((r_{∅}, r_{∅}), u). Then, δ((r_{1}^{u}, r_{2}^{u}), (t_{1}^{j}, t_{2}^{j})) = (ρ_{1}, ρ_{2}). It follows, therefore, that the matched run ρ^{u} ∈ H such that ρ_{1}^{u} = r_{1}^{u} and ρ_{2}^{u} = r_{2}^{u} is the matched run obtained by removing e from ρ. □

6 Decidability of strong step bisimulation

Recall that our goal is to show that hereditary history preserving bisimulation is decidable for 1-safe trace-labelled nets. From the previous section, it suffices to check whether a pair of trace-labelled nets admits a synchronous step transition system. It turns out that this amounts to checking for the existence of a statebased step bisimulation between a pair of finite step transition systems. Trace-relabelling Let (A, I_{A}) and (B, I_{B}) be a pair of trace alphabets. A trace-relabelling of (A, I_{A}) by (B, I_{B}) is a function λ : A → B such that aI_{A}a′ if and only if λ(a)I_{B}λ(a′). Step bisimulations For i ∈ {1, 2}, let T S_{i} = (Q_{i}, δ_{i}, q_{in}^{i}) be a step transition system over trace alphabet (A_{i}, I_{i}), and let λ_{i} : A_{i} → B be a trace-relabelling of (A_{i}, I_{i}) by a third trace alphabet (B, I_{B}). A step bisimulation between T S_{1} and T S_{2} is a relation R ⊆ Q_{1} × Q_{2} such that:

(i) (q_{in}^{1}, q_{in}^{2}) ∈ R. (ii) (q_{1}, q_{2}) ∈ R and δ_{1}(q_{1}, u_{1}) = q′_{1} implies there exists u_{2} such that λ_{1}(u_{1}) =

λ_{2}(u_{2}) and (q′_{1}, δ_{2}(q_{2}, u_{2})) ∈ R. (iii) (q_{1}, q_{2}) ∈ R and δ_{2}(q_{2}, u_{2}) = q′_{2} implies there exists u_{1} such that λ_{1}(u_{1}) =

λ_{2}(u_{2}) and (δ_{1}(q_{1}, u_{1}), q′_{2}) ∈ R. (iv) Let (q_{1}, q_{2}) ∈ R and (δ_{1}(q_{1}, u_{1}), δ_{2}(q_{2}, u_{2})) ∈ R for u_{1}, u_{2} such that λ_{1}(u_{1}) =

λ_{2}(u_{2}) = u. For each v ⊆ u, (δ(q_{1}, λ_{1}^{−1}(v)), δ(q_{2}, λ_{2}^{−1}(v))) ∈ R.

Thus, a step bisimulation is just a bisimulation with respect to an additional level of labelling that respects substeps. Conditions (ii) and (iii) are the normal forward extensibility criteria for bisimulation, extended to steps. The fourth condition ensures that R is closed under substeps. Run foldings Let (Σ, I) be a trace alphabet and let N = (S, T, F, M_{in}, λ) be a trace-labelled net over Σ. For each run r ∈ Runs(N), recall that M_{r} denotes the marking associated with r. Let top_{r} ⊆ Σ denote the labels associated with the maximal transitions in r. Clearly, top_{r} is a subset of Σ in which all actions are pairwise independent. The run folding of N is the step transition system T S = (Q, δ, q_{in}) over (T, I_{N}) where:

– Q = {(M_{r}, top_{r}) | r ∈ Runs(N)}.

– q_{in} = (M_{in}, ∅).

– For all u ⊆ T such that M_{r} ⟶^{u}, δ((M_{r}, top_{r}), u) = (M_{r+u}, top_{r+u}).

Observe that the run folding of N is a finite step transition system. The transition function δ is well-defined because N is trace-labelled—it is not difficult to see that for any pair of runs r, r′ such that M_{r} = M_{r′}, top_{r} = top_{r′} and

M_{r} ⟶^{u}, top_{r+u} = top_{r′+u}.

Lemma 4. Let (Σ, I) be a trace alphabet and N_{i} = (S_{i}, T_{i}, F_{i}, M_{in}^{i}, λ_{i}), i = {1, 2} be a pair of trace-labelled nets over Σ. Then, N_{1} and N_{2} admit a synchronized step transition system if and only if there exists a step bisimulation between the run foldings of N_{1} and N_{2} with trace-relabellings λ_{1} and λ_{2} from T_{1} and T_{2} into Σ, respectively.

Proof. (⇒) Let T S = (Q, δ, q_{in}) be a synchronized step transition system for N_{1} and N_{2} and let T S_{1} = (Q_{1}, δ_{1}, q_{in}^{1}) and T S_{2} = (Q_{2}, δ_{2}, q_{in}^{2}) be the run foldings of N_{1} and N_{2}, respectively. Recall that each state in T S is of the form (r_{1}, r_{2}), where r_{1} ∈ Runs(N_{1}) and r_{2} ∈ Runs(N_{2}) and each state in T S_{i}, i ∈ {1, 2}, is of the form (M_{r}, top_{r}) for some run r ∈ Runs(N_{i}).

We define a relation R ⊆ Q_{1} × Q_{2} as follows:

R = {((M_{1}, A_{1}), (M_{2}, A_{2})) | (r_{1}, r_{2}) ∈ Q, M_{i} = M_{r_{i}}, A_{i} = top_{r_{i}}, i ∈ {1, 2}} The fact that R is a step bisimulation between T S_{1} and T S_{2} follows immedi-

ately from the definition of a synchronized step transition system for N_{1} and N_{2}. The forward extensibility conditions for R follow from the extensibility criteria for T S. The substep closure of R follows from the coherence of T S.

(⇐) Conversely, suppose that R is a step bisimulation between T S_{1} and T S_{2}. We have to construct a synchronized step transition system T S for N_{1} and N_{2}.

We construct T S inductively, maintaining the invariant that for every state (r_{1}, r_{2}) that we add to T S, the corresponding pair of states ((M_{r_{1}}, top_{r_{1}}), (M_{r_{2}}, top_{r_{2}})) belongs to R.

We begin with the initial state (r_{∅}, r_{∅}) that corresponds to the pair ((M_{in}^{1}, ∅), (M_{in}^{2}, ∅)) which is guaranteed to belong to R.

Let (r_{1}, r_{2}) be a state in T S. We know that ((M_{r_{1}}, top_{r_{1}}), (M_{r_{2}}, top_{r_{2}})) ∈ R. For each pair (u_{1}, u_{2}) such that (δ_{1}((M_{r_{1}}, top_{r_{1}}), u_{1}), δ_{2}((M_{r_{2}}, top_{r_{2}}), u_{2})) ∈ R, add the state (r_{1} + u_{1}, r_{2} + u_{2}) to T S.

It is easy to see that T S is a joint step transition system for N_{1} and N_{2}. To check that it is, in fact, a synchronized step transition system for N_{1} and N_{2}, we must establish coherence and the forward extensibility properties.

We first check coherence. Suppose that δ((r_{1}, r_{2}), (t_{1}, t_{2})) = (r′_{1}, r′_{2}) and δ((r′_{1}, r′_{2}), (t′_{1}, t′_{2})) = (r′′_{1}, r′′_{2}) where (t_{1}, t_{2})I_{N_{12}}(t′_{1}, t′_{2}). We need to show that δ((r_{1}, r_{2}), {(t_{1}, t_{2}), (t′_{1}, t′_{2})}) = (r′′_{1}, r′′_{2}) as well. From the construction of T S, we know that both ((M_{r_{1}}, top_{r_{1}}), (M_{r_{2}}, top_{r_{2}})) and ((M_{r′′_{1}}, top_{r′′_{1}}), (M_{r′′_{2}}, top_{r′′_{2}})) belong to R. From the definition of run foldings, we have δ_{i}((M_{r_{i}}, top_{r_{i}}), {t_{i}, t′_{i}}) = (M_{r′′_{i}}, top_{r′′_{i}}) for i ∈ {1, 2}. Hence, δ((r_{1}, r_{2}), {(t_{1}, t_{2}), (t′_{1}, t′_{2})}) = (r′′_{1}, r′′_{2}).

The forward extensibility properties for T S follow naturally from the properties of step bisimulations, so we omit the details. □

Theorem 5. Hereditary history preserving bisimulation is decidable for tracelabelled systems.

Proof. From Lemmas 3 and 4, it follows that a pair of nets N_{1} and N_{2} admit a hereditary history preserving bisimulation if and only if there is a step bisimulation between their run foldings. It is clear that the existence of a step bisimulation between two finite step transition systems can be checked (exhaustively, if nothing else). Since the run foldings of N_{1} and N_{2} are guaranteed to be finite step transition systems, the result follows. □

7 Discussion

As we mentioned at the outset, while branching time semantics is relatively well understood in the interleaved approach to the semantics of concurrent systems, the situation is not so clear when labelled partial orders are used to record the behaviour of such systems. In many contexts, the application of Mazurkiewicz trace theory provides a context in which apparently intractable problems become solvable. Our result here is one example of this phenomenon. This seems to suggest that it might make sense to restrict our attention to trace-labelled systems, at least initially, when attempting to build up our understanding of the interplay between nondeterminism and concurrency.

References

1. M.A. Bednarczyk: Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdansk (1991).

2. M.A. Bednarczyk: Categories of asynchronous systems, PhD Thesis, Report 1/88, Computer Science, University of Sussex (1988).

3. P. Degano, R. de Nicola and U. Montanari: Partial ordering descriptions and observations of nondeterministic concurrent processes, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Springer LNCS 354 (1989) 438–466.

4. V. Diekert and G. Rozenberg (eds), The Book of Traces, World Scientific, Singapore (1995).

5. S.B. Fröschle and T.T. Hildebrandt: On plain and hereditary history-preserving bisimulation, Proc MFCS ’99, Springer LNCS 1672 (1999) 354–365.

6. L. Jategaonkar and A. Meyer: Deciding true concurrency equivalence on safe, finite nets, Theoretical Computer Science, 154(1) (1996) 107–143.

7. A. Joyal, M. Nielsen and G. Winskel: Bisimulation from open maps, Information and Computation, 127(2) (1996) 164–185.

8. M. Jurdzinski and M. Nielsen: Hereditary history preserving bisimilarity is undecidable, in Proc. STACS 2000 Springer LNCS 1770 (2000) 358–369.

9. K. Lodaya, R. Parikh, R. Ramanujam and P.S. Thiagarajan: A Logical Study of Distributed Transition Systems, Information and Computation 119(1) (1995) 91–118.

10. A. Mazurkiewicz: Basic notions of trace theory, in: J.W. de Bakker, W.- P. de Roever, G. Rozenberg (eds.), Linear time, branching time and partial order in logics and models for concurrency, LNCS, 354 (1989) 285–363.

11. R. Milner: Communication and Concurrency, Prentice-Hall, London (1989).

12. M. Nielsen and C. Clausen: Games and Logics for a Noninterleaving Bisimulation, Nordic Journal of Computing 2(2) (1995) 221–249.

13. D. Park: Concurrency and automata on infinite sequences, in Proc. Theoretical Computer Science: 5th GI Conference, Springer LNCS 104 (1981).

14. W. Reisig and G. Rozenberg (eds.): Lectures on Petri Nets, Vols I and II Springer LNCS 1492,1493 (1998).

15. A. Rabinovitch and B.A. Trakhtenbrot: Behavior strucures and nets, Fundamenta Informaticae, 11(4) (1988) 357–403.

16. R. van Glabbeek and U. Goltz: Refinement of actions and equivalence notions for concurrent systems, Proc MFCS ’89, Springer LNCS 379 (1989) 237–248.

17. G. Winskel and M. Nielsen: Models for concurrency, in S. Abramsky, D. Gabbay and T.S.E. Maibaum, eds, Handbook of Logic in Computer Science, Vol 4, Oxford (1995) 1–148.

18. W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O.—Inform. Théor. Appl., 21 (1987) 99–135.