Decidability of Bisimulation Equivalence for Normed Pushdown Processes

Colin Stirling Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK email: cps@dcs.ed.ac.uk

Abstract

We prove that bisimulation equivalence is decidable for normed pushdown processes.

1 Introduction

In the classical theory of automata the expressive power of pushdown automata is matched by context-free grammars. Both accept the same family of languages, the context-free languages. Concurrency theory requires a more intensional exposition of behaviour (as language equivalence need not be preserved in the presence of communicating abstract machines). Many finer equivalences have been proposed. Bisimulation equivalence, due to Park and Milner, has received much attention.

Baeten, Bergstra and Klop proved that bisimulation equivalence is decidable for irredundant context-free grammars (without the empty production). Within process calculus theory these grammars correspond to normed BPA processes. Their proof relies on isolating a complex periodicity from the transition graphs of these processes. Simpler proofs of the result soon followed which expose algebraic structure.

Caucal and Monfort showed that normed pushdown processes (the process analogue of irredundant pushdown automata without ϵ-transitions) are strictly more expressive than normed BPA with respect to bisimulation equivalence. In this paper we prove that bisimulation equivalence is decidable for this richer family of processes. However the proof is not easy, and does not follow immediately from the techniques used for showing decidability of normed BPA. One indication of this is that although the proof of decidability of bisimulation equivalence for BPP (Basic Parallel Processes) is similar to that for BPA bisimulation equivalence is undecidable for the pushdown extension to BPP.

2 Normed pushdown processes

Ingredients for describing pushdown processes are a finite set of states 𝒫 = {p_{1}, …, p_{k}}, a finite set of stack symbols Γ = {X_{1}, …, X_{m}}, a finite set of actions 𝒜 = {a_{1}, …, a_{n}} and a finite family of basic transitions, each of the form pX −)^{a} qα where p and q are states, a is an action, X is a stack symbol and α is a sequence of stack symbols. A pushdown process is then any expression pα, p ∈ 𝒫 and α ∈ Γ^{∗}, whose behaviour (transition graph) is determined by the basic transitions together with the following prefix rule, where β ∈ Γ^{∗}:

if pX −)^{a} qα then pXβ −)^{a} qαβ

This account follows the presentation of Caucal [8]. It is a slight redescription of classical pushdown automata (without ϵ-transitions and final states), as for instance in [20], viewing them as generators instead of as acceptors.

Example 1 Let 𝒫 = {p, q, r, s}, Γ = {X} and 𝒜 = {a, b, c, d}. The family of basic transitions is

{pX −)^{a} pXX, pX −)^{c} qϵ, pX −)^{b} rϵ, qX −)^{d} sX, sX −)^{d} qϵ, rX −)^{d} rϵ}

where ϵ is the empty stack sequence. The transition graph generated by pX is:

qϵ (−^{d} sX (−^{d} qX (−^{d} sXX (−^{d} qXX (−^{d} …
[ c  [ c  [ c  ⋮
pX  −)^{a}  pXX  −)^{a}  pXXX −)^{a} …
] b  ] b  ] b  ⋮
rϵ  (−^{d}  rX  (−^{d}  rXX (−^{d} …

For any n ≥ 0 the transition qXX^{n} −)^{d} sXX^{n} is derived from the basic transition qX −)^{d} sX using the prefix rule when β is X^{n}. □

Example 1 illustrates how a pushdown process may generate an infinite state transition graph. In the following we are interested in comparing the behaviour of two pushdown processes. Without loss of generality, we can assume that they are built from the same ingredients 𝒫, Γ, 𝒜 and basic transitions (as the appropriate disjoint union, with respect to states and stack symbols, of two pushdown descriptions is a pushdown description). One notion of behaviour of pα is the language it generates, which is the set of words {w ∈ 𝒜^{∗} : ∃q ∈ 𝒫. pα −)^{w} qϵ} where the extended transitions −)^{w} are defined in the usual way. Acceptance is by empty stack instead of by final state (see [20]). The process pX of Example 1 generates the language {a^{n}b d^{n} : n ≥ 0} ∪ {a^{n}c d^{2n} : n ≥ 0}. Any language generated by a pushdown process is context-free, and for each context-free language without the empty string there is a pushdown process which generates it. This remains true under the following restriction. A process pα is normed if every reachable process with a non-empty stack generates a non-empty language. (That is, for every qβ such that β ≠ ϵ and pα −)^{v} qβ for some v, there is a w and a state r, such that qβ −)^{w} rϵ.) Normedness amounts to irredundancy in the pushdown automaton. In the rest of the paper we assume this restriction to normed pushdown processes.

Each context-free language without the empty string is also generated by a normed pushdown process whose state set 𝒫 contains just one state. In which case 𝒫 is superfluous, and the result is a normed context-free or BPA process (in Greibach normal form). The stack symbols Γ are the nonterminals and basic transitions have the form X −)^{a} α. The prefix rule is: if X −)^{a} α then Xβ −)^{a} αβ. The language generated by a context-free process α is {w : α −)^{w} ϵ}. There is a standard transformation, see [20], which translates a normed pushdown process into a normed context-free process which generates the same language. With respect to languages, the expressive power of normed context-free processes is the same as normed pushdown processes.

Concurrency theory is built on a more intensional account of behavioural equivalence than that given by languages (as language equivalence need not be preserved in the presence of communicating abstract machines). A pivotal notion, due to Park and Milner, is bisimilarity which is finer than language equivalence on processes. Definition 1 A binary relation ℛ between processes is a bisimulation relation provided that whenever (E, F) ∈ ℛ, for all a

if E −)^{a} E′ then ∃F′. F −)^{a} F′ and (E′, F′) ∈ ℛ, and

if F −)^{a} F′ then ∃E′. E −)^{a} E′ and (E′, F′) ∈ ℛ.

Two processes E and F are defined to be bisimulation equivalent, or bisimilar, written E ∼ F, if there is a bisimulation relation ℛ relating them.

The transformation from pushdown processes to context-free processes does not preserve bisimulation equivalence. In fact, with respect to bisimilarity normed pushdown processes constitute a richer family than normed context-free processes, as shown by Caucal and Monfort [11]. (Independently [1] proves a variant of this result when introducing the state operator into process algebra.) Their proof is very elegant, and utilises the canonical graph of a process which is the quotient of its transition graph with respect to bisimulation equivalence. For instance, the canonical graph for Example 1 fuses together the pairs of vertices labelled qX^{n} and rX^{2n} for any n ≥ 0. Normed context-free processes are closed under canonical graphs in the sense that for each such canonical graph there is a normed context-free process whose transition graph is isomorphic to it. Normed pushdown processes fail to have this property. Caucal and Monfort show that Example 1 is a counterexample, as its canonical graph lacks the regular structure (as identified by Muller and Schupp [25]) that the transition graph of a pushdown process must possess: see [6] for further results about canonical graphs.

