Weak Bisimulation Approximants

Will Harwood, Faron Moller, and Anton Setzer^{⋆}

Department of Computer Science, Swansea University Singleton Park, Sketty, Swansea SA2 8PP, UK

               {cswill,f.g.moller,a.g.setzer}@swansea.ac.uk

Abstract. Bisimilarity ∼ and weak bisimilarity ≈ are canonical notions of equivalence between processes, which are defined co-inductively, but may be approached – and even reached – by their (transfinite) inductively-defined approximants ∼_{α} and ≈_{α}. For arbitrary processes this approximation may need to climb arbitrarily high through the infinite ordinals before stabilising. In this paper we consider a simple yet well-studied process algebra, the Basic Parallel Processes (BPP), and investigate for this class of processes the minimal ordinal α such that ≈ = ≈_{α}.

The main tool in our investigation is a novel proof of Dickson’s Lemma. Unlike classical proofs, the proof we provide gives rise to a tight ordinal bound, of ω^{n}, on the order type of non-increasing sequences of n-tuples of natural numbers. With this we are able to reduce a long-standing bound on the approximation hierarchy for weak bisimilarity ≈ over BPP, and show that ≈ = ≈_{ω^{ω}}.

1 Introduction

There has been great interest of late in the development of techniques for deciding equivalences between infinite-state processes, particularly for the question of bisimilarity between processes generated by some type of term algebra. Several surveys of this developing area have been published, beginning with [16], and there is now a chapter in the Handbook of Process Algebra dedicated to the topic [2], as well as a website devoted to maintaining an up-to-date comprehensive overview of the state-of-the-art [20].

While questions concerning strong bisimilarity have been successfully addressed, techniques for tackling the question of weak bisimilarity, that is, when silent unobservable transitions are allowed, are still lacking, and many open problems remain. The main difficulty arising when considering weak bisimilarity is that processes immediately become infinite-branching: at any point in a computation, a single action can result in any number of transitions leading to any one of an infinite number of next states. Common finiteness properties fail due to this; in particular, bisimilarity can no longer be characterised by its finite approximations in the way that it can for finite-branching processes. For arbitrary infinite-branching processes, we may need to climb arbitrarily high through

⋆ Supported by EPSRC grant GR/S30450/01.

the transfinite approximations to bisimilarity before reaching the bisimulation relation itself.

In this paper we consider the problem of weak bisimilarity for so-called Basic Parallel Processes (BPP), a simple yet well-studied model of concurrent processes. These correspond to commutative context-free processes, or equivalently to communication-free Petri nets. The question as to the decidability of weak bisimilarity between BPP processes remains unsolved (though decidability results for very restricted classes of BPP have been established by Hirshfeld in [10] and Stirling in [21]). It has recently been shown that the problem is at least PSPACE-hard [19], even in the restricted case of so-called normed BPP, but this sheds no light one way or the other as to decidability. Jančar suggests in [14] that the techniques he uses there to establish PSPACE-completeness of strong bisimilarity for BPP might be exploited to give a decision procedure for weak bisimilarity, but three years later this conjecture remains unsubstantiated.

It has long been conjectured that for BPP, weak bisimilarity is characterised by its (ω×2)-level approximation. Such a result could provide a way to a decision procedure. However, no nontrivial approximation bound has before now been established; the strength of the (ω×2)-conjecture remains rooted only in the fact that no counterexample has been found. In this paper we provide the first non-trivial countable bound on the approximation: for a BPP defined over k variables, weak bisimilarity is reached by the ω^{2k} level; weak bisimilarity is thus reached by the ω^{ω} level for any BPP.

Our argument is based on a new constructive proof of Dickson’s Lemma which provides an ordinal bound on the sequences described by the Lemma. This proof is presented in Section 2 of the paper. After this, the definitions necessary for the remainder of the paper are outlined in Section 3 along with a variety of results, and our results on BPP are presented in Section 4. We finish with some concluding observations in Section 5.

2 Ordinal Bounds for Dickson’s Lemma

In the sequel we shall use the following notation. We let x, y (with subscripts) range over natural numbers ℕ = {0, 1, 2, …}; x⃗, y⃗ (with subscripts) range over finite sequences (n-tuples) of natural numbers; and X⃗, Y⃗ range over arbitrary (finite or infinite) sequences of such n-tuples. We shall use angle brackets to denote sequences, such as x⃗ = ⟨x_{1}, …, x_{n}⟩ and X⃗ = ⟨x⃗_{1}, x⃗_{2}, …⟩, and juxtaposition to represent concatenation; e.g., if X⃗ is a finite sequence of n-tuples then X⃗⟨x⃗⟩ is the longer sequence which has the extra n-tuple x⃗ added to the end. Finally, we shall use the notation (·)_{k} to select the kth component from a sequence; for example, if x⃗_{i} = ⟨x_{1}, …, x_{n}⟩ then (x⃗_{i})_{k} = x_{k}. (The parentheses are used to avoid confusion with the subscripting allowed in the variable naming the sequence.)