Burkart and Steffen provide additional insight into pushdown processes [4], by showing that, unlike context-free processes, they are closed under Hoare parallel composition with finite state processes (with respect to bisimilarity). Moreover they demonstrate that the family of pushdown processes is the smallest extension of context-free processes with this closure property.

Baeten, Bergstra and Klop proved that bisimulation equivalence is decidable for normed context-free processes [2, 3]. Simpler proofs were developed in [7, 15, 22, 17], and [19] showed that there is even a polynomial time decision procedure. The decidability result was generalized in [14] to encompass unnormed processes, and then refined in [5] to give upper bounds. Groote and Hüttel proved that other standard equivalences on processes (traces, failures, simulation, 2/3-bisimulation etc..,) are all undecidable [16]. Similar results were proved for Basic Parallel Processes, BPP, which are like context-free processes except that a process expression α is a multiset^{∗}. Christensen, Hirshfeld and Moller showed that bisimulation equivalence is decidable for normed BPP [12], and this result was generalised in [13] to include the unnormed case. Hüttel proved that the other equivalences are undecidable [21].

Decidability of bisimulation equivalence for normed pushdown processes is harder to show than for normed context-free processes. There are many reasons for this. First Baeten, Bergstra and Klop’s method is not applicable, as normed pushdown transition graphs need not display the periodicity upon which their proof relies. Secondly, the structural methods in the simplifed proofs of decidability, which appeal to decomposition and congruence, are not immediately applicable, as it is not clear what are the components of a pushdown process: a context-free process X_{1} …X_{n} is built from the subprocesses X_{i}, but a process pX_{1} …X_{n} does not contain X_{i} as a pushdown component. Perhaps the clearest indication of the increased difficulty is that for the pushdown extension of BPP^{†} bisimulation equivalence is undecidable, a result due to Hirshfeld (utilizing Jančar’s technique for showing undecidability of bisimilarity for Petri nets [23]): for details see the excellent survey [24].

∗The prefix rule becomes: if X −)^{a} α then δXβ −)^{a} δαβ.

The proof presented below of decidability of bisimulation equivalence for normed pushdown processes consists of two semi-decision procedures (for which we are unable to provide a complexity measure). One half of the proof is easy, as bisimilarity is characterizable using approximants when processes, such as pushdown processes, are image-finite^{‡}.

Definition 2 The family {∼_{n} : n ≥ 0} is defined inductively as follows

E ∼_{0} F for all processes E, F E ∼_{n+1} F iff for each a ∈ 𝒜

if E −)^{a} E′ then ∃F′. F −)^{a} F′ and E′ ∼_{n} F′, and

if F −)^{a} F′ then ∃E′. E −)^{a} E′ and E′ ∼_{n} F′

The following is a standard result.

Proposition 1 If E and F are image-finite then E ∼ F iff ∀n ≥ 0. E ∼_{n} F.

For each n ≥ 0, the relation ∼_{n} is decidable for pushdown processes, and therefore bisimulation inequivalence is semi-decidable via the simple procedure which seeks the least i such that pα ≁_{i} qβ. Therefore we just need to establish the semi-decidability of bisimulation equivalence. The crux of this part of the proof is that there is a finite tableau proof of pα ∼ qβ. As finite proofs can be enumerated, this amounts to a semi-decision procedure. The method generalises the technique developed by the author and Hüttel [22]. It relies upon exposure of structure within normed pushdown processes. We introduce a finer equivalence than bisimilarity to ensure a congruence, and we show that with respect to it pushdown processes can be taken apart, when extra stack symbols are introduced.

3 Congruence and cancellation

The following two key properties underpin decidability of bisimulation equivalence on normed context-free processes:

Congruence :  if α ∼ β then αδ ∼ βδ
Cancellation : if αδ ∼ βδ then α ∼ β

†When the prefix rule is: if pX −)^{a} qα then pδXβ −)^{a} qδαβ.

‡E is image-finite if for each w ∈ A^{∗} the set {F : E −)^{w} F} is finite.

Explicit use of these features can be seen in the decidability proof which uses tableaux [22]. (A more elegant proof of decidability of bisimilarity exploits the stronger property of unique prime decomposition, due to Hirshfeld [17].) In the more general case, when the restriction to being normed is lifted, congruence still holds but cancellation fails. However bisimulation equivalence remains decidable because of a weaker form of cancellation [14]: if there are infinitely many different δ (with respect to ∼) such that αδ ∼ βδ then α ∼ β.

Neither of these key properties is true of normed pushdown processes. A counterexample to congruence is that although qX ∼ rXX in Example 1 of the previous section, qXX ≁ rXXX. Example 1 also furnishes instances of failure of cancellation such as rX^{6} ∼ qXXX but rX^{5} ≁ qXX. Moreover, the weaker version of cancellation also fails.

Two pushdown processes can be bisimilar without agreeing on their final states when the stack empties: for instance the bisimulation relation between qX and rXX of Example 1 contains the pair (qϵ, rϵ). This explains why congruence (with respect to stacking) fails for pushdown processes. However by refining the definition of bisimulation equivalence we can ensure a congruence.

Definition 1 A binary relation ℛ on pushdown processes is an a-bisimulation provided that whenever (pα, qβ) ∈ ℛ, for all a ∈ 𝒜

if α = ϵ then β = ϵ and p = q, and if β = ϵ then α = ϵ and p = q, and

if pα −)^{a} p′α′ then ∃q′β′. qβ −)^{a} q′β′ and (p′α′, q′β′) ∈ ℛ, and

if qβ −)^{a} q′β′ then ∃p′α′. pα −)^{a} p′α′ and (p′α′, q′β′) ∈ ℛ.

The “a” stands for “agreeing”, as the first two clauses require final states to be the same when processes terminate. Two pushdown processes pα and qβ are a-bisimilar, written pα ≡ qβ, if there is an a-bisimulation relating them. Note that the earlier two processes qX and rXX are not a-bisimilar. Later, in this section, we shall relate bisimilarity and a-bisimilarity.

Not surprisingly a-bisimilarity is an equivalence relation, and it is also a congruence with respect to stacking.

Proposition 1 The relation ≡ is an equivalence relation.

Proposition 2 If pα ≡ qβ then pαδ ≡ qβδ.

A-bisimilarity can also be characterized using approximants.

Definition 2 The family {≡_{n} : n ≥ 0} is defined inductively on pushdown processes as follows: pϵ ≡_{0} pϵ for any state p, and pα ≡_{0} qβ for any p, q, α ≠ ϵ and β ≠ ϵ. pα ≡_{n+1} qβ iff pα ≡_{0} qβ, and for each a ∈ 𝒜,

if pα −)^{a} p′α′ then ∃q′β′. qβ −)^{a} q′β′ and p′α′ ≡_{n} q′β′, and

if qβ −)^{a} q′β′ then ∃p′α′. pα −)^{a} p′α′ and p′α′ ≡_{n} q′β′.

The base relation ≡_{0} does not include all pairs of pushdown processes. For example any pair pϵ, qβ (when p ≠ q) is excluded.

Proposition 3 pα ≡ qβ iff ∀n ≥ 0. pα ≡_{n} qβ.

Our next concern is to provide a mechanism for composing and decomposing pushdown processes. We extend pushdown descriptions by augmenting their stack symbols Γ with a finite family of stack constants 𝒲. Assume that the state set of the pushdown description is 𝒫 = {p_{1}, …, p_{k}}. Each new stack symbol W ∈ 𝒲 has an associated definition

W =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k})

where each q_{i} ∈ 𝒫, and each δ_{i} is a sequence of stack elements, possibly including constants. However we assume that if δ_{i} ≠ ϵ then its first symbol belongs to Γ. The intention is that for each state p_{j} ∈ 𝒫 the behaviour of p_{j}W is that of q_{j}δ_{j}, the jth component of the definition of W^{§}. An extended pushdown process is an expression pα where α = ϵ or α ∈ Γ(Γ ∪ 𝒲)^{∗}. Basic transitions are unaffected, remaining of the form pX −)^{a} qα where X ∈ Γ and α ∈ Γ^{∗}. However the prefix rule is generalised to

if pX −)^{a} qα then pXβ −)^{a} [qαβ]

where bracketing […] is defined as follows:

[p_{i}ϵ]  = p_{i}ϵ, and
[p_{i}Xβ] = p_{i}Xβ when X ∈ Γ, and
[p_{i}Wβ] = [q_{i}δ_{i}β] when W =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k})

Therefore if pα is an extended pushdown process and w ∈ 𝒜^{∗} and pα −)^{w} qβ then qβ is also an extended pushdown process.

A-bisimilarity remains a congruence in the presence of constants.

Proposition 4 If pXα ≡ qYβ then pXαW ≡ qYβW.

Constants also provide a handle for composing pushdown processes, as illustrated by the next two results whose proofs are routine.

§This selection notation (…) for pushdown processes is used in [26, 4].

Proposition 5 If W =^{def} (q_{1}δ_{1}β, …, q_{k}δ_{k}β) and V =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k}) then

pXαW ≡ pXαVβ.

Proposition 6 If W =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k}) and V =^{def} (r_{1}λ_{1}, …, r_{k}λ_{k}) and for

each i : 1 ≤ i ≤ k, q_{i}δ_{i} ≡ r_{i}λ_{i} then pXαW ≡ pXαV.

It is time to examine the condition of being normed more carefully. The norm of a process pα, when α may contain constants, is a k-tuple (n_{1}, …, n_{k}) where each n_{i} ∈ ℕ ∪ {⊥}. The component n_{i} is either the length of a shortest word w such that pα −)^{w} p_{i}ϵ or there is no such word and n_{i} is the undefined element ⊥. We let n(pα) be the norm of pα, and we let n(pα)_{i} be its ith component. The restriction to normed processes implies that at least one entry in a norm is different from ⊥. Let max(pα) be the maximum defined entry in n(pα) and min(pα) be the least defined entry. Finally we let D(pα) be the set {i : n(pα)_{i} ≠⊥}. We can now slightly refine the previous Proposition.

Proposition 7 If W =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k}) and V =^{def} (r_{1}λ_{1}, …, r_{k}λ_{k}) and for

each i ∈ D(pXα). q_{i}δ_{i} ≡ r_{i}λ_{i} then pXαW ≡ pXαV.

Two useful measures on a pushdown description are now defined. First M is just greater than the maximum norm of a stack symbol in Γ:

M =^{def} 1 + max{max(pX) : p ∈ 𝒫 and X ∈ Γ}

And second G is the maximum length of a stack sequence on the right hand side of a basic transition (where | | is “length of”):

G =^{def} max{|α| : pX −)^{a} qα is a basic transition }

The family of finite constants 𝒲 is partitioned into two. First are simple constants. Each has a definition U =^{def} (q_{1}δ_{1}, …, q_{k}δ_{k}) where each δ_{i} ∈ Γ^{+} and |δ_{i}| ≤ MG: constants are not allowed in their definition, and neither is the empty stack. Up to renaming of constants, there are only finitely many different simple constants, because of the constraint on their length. We now come to the first substantive result, where simple constants are used to provide a format for cancellation.

Lemma 1 If pXα ≡ qβδ and β ∈ Γ^{+} and max(pX) < min(qβ) and |β| ≤ M then there is a simple U =^{def} (q_{1}γ_{1}, …, q_{k}γ_{k}) such that

1. pXUδ ≡ qβδ, and

2. for all i ∈ D(pX). [p_{i}α] ≡ q_{i}γ_{i}δ.

Proof: Suppose pXα ≡ qβδ and β ∈ Γ^{+} and max(pX) < min(qβ) and |β| ≤ M. For each i ∈ D(pX) consider a shortest w_{i} such that pX −)^{w_{i}} p_{i}ϵ.

Therefore, pXα −)^{w_{i}} [p_{i}α]. Since pXα ≡ qβδ we know that qβδ −)^{w_{i}} q_{i}λ_{i} and

[p_{i}α] ≡ q_{i}λ_{i}. However, as max(pX) < min(qβ) it follows that λ_{i} = γ_{i}δ and qβ −)^{w_{i}} q_{i}γ_{i} and γ_{i} ≠ ϵ, and as β ∈ Γ^{+} this means that γ_{i} ∈ Γ^{+}. Also because

|w_{i}| < M (and |β| ≤ M) it follows that |γ_{i}| ≤ MG. Let U =^{def} (q_{1}γ_{1}, …, q_{k}γ_{k})

where for each i ∈ D(pX) q_{i}γ_{i} is determined as above and for each i ∉ D(pX), q_{i}γ_{i} = pX. By definition U is a simple constant, and by construction 2 holds. By induction on n it follows that for any p′α′ such that α′ ∈ Γ^{+} and D(p′α′) ⊆ D(pX), p′α′Uδ ≡_{n} p′α′α. Therefore pXUδ ≡ pXα, which implies 1. □

The other constants in W are recursive. Each recursive constant has a definition V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}), where each λ_{i} is either the empty sequence or of the form λ′_{i}V where V is the defining constant and λ′_{i} is a non-empty sequence of stack symbols which may contain simple (but not recursive) constants. Their first use is to relate bisimilarity and a-bisimilarity. Let I =^{def} (p_{1}ϵ, …, p_{1}ϵ) be an initial degenerate recursive constant. Clearly the following holds.

Proposition 8 pXα ∼ qYβ iff pXαI ≡ qYβI.

The second and more substantive use of recursive constants is to provide a very delicate form of cancellation which turns out to be sufficiently strong for showing semi-decidability of a-bisimilarity. Simple cancellation, if pαδ ≡ qβδ then pα ≡ qβ, fails as does the more refined notion, if pαδ ≡ qβδ for infinitely many different δ then pα ≡ qβ. What could be even weaker? The idea is, roughly speaking, if pαδ ≡ qβδ for infinitely many δ then there are just finitely many “regular shapes” such that each δ has one of these shapes, where the notion of shape is captured using recursive constants. More precisely, we state the exact result.