One n-tuple y⃗ = ⟨y_{1}, …, y_{n}⟩ of natural numbers dominates another such n-tuple x⃗ = ⟨x_{1}, …, x_{n}⟩ if x⃗ ≤ y⃗, where ≤ is considered pointwise, that is, x_{i} ≤ y_{i} for each i ∈ {1, …, n}. A sequence of n-tuples is a non-dominating sequence over ℕ^{n} if no element of the sequence dominates any of its predecessors in the sequence. A tree – by which we mean a rooted directed graph with no undirected cycles – with nodes labelled by n-tuples from ℕ^{n} is a non-dominating tree over ℕ^{n} if the sequence of labels along any path through the tree is a non-dominating sequence.

Dickson’s Lemma [6] asserts that there can be no infinite non-dominating sequences.

Lemma 1 (Dickson’s Lemma). All non-dominating sequences are finite. That is, given an infinite sequence of vectors x⃗_{1}, x⃗_{2}, x⃗_{3}, … ∈ ℕ^{n}, we can always find indices i, j with i < j such that x⃗_{i} ≤ x⃗_{j}.

The standard proof of this lemma uses a straightforward induction on n: for the base case, any sequence of decreasing natural numbers must be finite; and for the induction step, from an infinite sequence of n-tuples you extract an infinite subsequence in which the last components are nondecreasing (either constant or increasing), and then apply induction on the sequence of (n−1)-tuples which arise by ignoring these last components.

The problem with this proof is that it is nonconstructive; in particular, it gives no clue as to the ordinal bound on the lengths of non-dominating sequences. The difficulty with determining an ordinal bound comes from the fact that the domination order is not a total order on n-tuples (as opposed, for example, to lexicographical order). We provide here an alternative constructive proof from which we can extract an ordinal bound on the lengths of such sequences.

Theorem 1 (Constructive Dickson’s Lemma). The order type of the set of non-dominating sequences of n-tuples of natural numbers with partial ordering

X⃗ ≺ Y⃗ ⇔^{def} X⃗ strictly extends Y⃗

is ω^{n}.

Proof. That the order type is at least ω^{n} is clear: the order type of the set of lexicographically descending sequences with respect to extension is ω^{n}, and this set is contained in the set of non-dominating sequences.

It remains to show that the order type is at most ω^{n}. This result will follow immediately from the construction of a function

f_{n} : (ℕ^{n})^{+} → ℕ^{n}

on non-empty finite sequences of n-tuples which satisfies the following property:

If X⃗⟨x⃗⟩ is a non-dominating sequence of n-tuples, and X⃗ is itself non-empty, then f_{n}(X⃗⟨x⃗⟩) <_{lex} f_{n}(X⃗).

We shall inductively define these functions f_{n}. The base case is straightforward: we can define f_{1} by

f_{1}(⟨x_{1}, …, x_{k}⟩) =^{def} x_{k}.

A non-dominating sequence of natural numbers is simply a decreasing sequence, which has ordinal bound ω.

For illustrative purposes we carry out the construction of the function f_{2} for sequences of pairs, and later generalise our construction to sequences of n-tuples.

Given a non-empty finite sequence of pairs X⃗ = ⟨⟨x_{1}, y_{1}⟩, …, ⟨x_{k}, y_{k}⟩⟩, define

• min_{x}(X⃗) =^{def} min{ x_{i} : 1 ≤ i ≤ k },

• min_{y}(X⃗) =^{def} min{ y_{i} : 1 ≤ i ≤ k }, and

• S_{2}(X⃗) =^{def} { ⟨x, y⟩ : min_{x}(X⃗) ≤ x, min_{y}(X⃗) ≤ y, and ⟨x_{i}, y_{i}⟩ ≰ ⟨x, y⟩ for all i : 1 ≤ i ≤ k }.

S_{2}(X⃗) consists of the pairs with which the sequence X⃗ can be extended without altering the min_{x} and min_{y} values and yet while maintaining non-domination. Note that S_{2}(X⃗) must be finite: if we let i and j be such that x_{i} = min_{x}(X⃗) and y_{j} = min_{y}(X⃗), then in order for ⟨x, y⟩ ≱ ⟨x_{i}, y_{i}⟩ and ⟨x, y⟩ ≱ ⟨x_{j}, y_{j}⟩ we must have x < x_{j} (since y ≥ y_{j}) and y < y_{i} (since x ≥ x_{i}).

Suppose that Y⃗ = X⃗⟨⟨x, y⟩⟩ is a non-dominating sequence, and that X⃗ is itself non-empty. Then clearly min_{x}(Y⃗ ) ≤ min_{x}(X⃗) and min_{y}(Y⃗ ) ≤ min_{y}(X⃗); and if equality holds in both cases then S_{2}(Y⃗ ) ⊊ S_{2}(X⃗), since S_{2}(Y⃗ ) ⊆ S_{2}(X⃗) yet ⟨x, y⟩ ∈ S_{2}(X⃗) \ S_{2}(Y⃗ ). Thus |S_{2}(Y⃗ )| < |S_{2}(X⃗)|.

We can then define the function f_{2} on non-empty sequences X⃗ of pairs as follows:

f_{2}(X⃗) =^{def} ⟨ min_{x}(X⃗)+min_{y}(X⃗), |S_{2}(X⃗)| ⟩