Lemma 2 Fix pX and qβ assuming that β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ). There is a finite set of recursive constants 𝒱 such that for any α which does not contain recursive constants and for any δ if pXαδ ≡ qβδ then there is a V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) in 𝒱 such that

1. pXαV ≡ qβV, and

2. for all j ∈ D(pXα) ∪ D(qβ). if λ_{j} = ϵ then [p_{j}δ] ≡ [q_{j}δ], and

3. for all j. if λ_{j} = λ′_{j}V then [p_{j}δ] ≡ q_{j}λ′_{j}δ.

We shall prove this result in two stages.

The first stage is central, and shows how a family of finite shapes can be iteratively constructed.

Lemma 3 Fix pXα and qYβ assuming that α and β do not contain recursive constants. There exists a finite family 𝒱 of recursive constants such that for any δ if pXαδ ≡ qYβδ then there is a V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) in 𝒱 such that

1. pXαV ≡ qYβV, and

2. for all i ∈ D(pXα) ∪ D(qYβ). if λ_{i} = ϵ then [p_{i}δ] ≡ [q_{i}δ], and

3. for all i. if λ_{i} = λ′_{i}V then [p_{i}δ] ≡ q_{i}λ′_{i}δ.

Proof: Let Δ = {δ : pXαδ ≡ qYβδ}. If Δ is empty then let 𝒱 be empty, and the result holds. Otherwise assume a total ordering on the state set {p_{1}, …, p_{k}}, so that p_{i} < p_{j} whenever i < j. We say that the recursive constant V is definitionally equivalent to V′ if their definitions are the same except for their occurrences of V and V′: in which case, for all n ≥ 0, pXαV ≡_{n} pXαV′ for any p, X and α.

For each δ ∈ Δ we define the family {V_{i}^{δ} : 0 ≤ i ≤ k^{2}} iteratively, so that for each i properties 2 and 3 hold for V_{i}^{δ} and property 1 holds when i = k^{2}. Furthermore, for each i the set {V_{i}^{δ} : δ ∈ Δ} when quotiented by definitional equivalence is finite. From this the result follows by taking 𝒱 to be the family {V_{k^{2}}^{δ} : δ ∈ Δ} after quotienting by definitional equivalence.

The element V_{0}^{δ} =^{def} (p_{1}ϵ, …p_{k}ϵ). Clearly, both 2 and 3 hold, and the set {V_{0}^{δ} : δ ∈ Δ} is a singleton up to definitional equivalence. Assume V_{i}^{δ} for 0 ≤ i < k^{2} has been defined, and that both 2 and 3 hold for it, and that the set {V_{i}^{δ} : δ ∈ Δ} is finite up to definitional equivalence. If property 1 is also true then let V_{j}^{δ}, for all j : i ≤ j ≤ k^{2} be V_{i}^{δ}. Otherwise V_{i+1}^{δ} is constructed as a refinement of V_{i}^{δ}. As 1 fails there is a least n ≥ 0 such that pXαV_{i}^{δ} ≢_{n} qYβV_{i}^{δ}, and we know that n > 0. However, we also know that

pXαδ ≡ qYβδ. Hence pXα −)^{a} [p′_{1}α_{1}] and qYβ −)^{a} [q_{1}β_{1}] for some a and

p′_{1}α_{1} and q_{1}β_{1} such that [p′_{1}α_{1}δ] ≡ [q_{1}β_{1}δ] and [p′_{1}α_{1}V_{i}^{δ}] ≢_{n−1} [q_{1}β_{1}V_{i}^{δ}]. The sequences α_{1} and β_{1} do not contain recursive constants. If both α_{1} and β_{1} are non-empty then we can obtain a subsequent pair p′_{2}α_{2} and q_{2}β_{2} such that [p′_{2}α_{2}δ] ≡ [q_{2}β_{2}δ] and [p′_{2}α_{2}V_{i}^{δ}] ≢_{n−2} [q_{2}β_{2}V_{i}^{δ}], and so on. Therefore as n is finite we must reach a pair p′_{j}α_{j} and q_{j}β_{j} such that [p′_{j}α_{j}δ] ≡ [q_{j}β_{j}δ] and [p′_{j}α_{j}V_{i}^{δ}] ≢_{n−j} [q_{j}β_{j}V_{i}^{δ}], where α_{j} or β_{j} is empty (and neither contain recursive constants).

Without loss of generality assume that α_{j} = ϵ. Let rλ be the entry for p′_{j} in V_{i}^{δ}. There are two cases. Case 1 λ = ϵ. Now consider β_{j}. First assume that β_{j} ≠ ϵ. Let V_{i+1}^{δ} be V_{i}^{δ} except that q_{j}β_{j}V_{i+1}^{δ} is associated with the state p′_{j} instead of rϵ (and throughout the other entries V_{i+1}^{δ} replaces V_{i}^{δ}). Clearly properties 2 and 3 hold for V_{i+1}^{δ} given that they hold for V_{i}^{δ}. Next assume instead that β_{j} = ϵ. Assume that sγ is q_{j}’s entry in V_{i}^{δ}. There are two subcases. First, γ ≠ ϵ. Then V_{i+1}^{δ} is V_{i}^{δ} except that sγ is associated with p′_{j} (and throughout all entries V_{i+1}^{δ} replaces V_{i}^{δ}). Second, γ = ϵ. If p′_{j} < q_{j} in the total order on states V_{i+1}^{δ} is V_{i}^{δ} except that rϵ is associated with q_{j} instead of sϵ, and if q_{j} < p′_{j} then V_{i+1}^{δ} is V_{i}^{δ} except that sϵ is associated with p′_{j} (and in both cases throughout the other entries V_{i+1}^{δ} replaces V_{i}^{δ}). Again clearly properties 2 and 3 both hold for V_{i+1}^{δ}. Case 2 λ ≠ ϵ, and so λ = λ′V_{i}^{δ}. Again consider β_{j}. If β_{j} ≠ ϵ then as [p′_{j}δ] ≡ q_{j}β_{j}δ by 3 we know that [p′_{j}δ] ≡ rλ′δ, and so rλ′δ ≡ q_{j}β_{j}δ. However rλ′V_{i}^{δ} ≢_{n−j} q_{j}β_{j}V_{i}^{δ} (as [p′_{j}α_{j}V_{i}^{δ}] = rλ′V_{i}^{δ}). Therefore the proof proceeds as before by defining further pairs r_{m}λ′_{m} and q_{j+m} β_{j+m} such that [r_{m}λ′_{m}δ] ≡ [q_{j+m} β_{j+m} δ] and [r_{m}λ′_{m}V_{i}^{δ}] ≢_{n−(j+m)} [q_{j+m} β_{j+m} V_{i}^{δ}]. Otherwise β_{j} = ϵ. Let sγ be the entry for q_{j} in V_{i}^{δ}. If γ = ϵ then we proceed as in case 1 above (with the α and β roles reversed). If γ ≠ ϵ then γ = γ′V_{i}^{δ} where γ′ does not contain recursive constants. By 3 for V_{i}^{δ} [q_{j}δ] ≡ sγ′δ and [p′_{j}δ] ≡ rλ′δ and therefore rλ′δ ≡ sγ′δ, and also rλ′V_{i}^{δ} ≢_{n−j} sγ′V_{i}^{δ}. Therefore again we define further pairs r_{m}λ′_{m} and s_{m}γ′_{m} such that [r_{m}λ′_{m}δ] ≡ [s_{m}γ′_{m}δ], and [r_{m}λ′_{m}V_{i}^{δ}] ≢_{n−(j+m)} [s_{m}γ′_{m}V_{i}^{δ}]. As n is finite there can only be finitely many invocations of 3 before V_{i}^{δ} is updated according to the first case.