If X⃗⟨⟨x, y⟩⟩ is a non-dominating sequence and X⃗ is itself non-empty, then by the above argument we must have that f_{2}(X⃗⟨⟨x, y⟩⟩) <_{lex} f_{2}(X⃗).

For the inductive construction of f_{n} we assume we have constructed the function f_{n−1} as required. For 1 ≤ i ≤ n we define the function

π_{-i}(⟨x_{1}, …, x_{n}⟩) =^{def} ⟨x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}⟩

which simply deletes the ith component from the n-tuple ⟨x_{1}, …, x_{n}⟩. Next, given a non-empty finite sequence X⃗ = ⟨x⃗_{1}, …, x⃗_{k}⟩ of n-tuples, we define the set

nd_{-i}(X⃗) =^{def} \{ \begin{matrix}⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}})⟩ : p > 0, 0 < i_{1} < ⋯ < i_{p} ≤ k, \\ and ⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}})⟩ is non-dominating \} \end{matrix}

which consists of the non-dominating subsequences of (n−1)-tuples of X⃗ in which the ith components of the n-tuples have been deleted. Finally we make the following definitions:

• min_{-i}(X⃗) =^{def} min_{<_{lex}}{ f_{n−1}(Y⃗ ) : Y⃗ ∈ nd_{-i}(X⃗) }

• S_{n}(X⃗) =^{def} { x⃗ : min_{-i}(X⃗) = min_{-i}(X⃗⟨x⃗⟩) for all i : 1 ≤ i ≤ n, and x⃗_{i} ≰ x⃗ for all i : 1 ≤ i ≤ k }

S_{n}(X⃗) consists of the n-tuples with which the sequence X⃗ can be extended without altering the min_{-i} values and yet while maintaining non-domination. Note that S_{n}(X⃗) must be finite. To see this, let 1 ≤ i ≤ n and i_{1}, …, i_{p} be such that

min_{-i}(X⃗) = f_{n−1}(⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}})⟩),

and suppose that x⃗ ∈ S_{n}(X⃗). If the sequence ⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}}), π_{-i}(x⃗)⟩ is non-dominating, then by induction we would get that

min_{-i}(X⃗⟨x⃗⟩) \begin{matrix}≤_{lex} & f_{n−1}(⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}}), π_{-i}(x⃗)⟩) \\ <_{lex} & f_{n−1}(⟨π_{-i}(x⃗_{i_{1}}), …, π_{-i}(x⃗_{i_{p}})⟩) \\ = & min_{-i}(X⃗) \end{matrix}

contradicting x⃗ ∈ S_{n}(X⃗). Therefore we must have that π_{-i}(x⃗) ≥ π_{-i}(x⃗_{i_{j}}) for some j. But since x⃗ ≱ x⃗_{i_{j}} we must then have that (x⃗)_{i} < (x⃗_{i_{j}})_{i}.

Suppose that Y⃗ = X⃗⟨x⃗⟩ is a non-dominating sequence, and that X⃗ is itself non-empty. Then min_{-i}(Y⃗ ) ≤ min_{-i}(X⃗) for all i (since nd_{-i}(X⃗) ⊆ nd_{-i}(Y⃗ )); and if equality holds in all cases then S_{n}(Y⃗ ) ⊊ S_{n}(X⃗) since S_{n}(Y⃗ ) ⊆ S_{n}(X⃗) yet x⃗ ∈ S_{n}(X⃗) \ S_{n}(Y⃗ ). Thus |S_{n}(Y⃗ )| < |S_{n}(X⃗)|.

We can then define the function f_{n} on non-empty sequences X⃗ of n-tuples as follows:

f_{n}(X⃗) = ( ∑_{i=1}^{n} min_{-i}(X⃗))⟨|S_{n}(X⃗)|⟩

where the sum is taken component-wise. (This sum is, if we identify ⟨k_{1}, …, k_{n}⟩ with ω^{n−1} ·k_{1} +ω^{n−2} ·k_{2} +⋯+ω^{0} ·k_{n}, the natural sum of ordinals.) If X⃗⟨x⃗⟩ is a non-dominating sequence and X⃗ is itself non-empty, then by the above argument we must have that f_{n}(X⃗⟨x⃗⟩) <_{lex} f_{n}(X⃗). □

2.1 Ordinal Bounds on Trees

Our constructive version of Dickson’s Lemma easily extends to trees, where we take the following definition of the height of a well-founded tree (that is, a tree with no infinite paths).

Definition 1. The height of a well-founded tree rooted at t is defined by

h(t) =^{def} sup{ h(s) + 1 : t ⟶ s }.

(By convention, sup ∅ = 0.)

Theorem 2. If t is (the root of) a non-dominating tree over ℕ^{n}, then h(t) ≤ ω^{n}.

Proof. For each node x of the tree, define ℓ(x) ∈ ℕ^{n} by ℓ(x) = f_{n}(π_{x}), where f_{n} is as defined in the proof of Lemma 1, and π_{x} is the non-dominating sequence of labels on the path from (the root) t to x. It will suffice then to prove that h(x)≤ℓ(x) (viewing ℓ(x) as an ordinal, that is, interpreting the n-tuple ⟨k_{1}, …, k_{n}⟩ ∈ ℕ^{n} as ω^{n−1}k_{1} + ω^{n−2}k_{2} + ⋯ + ω^{0}k_{n}) for all nodes x of the tree. This is accomplished by a straightforward induction on h(x):

h(x) = sup{ h(y)+1 : x → y } ≤ sup{ ℓ(y)+1 : x → y } (by induction) ≤ ℓ(x). □

3 Processes and Bisimilarity

A process is represented by (a state in) a labelled transition system defined as follows.

Definition 2. A labelled transition system (LTS) is a triple S = (S, Act, →) where S is a set of states, Act is a finite set of actions, and → ⊆ S × Act × S is a transition relation.

We write s →^{a} t instead of (s, a, t) ∈ →, thus defining an infix binary relation →^{a} = {(s, t) : (s, a, t) ∈ →} for each action a ∈ Act.

It is common to admit silent transitions to model the internal unobservable evolution of a system. In standard automata theory these are typically referred to as “epsilon” (or occasionally “lambda”) transitions, but in concurrency theory they are commonly represented by a special action τ ∈ Act. With this, we can then define observable transitions as follows:

s ⇒^{τ} t iff s (→^{τ})^{∗} t and

s ⇒^{a} t iff s (→^{τ})^{∗} · →^{a} · (→^{τ})^{∗} t for a ≠ τ.

In general, ⇒^{a} ⊇ →^{a}; and over an LTS with no silent transitions, ⇒^{a} = →^{a}, and in this case all the relations we define wrt ⇒ will be identical to the analogous relations defined wrt →.

The notion of “behavioural sameness” between two processes (which we view as two states in the same LTS) can be formally captured in many different ways (see, e.g., [8] for an overview). Among those behavioural equivalences, bisimilarity enjoys special attention. Its formal definition is as follows.

Definition 3. Let S = (S, Act, →) be an LTS. A binary relation R ⊆ S × S is a bisimulation relation iff whenever (s, t) ∈ R, we have that

– for each transition s →^{a} s′ there is a transition t →^{a} t′ such that (s′, t′) ∈ R; and – for each transition t →^{a} t′ there is a transition s →^{a} s′ such that (s′, t′) ∈ R.

Processes s and t are bisimulation equivalent (bisimilar), written s ∼ t, iff they are related by some bisimulation. Thus ∼ is the union, and ergo the largest, of all bisimulation relations.

If we replace the transition relation → in this definition with the weak transition relation ⇒, we arrive at the definition of a weak bisimulation relation defining weak bisimulation equivalence (weak bisimilarity), which we denote by ≈. In general, ≈ ⊇ ∼; and over an LTS with no silent transitions, ≈ = ∼.

The above definition of (weak) bisimilarity is a co-inductive one, but can be approximated using the following inductively-defined stratification.

Definition 4. The bisimulation approximants ∼_{α}, for all ordinals α ∈ O, are defined as follows:

– s ∼_{0} t for all process states s and t.

– s ∼_{α+1} t iff

• for each transition s →^{a} s′ there is a transition t →^{a} t′ such that s′ ∼_{α} t′; and

• for each transition t →^{a} t′ there is a transition s →^{a} s′ such that s′ ∼_{α} t′.

– For all limit ordinals λ, s ∼_{λ} t iff s ∼_{α} t for all α < λ.

The weak bisimulation approximants ≈_{α} are defined by replacing the transition relation → with the weak transition relation ⇒ in the above definition.

The following results are then standard.

Theorem 3.

1. Each ∼_{α} and ≈_{α} is an equivalence relation over the states of any LTS.

2. Given α < β, ∼_{α} ⊇ ∼_{β} and ≈_{α} ⊇ ≈_{β} over the states of any LTS; and in general these define strictly decreasing hierarchies: given any ordinal α we can provide an LTS with states s and t satisfying s ∼_{α} t but s ≁_{α+1} t (and s ≈_{α} t but s ≉_{α+1} t).

3. s ∼ t iff s ∼_{α} t for all ordinals α ∈ O, and s ≈ t iff s ≈_{α} t for all ordinals α ∈ O. That is, ∼ = ∩_{α∈O} ∼_{α} and ≈ = ∩_{α∈O} ≈_{α}.

Remark 1. For Part 2 of Theorem 3 we can define an LTS over a singleton alphabet {a} (a≠τ) whose state set is γ for some ordinal γ (that is, each ordinal smaller than γ is a state), and such that α →^{a} β iff β < α. Then it is easy to show that for α < β, α ∼_{α} β but α ≁_{α+1} β. (First we show, by induction on α, that if α ≤ μ, ν then μ ∼_{α} ν; then we show, by induction on α, that if α < β then α ≁_{α+1} β.) As this LTS does not have τ actions, and hence ≈=∼, this also gives that α ≈_{α} β but α ≉_{α+1} β.

If s ≁ t, we must have a least ordinal α ∈ O such that s ≁_{α+1} t, and for this ordinal α we must have s ∼_{α} t. (If s ≁_{λ} t for a limit ordinal λ then we must have s ≁_{α} t, and hence s ≁_{α+1} t, for some α < λ.) We shall identify this value α by writing s ∼_{α}^{!} t. In the same way we write s ≈_{α}^{!} t to identify the least ordinal α ∈ O such that s ≉_{α+1} t.