The construction of V_{i+1}^{δ} updates exactly one entry in V_{i}^{δ} which must be of the form rϵ. The update becomes either non-empty or is replaced by an empty entry from an earlier state in the total order. For each V_{i}^{δ} the number of possible different recursive constants V_{i+1}^{δ} by this construction given that pXαV_{i}^{δ} ≢_{n} qYβV_{i}^{δ} (with n least) is finite. Consequently the set {V_{i+1}^{δ} : δ ∈ Δ} is finite up to definitional equivalence. Moreover given the regime for updating, there can be at most k^{2} updates, and therefore pXαV_{k^{2}}^{δ} ≡ qYβV_{k^{2}}^{δ}. □

This takes us to the proof of Lemma 2.

Proof of Lemma 2: Assume pX and qβ where β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ). We show the following: There exists a finite family 𝒰 of simple constants and a finite family 𝒱 of recursive constants such that for any α not containing recursive constants and for any δ if pXαδ ≡ qβδ then there is a U =^{def} (r_{1}γ_{1}, …, r_{k}γ_{k}) in 𝒰 and a

V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) in 𝒱 such that

1. pXUV ≡ qβV, and

2. for all j ∈ D(pX). [p_{j}αV] ≡ r_{j}γ_{j}V, and

3. for all j ∈ D(pXα) ∪ D(qβ). if λ_{j} = ϵ then [p_{j}δ] ≡ [q_{j}δ], and

4. for all j. if λ_{j} = λ′_{j}V then [p_{j}δ] ≡ q_{j}λ′_{j}δ.

Lemma 2 now follows because 1 and 2 imply that pXαV ≡ qβV (using Propositions 5 and 7). Let Δ = {(α, δ) : pXαδ ≡ qβδ}. If Δ is empty let 𝒰 and 𝒱 be empty, and the result follows. Otherwise Δ is non-empty. By Lemma 1 for each (α, δ) ∈ Δ there is a simple U =^{def} (r_{1}γ_{1}, …, r_{k}γ_{k}) such that pXUδ ≡ qβδ and for all j ∈ D(pX). [p_{j}αδ] ≡ r_{j}γ_{j}δ. By the construction in Lemma 1 we know that there are only finitely many such U (as each component of their definition is drawn from the set {q′γ′ : qβ −)^{w} q′γ′ for |w| ≤ max(pX)}). Let U_{1}, …, U_{l} be the different simple constants. We partition Δ

into sets Δ_{1}, …, Δ_{l} such that for each (α, δ) ∈ Δ_{t}, with U_{t} =^{def} (r_{1}γ_{1}, …, r_{k}γ_{k}),

pXU_{t}δ ≡ qβδ and for all j ∈ D(pX). [p_{j}α_{i}δ] ≡ r_{j}γ_{j}δ. By Lemma 3 for each Δ_{t} there are finitely many recursive V such that pXU_{t}V ≡ qβV and for each (α, δ) ∈ Δ_{t} one of these recursive constants V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) has the property that [p_{j}δ] ≡ [q_{j}λ′_{j}δ] for all j ∈ D(qβ) ∪ D(pXU_{t}) (where if λ_{j} = λ′V then λ′_{j} = λ′ and if λ_{j} = ϵ then λ′_{j} = ϵ). Let 𝒱_{t} be this finite family of recursive constants. The proof is finished if for each (α, δ) ∈ Δ_{t} there is a V ∈ 𝒱_{t} such that for all j ∈ D(pX). [p_{j}αV] ≡ q_{j}γ_{j}V. Using a similar proof method to that in Lemma 3 we refine this set of recursive constants so that it becomes true. Let 𝒱_{t0} be 𝒱_{t}. Take the least n such that there is an (α, δ) ∈ Δ_{t} and

V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) ∈ 𝒱_{t0} with [p_{j}δ] ≡ [q_{j}λ′_{j}δ] for all j ∈ D(qβ) ∪ D(pXα)

such that [p_{j}αV] ≢_{n} q_{j}γ_{j}V. However we know that [p_{j}αδ] ≡ q_{j}γ_{j}δ. Therefore, by the technique in the proof of Lemma 3 this means that for some j, [p_{j}V] ≢_{0} [q′λV] and [p_{j}δ] ≡ [q′λδ] and the jth component of V, q_{j}λ_{j}, has the form rϵ. We now update V. There are two cases. First if λ ≠ ϵ then each entry rϵ in V is replaced with q′λV. If λ = ϵ then replace each entry rϵ with the entry for q′ (which cannot be rϵ). All other entries in V remain untouched. Call the resulting constant V′. A small exercise shows that for any α and β if [pαV] ≡ [qβV] then [pαV′] ≡ [qβV′] (and so, in particular, pXU_{t}V′ ≡ qβV′): this is the reason why all entries rϵ are updated at once. Let 𝒱_{t1} be 𝒱_{t0} with V replaced by V′. Now keep repeating the procedure. As with the argument in Lemma 3 the number of possible updates must be finite (here less than rk^{2} where r is the number of constants in 𝒱_{t0}). □

4 Tableaux

Given a pushdown description and two normed processes pα and qβ, the aim is to show semi-decidability of pα ∼ qβ. If α = ϵ or β = ϵ then checking for decidability is clear. Otherwise the problem reduces to decidability of pαI ≡ qβI where I is the initial recursive constant. Therefore, we need to extend the pushdown description with a finite family of stack constants 𝒲. As we saw in the previous section we can include all potential simple constants. For the recursive constants we have no such upper bound (and hence the reason for semi-decidability). However, besides the initial constant I, we only need to introduce a finite family (see Lemma 2 of the previous section) for pairs pX and qβ, β ∈ Γ^{+}, and |β| ≤ M, and for which there is an α and a δ such that pXαδ ≡ qβδ.

We complete the decidability result by presenting a tableau proof system for a-bisimilarity. The proof system is goal directed, and consists of a finite set of rules each of the form

\frac{Goal}{Subgoal_{1} … Subgoal_{n}} 𝒞

where Goal is what currently is to be proved and the subgoals are what it reduces to, and 𝒞 is a possible side condition on the rule application. Each goal and subgoal has the form pα = qβ (the proof analogue of pα ≡ qβ) where the constituents are extended normed pushdown processes. Each rule is backwards sound: if all the subgoals are true then so is the goal. As we are dealing with infinite state systems there is also the important notion of when a current goal counts as terminal, for the rules only apply to nonterminals. Terminal goals are classified as either successful or unsuccessful. A tableau proof for Goal is a finite proof tree, whose root is Goal and all of whose leaves are successful terminals, and all of whose inner subgoals are the result of an application of one of the rules to the goal immediately above them. If the successful terminals are true it follows that the root goal is also true. We show that pXα ∼ qYβ iff there is a tableau proof for pXαI = qYβI.

The tableau proof rules are presented in Figure 1. There is a cancellation rule CAN which introduces recursive constants and a reduction rule RED which introduces simple constants: their formulation directly reflects the important Lemmas of the previous section. The third rule is unfold UNF: for each transition from pXα there is a corresponding transition from qYβ, and the resulting pairs become subgoals (and vice-versa). A tableau is built from proof steps, possibly interspersed with applications of UNF. A proof step has the form

pXαδ = qβδ \overline{CAN}

…[q_{i}λ′_{i}δ] = [p_{i}δ] … pXαV = qβV ; \overline{RED} ; …[p_{j}αV] = q_{j}γ_{j}V … pXUV = qβV ; \overline{UNF} ; …

or when CAN is not applicable, it has the form Cancellation (CAN)

\frac{pXαδ = qβδ}{[q_{i1}λ′_{i1}δ] = [p_{i1}δ] …[q_{il}λ′_{il}δ] = [p_{il}δ] pXαV = qβV} C1

Condition C1:

1. β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ) and |δ| > 1, and 2. V =^{def} (q_{1}λ_{1}, …q_{k}λ_{k}) is recursive, and

3. D(pXα) ∪ D(qβ) = {i1, …, il}, and

4. if λ_{ij} = ϵ then λ′_{ij} = ϵ, and if λ_{ij} = λ′′V then λ′_{ij} = λ′′.

Reduction (RED)

\frac{pXα = qβδ}{[p_{i1}α] = q_{i1}γ_{i1}δ … [p_{il}α] = q_{il}γ_{il}δ pXUδ = qβδ} C2

Condition C2:

1. β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ) and |δ| > 1, and

2. U =^{def} (q_{1}γ_{1}, …, q_{k}γ_{k}) is simple, and D(pX) = {i1, …, il}.

Unfold (UNF)

\frac{pXα = qYβ}{p_{1}α_{1} = q_{1}β_{1} … p_{l}α_{l} = q_{l}β_{l}} C3

Condition C3: For any a

1. if pXα −)^{a} p′α′ then ∃i : 1 ≤ i ≤ l. p′α′ = p_{i}α_{i} and qYβ −)^{a} q_{i}β_{i},

2. if qYβ −)^{a} q′β′ then ∃i : 1 ≤ i ≤ l. q′β′ = q_{i}β_{i} and pXα −)^{a} p_{i}α_{i}.

Figure 1: Tableau rules Successful terminals

1. pα = pα

2. pα = qβ and in the proof tree the same equation pα = qβ occurs above on the path to the root.

Unsuccessful terminals

1. pϵ = qϵ and p ≠ q

2. pα = qβ and min(pα) ≠ min(qβ)

3. pα = qβ and pα −)^{a} but not(qβ −)^{a} )

4. pα = qβ and qβ −)^{a} but not(pα −)^{a} )

Figure 2: Terminal nodes

pXα = qβδ \overline{RED}

…[p_{i}α] = q_{i}γ_{i}δ … pXUδ = qβδ ; \overline{CAN} ; …[q_{j}λ′_{j}δ] = [p_{j}δ] … pXUV = qβV ; \overline{UNF} ; …

The idea is to repeat proof steps whose roots are themselves leaves of a proof step except when the side conditions for CAN and RED do not apply in which case the UNF rule is applied instead. The proof step starting with CAN takes priority over the one starting with RED, which takes priority over the use of UNF. Note that a recursive constant may only appear as a final stack symbol, and that simple constants are only explicitly introduced into processes on the left side of =: they can appear on the right hand side of = through the presence of recursive constants, when a process becomes [q_{i}V].

The conditions for being a terminal node are described in Figure 2. A node labelled pα = qβ in a proof tree is a successful terminal if it is an identity (qβ is pα) or a repeat: that is, there is a node above it on the path to the root also labelled pα = qβ. In the conditions for being an unsuccessful terminal we use the standard notation rλ −)^{a} as an abbreviation for ∃r′λ′. rλ −)^{a} r′λ′. Clearly, if a node labelled pα = qβ is an unsuccessful terminal then pα ≢ qβ.

The tableau proof rules are backwards sound with respect to the approximants ≡_{n}, and this fact is used in the following soundness result.

Lemma 1 If there is a tableau proof for pα = qβ then pα ≡ qβ.

Proof: It is straightforward to show that for any n ≥ 0 if all the leaves p′_{i}α′_{i} = q′_{i}β′_{i} of a proof step have the property that p′_{i}α′_{i} ≡_{n} q′_{i}β′_{i} then the root of the proof step p′α′ = q′β′ has the property p′α′ ≡_{n+1} q′β′. This is clearly the case for the UNF rule. For the other two proof steps it follows by a similar kind of backwards soundness for the rules CAN and RED: in the case of CAN if each leaf [q_{ij}λ′_{ij}δ] = [p_{ij}δ] has the property [q_{ij}λ′_{ij}δ] ≡_{n} [p_{ij}δ] and the leaf pXαV = qβV has the property pXα ≡_{n+1} qβV then the root pXαδ = qβδ obeys pXαδ ≡_{n+1} qβδ, and in the case of RED if each leaf [p_{ij}α] = q_{ij}γ_{ij}δ has the property [p_{ij}α] ≡_{n} q_{ij}γ_{ij}δ and the leaf pXUδ = qβδ has the feature pXUδ ≡_{n+1} qβδ then the root pXα = qβδ is such that pXα ≡_{n+1} qβδ.

Assume that there is a successful tableau built using proof steps with root pα = qβ, and suppose that pα ≢ qβ. Clearly it can not be the case that pα ≢_{0} qβ (for then pα = qβ would be an unsuccessful terminal). Hence there is a least n such that pα ≡_{n} qβ and pα ≢_{n+1} qβ. Consequently there is a leaf p′α′ = q′β′ of the first proof step such that p′α′ ≢_{n} q′β′ by backwards soundness described above. Take the leaf p_{i1}α_{i1} = q_{i1}β_{i1} for which there is a least n1 such that p_{i1}α_{i1} ≡_{n1} q_{i1}β_{i1} and p_{i1}α_{i1} ≢_{n1+1} q_{i1}β_{i1} (and so n1 < n). Repeatedly apply this argument. At each stage we have a root of a proof step p_{ij}α_{ij} = q_{ij}β_{ij} such that p_{ij}α_{ij} ≡_{nj} q_{ij}β_{ij} and p_{ij}α_{ij} ≢_{nj+1} q_{ij}β_{ij}, and nj < nl whenever j > l. As the tableau is finite, this sequence picks out a finite path through the tableau (when the intermediate subgoals between the root of a proof step and its chosen leaf are added). However the tableau is successful and so the final goal is a successful terminal. Clearly it can not be an identity p′α′ = p′α′ since p′α′ ≡_{n} p′α′ for all n ≥ 0. Consequently the final goal p′α′ = q′β′ also occurs earlier in the path. But now we have a contradiction as there can not be nj and nl (with nj ≠ nl) where p′α′ ≡_{nj} q′β′ and p′α′ ≢_{nj+1} q′β′ and p′α′ ≡_{nl} q′β′ and p′α′ ≢_{nl+1} q′β′. □