3.1 Bisimulation Games and Optimal Move Trees

There is a further approach to defining (weak) bisimilarity, one based on games and strategies, whose usefulness is outlined in the tutorial [15]. We describe it here for bisimilarity; its description for weak bisimilarity requires only replacing the transition relation → with the weak transition relation ⇒, after which all results stated will hold for the weak bisimilarity relations.

A game G(s, t) corresponding to two states s and t of an LTS is played between two players, A and B; the first player A (the adversary) wants to show that the states s and t are different, while the second player B (the bisimulator) wants to show that they are the same. To this end the game is played by the two players exchanging moves as follows:

– A chooses any transition s →^{a} s′ or t →^{a} t′ from one of the states s and t;

– B responds by choosing a matching transition t →^{a} t′ or s →^{a} s′ from the other state;

– the game then continues from the new position G(s′, t′).

The second player B wins this game if B can match every move that the first player A makes (that is, if A ever cannot make a move or the game continues indefinitely); if, however, B at some point cannot match a move made by A then player A wins. The following is then a straightforward result.

Theorem 4. s ∼ t iff the second player B has a winning strategy for G(s, t).

If s ≁ t, then s ∼_{α}^{!} t for some α ∈ O, and this α in a sense determines how long the game must last, assuming both players are playing optimally, before B loses the game G(s, t):

– Since s ≁_{α+1} t, A can make a move such that, regardless of B’s response, the exchange of moves will result in a game G(s′, t′) in which s′ ≁_{α} t′; such a move is an optimal move for A.

– For every β < α, regardless of the move made by A, B can respond in such a way that the exchange of moves will result in a game G(s′, t′) in which s′ ∼_{β} t′.

With this in mind, we can make the following definition.

Definition 5. An optimal move tree is a tree whose nodes are labelled by pairs of non-bisimilar states of an LTS in which an edge (s, t) ⟶ (s′, t′) exists precisely when (s, t) is a node of the tree and the following holds:

In the game G(s, t), a single exchange of moves in which A makes an optimal move may result in the game G(s′, t′)

The optimal move tree rooted at (s, t) is denoted by omt (s, t).

If (s, t) ⟶ (s′, t′) is an edge in an optimal move tree, then s ∼_{α}^{!} t and s′ ∼_{β}^{!} t′ for some α and β with α > β. Hence, every optimal move tree is well-founded. Furthermore, the following result is easily realised.

Lemma 2. h(omt(s, t)) = α iff s ∼_{α}^{!} t.

3.2 Bounded Branching Processes

Over the class of finite-branching labelled transition systems, it is a standard result that ∼ = ∼_{ω}. We give here a generalisation of this result for infinitebranching processes.

Definition 6. An infinite cardinal κ is regular iff it is not the supremum of fewer than κ smaller ordinals.

Thus for example ω is regular as it is not the supremum of any finite collection of natural numbers.

Definition 7. A process is <-κ-branching iff all of its states have fewer than κ transitions leading out of them. A tree t is <-κ-branching iff all of its nodes have fewer than κ children.

Theorem 5. If κ is a regular cardinal, and t is a well-founded <-κ-branching tree, then h(t) < κ.

Proof. By (transfinite) induction on h(t). If t ⟶ s then h(s) < h(t); and by induction h(s) < κ and hence h(s)+1 < κ. Since h(t) = sup{ h(s)+1 : t ⟶ s }, by the regularity of κ we must have that h(t) < κ. □

The most basic form of this result is König’s Lemma: any finite-branching well-founded tree can only have finitely-many nodes (and hence finite height).

The next result follows directly from the fact that |A×A| = |A| for any infinite set A.

Lemma 3. If s and t are non-equivalent states of a <-κ-branching process, then omt(s, t) is <-κ-branching.

¿From the above, we arrive at a theorem on approximant collapse, which generalises the standard result that ∼ = ∼_{ω} on finite-branching processes as well as a result in [22] concerning countably-branching processes.

Theorem 6. For regular cardinals κ, ∼ = ∼_{κ} over the class of <-κ-branching processes.

Proof. ∼ ⊆ ∼_{κ} is a given. If on the other hand s ≁ t, then h(omt(s, t)) = α where s ∼_{α}^{!} t. Thus, by Lemma 3 and Theorem 5, α < κ, and hence s ≁_{κ} t. □

4 Basic Parallel Processes

A Basic Process Algebra (BPA) process is defined by a context-free grammar in Greibach normal form. Formally this is given by a triple G = (V, A, Γ), where V is a finite set of variables (nonterminal symbols), A is a finite set of labels (terminal symbols), and Γ ⊆ V × A × V^{∗} is a finite set of rewrite rules (productions); it is assumed that every variable has at least one associated rewrite rule. Such a grammar gives rise to the LTS S_{G} = (V^{∗}, A, →) in which the states are sequences of variables, the actions are the labels, and the transition relation is given by the rewrite rules extended by the prefix rewriting rule: if (X, a, u) ∈ Γ then Xv →^{a} uv for all v ∈ V^{∗}. In this way, concatenation of variables naturally represents sequential composition.

A Basic Parallel Processes (BPP) process is defined in exactly the same fashion from such a grammar. However, in this case elements of V^{∗} are read modulo commutativity of concatenation, so that concatenation is interpreted as parallel composition rather than sequential composition. The states of the BPP process associated with a grammar are thus given not by sequences of variables but rather by multisets of variables.

As an example, Figure 1 depicts BPA and BPP processes defined by the same

\xymatrix{A \ar[r]^{a} \ar[d]^{c} & AB \ar[r]^{a} \ar[d]^{c} & ABB \ar[r]^{a} \ar[d]^{c} & … & A \ar[r]^{a} \ar[d]^{c} & AB \ar[l]^{b} \ar[r]^{a} \ar[d]^{c} & ABB \ar[l]^{b} \ar[r]^{a} \ar[d]^{c} & … \ar[l]^{b} \\ ε & B \ar[l]^{b} & BB \ar[l]^{b} & … \ar[l]^{b} & ε & B \ar[l]^{b} & BB \ar[l]^{b} & … \ar[l]^{b}}

Fig. 1. BPA and BPP processes defined by the grammar A →^{a} AB, A →^{c} ε, B →^{b} ε

grammar given by the three rules A →^{a} AB, A →^{c} ε and B →^{b} ε.

Decidability results for (strong) bisimilarity checking have been long established for both BPA [5] and BPP [3, 4]. For a wide class of interest (normed processes) these problems have even been shown to have polynomial-time solutions [11–13]. More recently, the decision problems for full BPA and BPP have been shown to be PSPACE-hard [17, 18].

Decidability results for weak bisimilarity are much harder to establish, mainly due to the problems of infinite branching. While over BPA and BPP we have ∼ = ∩_{n∈ω} ∼_{n}, the infinite-branching nature of the weak transition relations makes this result false. As an example, Figure 2 gives a BPP process with states P and Q in which P ≈_{n} Q for all n ∈ ω yet P ≉ Q. In this case we have P ≈_{ω}^{!} Q, but from these we can produce BPP process states X_{n} and Y_{n} such that X_{n} ≈_{ω+n}^{!} Y_{n} by adding the following production rules to the defining grammar:

X_{1} →^{a} P  X_{i+1} →^{a} X_{i}  Y_{1} →^{a} Q  Y_{i+1} →^{a} Y_{i}

\begin{aligned}A →^{a} A & P →^{τ} A & Q →^{a} ε \\ & P →^{τ} Q & Q →^{τ} QQ \end{aligned}  [figure: P; τ; τ; A; a; ε; Q; a; τ; QQ; τ; a; QQQ; τ; a; …; a]

Fig. 2. A BPP process with states P and Q satisfying P ≈_{ω}^{!} Q

However, no example BPP states X and Y are known which satisfy X ≈_{ω×2}^{!} Y. This leads to the following long-standing conjecture.

Conjecture (Hirshfeld, Jančar). Over BPP processes, ≈ = ≈_{ω×2}.

Remark 2. The situation is different for BPA, as noted originally in [22]: for any α<ω^{ω}, we can construct BPA processes P and Q for which P ≈_{α}^{!} Q. To see this, we consider the grammar G = (V, A, Γ) in which V = {X_{0}, X_{1}, …, X_{n−1}}, A = {a, τ}, and Γ consists of the following rules:

X_{0} →^{a} ε  X_{i} →^{τ} ε  X_{i+1} →^{τ} X_{i+1}X_{i}

For each α<ω^{n}, with Cantor normal form

α = ω^{n−1}a_{n−1} + ⋯ + ω^{2}a_{2} + ωa_{1} + a_{0},

let P_{α} = X_{0}^{a_{0}}X_{1}^{a_{1}}X_{2}^{a_{2}} ⋯ X_{n−1}^{a_{n−1}}. We can show that, for α<β<ω^{n}, P_{α} ≈_{α}^{!} P_{β}. This will follow from the following sequence of observations which demonstrate a close analogy between the processes P_{α} and the ordinal processes α from Remark 1:

– If P ≈ Q then RP ≈ RQ and P R ≈ QR. The first conclusion is true for every BPA process, while the second conclusion is true for every BPA process in which P ⇒^{τ} ε whenever P ≈ ε, which is certainly the case for the BPA process under consideration since in this case P ≈ ε implies that P = ε. (Proof: {(RP, RQ) : P ≈ Q} and {(P R, QR) : P ≈ Q} are easily verified to be weak bisimulation relations.)

– For i>j: X_{i}X_{j} ≈ X_{i}. (Proof: by induction on i−j.)

– Every state P ∈ V^{∗} is weakly bisimilar to some state P_{α}. (Proof: follows directly from the above observations.)

– X_{k} ⇒^{τ} P_{α} for every α≤ω^{k}. (Proof: easily verified.)

– P_{α} ⇒^{τ} P_{β} for every β≤α. (Proof: generalisation of the above observation.)

– P_{α} ⇒^{a} P_{β} for every β<α. (Proof: follows from the previous observation and the fact that P_{β+1} →^{a} P_{β}.)

– If P_{α} ⇒^{τ} P then P ≈ P_{β} for some β≤α. (Proof: easily verified.)