Now the main result which shows completeness of the tableau method.

Theorem 1 pXα ∼ qYβ iff there is a tableau proof for pXαI = qYβI.

Proof: One half follows by Lemma 1 above and Proposition 8 of the previous section: if there is a tableau proof for pXαI = qYβI then pXα ∼ qYβ. For the other half suppose pXα ∼ qYβ. By Proposition 8 pXαI ≡ qYβI. We now construct a tableau proof for pXαI = qYβI. First we introduce all the appropriate constants. For each pX and qβ, β ∈ Γ^{+}, |β| ≤ M and where max(pX) < min(qβ), we define finite sets of constants as determined by Lemmas 1 and 2 of the previous section. Now we repeatedly build proof steps that preserve truth until we reach terminals. Lemma 2 of the previous section and the introduction of constants guarantee that if pXαδ = qβδ is a subgoal with β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ) and |δ| > 1 then the proof step whose initial rule is CAN is applicable. If CAN is not applicable to pXα = qβδ and β ∈ Γ^{+} and |β| ≤ M and max(pX) < min(qβ) and |δ| > 1 then the other proof step applies. Otherwise the rule UNF is always applicable to a nonterminal subgoal (as any process in a tableau has the form pXα or pϵ). Clearly, as truth is preserved it is not possible to reach an unsuccessful terminal goal.

The only impediment is the possibility that the proof construction never ends, that we build a proof tree with an infinite path. The rest of the proof shows that this is impossible. Note that because of normedness, for each k ≥ 1 the set {rδ : for some pα such that |α| < k, rδ ≡ pα and δ and α contain at most one recursive constant} is finite.

Let S be the following measure

max({|λ_{i}| + M : V =^{def} (q_{1}λ_{1}, …, q_{k}λ_{k}) is recursive } ∪ {MG + 2} ∪ {4})

In a goal pα = qβ we say that pα is a left process and qβ is a right process. Note the following observations:

1. Any occurrence of a left or right process has at most one recursive constant which can only appear as the final stack symbol.

2. The only way that simple constants can be introduced into a right process is through the UNF rule, in the circumstance that pXα = qYV and qY −)^{a} rϵ: this means that in a right process qβUδ where U is simple, |Uδ| < S.

3. The only circumstance that both CAN and RED are not applicable to a nonterminal goal pXα = qβδ, |β| ∈ Γ^{+}, is when max(pX) ≮ min(qβ) and δ = ϵ or δ = V or δ = Uδ_{1} and U is simple. In which case |βδ| < S.

Suppose p_{1}α_{1} = q_{1}β_{1}, …, p_{n}α_{n} = q_{n}β_{n}, … is an infinite path of distinct goals in the tableau (with p_{1}α_{1} = pXαI and q_{1}β_{1} = qYβI). Let g_{i} be the ith goal in this sequence. We show that there must be a repeat goal in this sequence: for some i goal g_{i} is a terminal. A little notation. Consider the rule that takes g_{i} to g_{i+1}: if the rule is UNF we say g_{i+1} is an UNF successor of g_{i}, if the rule is CAN then we say it is an l-successor if it is of the form [q_{i}λ′_{i}δ] = [p_{i}δ] and an r-successor if it has the form pXαV = qβV. Similarly, if the rule is RED then we say it is an l-successor if it is of the form [p_{i}α] = q_{i}γδ and an r-successor if it has the form pXUδ = qβδ.

The following are true for the sequence g_{1}, …, g_{n}, …

1. There is an i such that for all j ≥ i the goal g_{j} is not an r-successor of CAN because the right process of such a goal has the form qβV where |β| < M (and so |βV| < S).

2. There is an i such that for all j ≥ i the goal g_{j} is not an UNF successor. First by 1 above there is an i such that no later goal is an UNF successor via the two kinds of proof steps (as it would then be preceded by a right successor of CAN). Secondly, by observation 3 earlier CAN and RED are not applicable to a goal only when its right process is small.

Hence there is a suffix g_{i}, …, g_{n}, … of goals such that each goal is a successor of RED or an l-successor of CAN. If in this suffix the goal g_{j} is an r-successor of RED then g_{j+1} is an l-successor of CAN. Clearly, there cannot be j ≥ i such that for all k ≥ j the goal g_{k} is an l-successor of CAN as each application reduces the right process by at least one stack symbol. Similarly, there cannot be j ≥ i such that for all k ≥ j the goal g_{k} is an l-successor of RED as each application reduces the left process by one stack symbol, except when a simple constant or a recursive constant is encountered: in the first case the stack may temporarily expand but the number of simple constants is reduced by one and in the second case, whenever a recursive constant is exposed the left process has size less than S. Consequently infinitely often there must be a change over from l-successors of CAN to a successor of RED. Consider any subsequence g_{i}, …, g_{i+k} of goals which are l-successors of CAN and such that CAN is not applicable to g_{i+k}. So g_{i+k−1} has the form pXαδ = qβδ and g_{i+k} has the form [q_{i}λ′_{i}δ] = [p_{i}δ]: either δ is small (of length less than M + 2) or δ has the form β_{1}Uδ_{1} where U is simple (and |β_{1}| ≤ M). Hence either |βδ| < S or the right process of g_{i+k} has size less than S. Hence there can not be such an infinite sequence of goals without a repeat. □

5 Conclusion and open questions

We have shown that bisimulation equivalence is decidable for normed pushdown processes. However, no complexity measure is available as the decision procedure essentially relies on Lemma 2 of Section 3. Moreover, it is not clear if the proof can be generalised to include unnormed pushdown processes: the main problem is that we are then unable to show completeness of the tableau proof system.

Normed BPA processes and normed pushdown processes are two means for generating the context-free languages (without the empty string). These languages are also generable using richer descriptions. Let Γ be a finite family of nonterminals and 𝒜 a finite family of actions. A basic transition has the form α −)^{a} β where α, β ∈ Γ^{∗} and a ∈ 𝒜. We can then define a process as a sequence of nonterminals whose behaviour is determined by the basic transitions together with the prefix rule:

PRE if α −)^{a} β then αδ −)^{a} βδ

The notion of normed process is then appropriately definable (for instance by utilising a finite set of final states which have no transitions, as in [24]).