– If P_{α} ⇒^{a} P then P ≈ P_{β} for some β<α. (Proof: again easily verified.)

We thus arrive at the following important observations about the states P_{α}:

– P_{α} ⇒^{τ} P_{β} for all β≤α, and if P_{α} ⇒^{τ} P then P ≈ P_{β} for some β≤α; and

– P_{α} ⇒^{a} P_{β} for all β<α, and if P_{α} ⇒^{a} P then P ≈ P_{β} for some β<α.

This suffices to deduce with little effort, analogously to Remark 1, that if α<β then P_{α} ≈_{α}^{!} P_{β}. (The conjecture for BPA, though, is that the bound given by this construction is tight: ≈ = ≈_{ω^{ω}}.)

BPP processes with silent moves are countably-branching, and thus by Theorem 6 ≈ = ≈_{ℵ_{1}}. In [22] there is an argument attributed to J. Bradfield which shows that the approximation hierarchy collapses by the level ≈_{ω_{1}^{CK}}, the first non-recursive ordinal. (The argument is made there for BPA but clearly holds as well for BPP.) But this is to measure in lightyears what should require centimetres; we proceed here to a more modest bound, based on our ordinal analysis of Dickson’s Lemma.

We assume an underlying grammar (V, A, Γ) defining our BPP process, and recall that a state in the associated process is simply a sequence u ∈ V^{∗} viewed as a multiset. With this, we make the important observation about weak bisimulation approximants over BPP: besides being equivalences, they are in fact congruences.

Lemma 4. For all u, v, w ∈ V^{∗}, if u ≈_{α} v then uw ≈_{α} vw.

Proof. By a simple induction on α. □

We next observe a result due to Hirshfeld [10].

Lemma 5. If u ≈_{α}^{!} v and uu′ ≈_{β}^{!} vv′ with β < α then uu′ ≈_{β}^{!} uv′ and vu′ ≈_{β}^{!} vv′.

Proof. uu′ ≈_{β} uv′ since uu′ ≈_{β} vv′ ≈_{α} uv′. On the other hand, if uu′ ≈_{β+1} uv′ then uu′ ≈_{β+1} uv′ ≈_{α} vv′. Thus uu′ ≈_{β}^{!} uv′. (vu′ ≈_{β}^{!} vv′ can be shown similarly).

□

BPP processes, being multisets over the finite variable set V, can be represented as |V |-tuples over ℕ. Given non-equivalent BPP states u_{0} and v_{0}, omt(u_{0}, v_{0}) can then be viewed as a ℕ^{2·|V |}-labelled tree. In general this tree will not be non-dominating, but the above lemma will enable us to produce a non-dominating ℕ^{2·|V |}-labelled tree from omt(u_{0}, v_{0})

Lemma 6. For BPP processes, if u_{0} ≈_{α}^{!} v_{0} then there exists a ℕ^{2·|V |}-labelled non-dominating tree of height α.

Proof. We apply the following substitution procedure to each successive level of the weak-transition optimal move tree omt(u_{0}, v_{0}) (where the level of a node refers to the distance from the root (u_{0}, v_{0}) to the node) by induction on the levels:

For each node x at this level, if x dominates some ancestor node y, that is, if there exists an ancestor node y = (u, v) where x = (uu′, vv′), then replace the subtree rooted at x with either x′ = omt(uu′, uv′) (if u <_{lex} v) or with x′ = omt(vu′, vv′) (if v <_{lex} u). (If this x′ itself then dominates an ancestor node, repeat this action.)

That <_{lex} is a well-founded relation on ℕ^{2·|V |} means this repetition must halt; and Lemma 5 implies that this is a height-preserving operation. □

Theorem 7. Over BPP processes, ≈ = ≈_{ω^{ω}}

Proof. If u ≈ v then u ≈_{ω^{ω}} v is a given. If, on the other hand, u ≉ v, then u ≈_{α}^{!} v for some α, and by the combination of Lemma 6 and Theorem 2 we must have that α ≤ ω^{2·|V |}. Thus, u ≉_{ω^{ω}} v. □

5 Conclusions

In this paper we provide a bound on the level at which the bisimulation approximation relations collapse over BPP. The bound we give of ω^{ω} is still a far cry from the widely-accepted conjectured bound of ω×2, but it nonetheless represents the first nontrivial countable bound that has been discovered in the decade since this conjecture was first uttered (originally by Hirshfeld and Jančar).

We arrive at our bound through a careful analysis of Dickson’s Lemma, and in particular via a novel constructive proof which provides this ordinal bound on non-dominating sequences of n-tuples. (Dickson’s Lemma itself merely declares that such sequences are necessarily finite without actually identifying any ordinal bound.) This approach does not immediately seem to be applicable to strengthening the bound, given that this bound on Dickson’s Lemma is tight. However, it seems equally likely that by taking into consideration the restricted form of non-dominating sequences produced by BPP transitions we can identify the missing ingredient for the proof of the tighter bound.

There have been other similar constructive proofs of Dickson’s Lemma in the area of term rewriting. In particular, Sustik [23] provides a similar proof using an ordinal mapping on sequences in order to mechanically prove Dickson’s Lemma using the ACL2 theorem prover. However, the ordinal mapping defined by Sustik gives an inferior bound to the one we provide; in particular, it requires ω^{ω} already for sequences of pairs.

Blass and Gurevich have very recently (preprint March 2006) written a manuscript [1] in which they define the stature of a well partial ordering P to be the order type of nondominating sequences of P, and (amongst other things) derive the same tight bound of ω^{n} as we have done. Their application of interest lies in program termination, and their proofs, being of more general results, are more complicated than the proof we provide. We therefore feel that our proof, which appeared in an earlier mauscript [9], as well as our application to bisimulation checking is of independent interest.

If the ω×2 bound for the weak bisimulation approximation relations over BPP is resolved positively, this can potentially be exploited to resolve the decidability of weak bisimilarity over BPP. Esparza in [7] has shown that weak equivalence is semi-decidable, by demonstrating a semilinear witness of equivalence, so semi-decidability of non-equivalence is all that is required. If ≈_{ω} can be shown to be decidable (which is likely a much simpler result to attain than for ≈) then it would naturally be expected that the successor relations ≈_{ω+1}, ≈_{ω+1}, … would also be decidable, which would give rise to a semi-decision procedure for ≉_{ω×2}: test each relation ≈_{ω+i} in turn until one such test fails.

References

1. A. Blass and Y. Gurevich. Program termination and well partial orderings. Microsoft Technical Report MSR-TR-2006-27, 31 pages, March 2006. (Available at ftp://ftp.research.microsoft.com/pub/tr/TR-2006-27.pdf.)

2. O. Burkart, D. Caucal, F. Moller and B. Steffen. Verification over Infinite States. Chapter 9 in the Handbook of Process Algebra, pages 545-623, Elsevier Publishers, 2001.

3. S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for basic parallel processes. In Proceedings of the 4th International Conference on Concurrency Theory (CONCUR’93), LNCS 715, pages 143-157, Springer, 1993.

4. S. Christensen, Y. Hirshfeld, and F. Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS’93), pages 386-396, IEEE Computer Society Press, 1993.

5. S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In Proceedings of the 3rd International Conference on Concurrency Theory (CONCUR’92), LNCS 630, pages 138-147, Springer, 1992.

6. L.E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with distinct factors. American Journal of Mathematics 3:413-422, 1913.

7. J. Esparza. Petri nets, commutative context-free grammars, and basic parallel proceses. Fundamenta Informaticae 30:23-41, 1997.

8. R. Glabbeek. The linear time – branching time spectrum I: The semantics of concrete sequential processes. Chapter 1 in the Handbook of Process Algebra, pages 3-99, Elsevier Publishers, 2001.

9. W. Harwood and F. Moller. Weak bisimulation approximants. In Selected Papers from the CALCO Young Researchers Workshop (CALCO-jnr 2005), Swansea University Research Report CSR 18-2005, pages 27-40, December 2005. (Available at http://www-compsci.swan.ac.uk/reports/2005.html.)

10. Y. Hirshfeld. Bisimulation trees and the decidability of weak bisimulation. Electronic Notes in Theoretical Computer Science 5:2-13, 1997.

11. Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. In Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science (FOCS’94), pages 623-631, IEEE Computer Society Press, 1994.

12. Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science 15:143-159, 13. Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisim-

ulation equivalence of normed basic parallel processes. Mathematical Structures in Computer Science 6:251-259, 1996.

14. P. Jančar. Strong bisimilarity on Basic Parallel Processes is PSPACE-complete. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS’03), pages 218-227, IEEE Computer Society Press, 2003.

15. P. Jančar and F. Moller. Techniques for decidability and undecidability of bisimilarity. In Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99), LNCS 1664, pages 30-45, Springer, 1999.

16. F. Moller. Infinite Results. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96), LNCS 1119, pages 195-216, Springer, 1996.

17. J. Srba. Strong bisimilarity and regularity of Basic Process Algebra is PSPACEhard. In Proceedings of the 29th International Conference on Automata, Languages and Programming (ICALP’02), LNCS 2380, pages 716-727, Springer, 2002.

18. J. Srba. Strong bisimilarity and regularity of Basic Parallel Processes is PSPACEhard. In Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), LNCS 2285, pages 535-546, Springer, 2002.

19. J. Srba. Complexity of weak bisimilarity and regularity for BPA and BPP. Mathematical Structures in Computer Science 13:567-587, 2003.

20. J. Srba. Roadmap of Infinite Results. http://www.brics.dk/~srba/roadmap.

21. C. Stirling. Decidability of weak bisimilarity for a subset of Basic Parallel Processes. In Proceedings of Foundations of Software Science and Computation Structures (FOSSACS’01), LNCS 2030, pages 379-393, 2001.

22. J. Stříbrná. Approximating weak bisimulation on Basic Process Algebras. In Proceedings of Mathematical Foundations of Computer Science (MFCS’99), LNCS 1672, pages 366-375, 1999.

23. M. Sustik. Proof of Dickson’s Lemma using the ACL2 theorem prover via an explicit ordinal mapping. Unpublished presentation at the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003). (Available from http://www.cs.utexas.edu/users/moore/acl2/workshop-2003.)