In the table below is a Caucal hierarchy of process descriptions according to how the family of basic transitions is specified. In each case we assume a finite family of rules. Type 3 captures finite-state processes, Type 2 captures BPA processes in Greibach normal form, and Type 1\frac{1}{2}, in fact, captures pushdown processes. For Type 0 and below this means that in each case there are finitely many basic transitions. In the other cases R_{1} and R_{2} are regular expressions over the nonterminals. The idea is that each rule R_{1} −)^{a} β stands for the possibly infinite family of basic transitions

{α −)^{a} β : α ∈ R_{1}} and R_{1} −)^{a} R_{2} stands for the family {α −)^{a} β : α ∈

R_{1} and β ∈ R_{2}}. For instance a Type −1 rule of the form X^{∗}Y −)^{a} Y includes for each n the basic transition X^{n}Y −)^{a} Y.

Basic Transitions

Type −2 R_{1} −)^{a} R_{2}
Type −1 R_{1} −)^{a} β
Type 0 α −)^{a} β
Type 1\frac{1}{2} α −)^{a} β where |α| = 2 and |β| > 0
Type 2 X −)^{a} β
Type 3 X −)^{a} Y or X −)^{a} ϵ

This Caucal hierarchy is implicit in Caucal’s work on understanding context-free graphs, and understanding when the monadic second-order theory of graphs is decidable [8, 7, 9, 6, 10]. With respect to language equivalence, there is no distinction between Type −2 and Type 2. With respect to bisimulation equivalence this is not the case. However Caucal showed in [8] that Type 0 processes coincide (up to isomorphism of their transition graphs) with pushdown processes (and hence Type 1\frac{1}{2} processes). Consequently a corollary of the main result in this paper is that bisimulation equivalence is decidable for normed Type 0 processes. This leaves as open questions whether it is also decidable for normed processes in Type −1 and Type −2. These could turn out to be very difficult open questions, as we note below. One other reason for interest in these problems is that decidability questions about weak bisimulation can be coded as decidability questions about strong bisimulation at a higher level in the hierarchy: for instance, weak bisimulation of totally normed BPA processes can be coded into strong bisimulation of normed pushdown processes [18].

Another area for further work is the long standing issue of decidability of language equivalence for deterministic pushdown automata, DPDA. These are normed deterministic pushdown processes which also have ϵ moves. When processes are deterministic language equivalence coincides with bisimulation equivalence. Hence the result proved in this paper generalises [26] which proves decidability of language equivalence for realtime DPDA accepting by the empty stack: a real-time DPDA has no ϵ moves. However the proof method is very different: [26] uses Valiant’s parallel stacking technique whereas the method here relies on congruence and cancellation. Further work is needed to establish whether we can offer new insight into this difficult open problem. However this problem is related to the open questions above, as a DPDA with ϵ transitions can be coded as Type −1 process without ϵ transitions. For a different perspective on these issues see [9].

Acknowledgement: The author would like to thank Mojmir Kretinsky whose visit to Edinburgh rekindled the work reported here, and Olaf Burkart and Didier Caucal for comments on an earlier draft.

References

[1] Baeten, J. and Bergstra, J. (1991). Recursive process definitions with the state operator. Theoretical Computer Science, 82, 285-302.

[2] Baeten, J., Bergstra, J., and Klop, J. (1987). Decidability of bisimulation equivalence for processes generating context-free languages. Lecture Notes in Computer Science, 259, 94-113.

[3] Baeten, J., Bergstra, J., and Klop, J. (1993). Decidability of bisimulation equivalence for processes generating context-free languages. Journal of Association of Computing Machinery, 40, 653-682.

[4] Burkart, O., and Steffen, B.(1995). Composition, decomposition, and model checking of pushdown processes. Nordic Journal of Computing, 2, 89-125.

[5] Burkart, O., Caucal, D., and Steffen, B. (1994). An elementary decision procedure for arbitrary context-free processes. Tech. Report 94-28, RWTH Aachen (extended version of Lecture Notes in Computer Science, 969, 423-433).

[6] Burkart, O., Caucal, D., and Steffen, B. (1996). Bisimulation collapse and the process taxonomy. Lecture Notes in Computer Science, 1119, 247-262.

[7] Caucal, D. (1990). Graphes canoniques de graphes algébriques. Informatique Théorique et Applications (RAIRO), 24,339-352.

[8] Caucal, D. (1992). On the regular structure of prefix rewriting. Theoretical Computer Science, 106, 61-86.

[9] Caucal, D. (1995). Bisimulation of context-free grammars and of pushdown automata. CSLI Lecture Notes, 53, 85-106.

[10] Caucal, D. (1996). On infinite transition graphs having a decidable monadic theory. Lecture Notes in Computer Science, 1099, 194-205.

[11] Caucal, D., and Monfort, R. (1990). On the transition graphs of automata and grammars. Lecture Notes in Computer Science, 484, 311-337.

[12] Christensen, S., Hirshfeld, Y., and Moller, F. (1993). Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. Proceedings 8th Annual Symposium on Logic in Computer Science, IEEE Computer Science Press.

[13] Christensen, S., Hirshfeld, Y., and Moller, F. (1993). Bisimulation is decidable for basic parallel processes. Lecture Notes in Computer Science, 715, 143-157.

[14] Christensen, S., Hüttel, H., and Stirling, C. (1995). Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121, 143-148.

[15] Groote, J. (1992). A short proof of the decidability of bisimulation for normed BPA processes. Information Processing Letters, 42, 167-171.

[16] Groote, J., and Hüttel, H. (1994). Undecidable equivalences for basic process algebra. Information and Computation, 115, 354-371.

[17] Hirshfeld, Y. (1994). Deciding equivalences in simple process algebras. Tech. Report ECS-LFCS-94-294, Edinburgh University.

[18] Hirshfeld, Y. (1996). Bisimulation trees and the decidability of weak bisimulations. To appear.

[19] Hirshfeld, Y., Jerrum, M., and Moller, F. (1994). A polynomial algorithm for deciding bisimilarity of normed context-free processes. Procs. IEEE 35th Annual Symposium on Foundations of Computer Science, 623-631.

[20] Hopcroft, J., and Ullman, J. (1979). Introduction to Automata Theory, Languages, and Computation, Addison-Wesley.

[21] Hüttel, H. (1994). Undecidable equivalences for basic parallel processes. Lecture Notes in Computer Science, 789.

[22] Hüttel, H., and Stirling, C. (1991). Actions speak louder than words: proving bisimilarity for context free processes. Proceedings 6th Annual Symposium on Logic in Computer Science, IEEE Computer Science Press, 376-386.

[23] Jančar, P. (1994). Decidability questions for bisimilarity of Petri nets and some related problems. Lecture Notes in Computer Science, 775, 581-594.

[24] Moller, F. (1996). Infinite results. Lecture Notes in Computer Science, 1119, 195-216.

[25] Muller, D., and Schupp, P. (1985). The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37, 51-75.

[26] Oyamuguchi, M., Honda, N., and Inagaki, Y. (1980). The equivalence problem for real-time strict deterministic languages. Information and Control, 45, 90-115.