BRICS RS-02-16 J. Srba: Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds BRICS

Basic Research in Computer Science

Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds

Jiří Srba

BRICS Report Series RS-02-16 ISSN 0909-0878 April 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Jiří Srba.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

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

This document in subdirectory RS/02/16/

Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds^{⋆}

Jiří Srba^{⋆⋆}
BRICS^{⋆ ⋆ ⋆}

Department of Computer Science, University of Aarhus, Ny Munkegade bld. 540, 8000 Aarhus C, Denmark

                              srba@brics.dk

Abstract. In this paper we study bisimilarity problems for simple process algebras. In particular, we show PSPACE-hardness of the following problems: (i) strong bisimilarity of Basic Parallel Processes (BPP), (ii) strong bisimilarity of Basic Process Algebra (BPA), (iii) strong regularity of BPP, and (iv) strong regularity of BPA. We also demonstrate NL-hardness of strong regularity problems for the normed subclasses of BPP and BPA. Bisimilarity problems for simple process algebras are introduced in a general framework of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided.

1 Introduction

An important question in the area of verification of infinite-state systems is that of equivalence checking [3]. In this paper we are interested in equivalence checking problems for simple process algebras, namely for the purely sequential case called Basic Process Algebra (BPA) and its parallel analogue called Basic Parallel Processes (BPP). These two formalisms occupy the lowest levels in most of the process hierarchies considered in the literature so far [6, 23, 21].

Strong bisimilarity [25, 22] is a well accepted notion of behavioural equivalence for concurrent processes. Unlike all other equivalences in van Glabbeek’s spectrum (see [32, 33]), strong bisimilarity is decidable for BPA [9] and BPP [8]. This challenging phenomenon was a motivation for further investigation of strong bisimilarity in the class of simple process algebras. Restricted classes of so called normed processes were studied (a process is normed if from every reachable state there is at least one

⋆ A revised and extended version of [28] and [29]. ⋆⋆ The author is supported in part by the GACR, grant No. 201/00/0400.

⋆ ⋆ ⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

terminating computation), with surprising results that even though language equivalence is still undecidable for normed BPA [13] and BPP [14], strong bisimilarity becomes decidable even in polynomial time [11, 12]. However, the situation is different for the unrestricted classes of simple process algebras.

Despite the fact that strong bisimilarity of BPA appeared to be decidable in 2-EXPTIME [4], it is still an open problem whether there exists an elementary decision algorithm for BPP. The conjecture that strong bisimilarity of unnormed BPP is decidable (as well as in the normed case) in polynomial time was only recently proved false (unless P=NP) by Mayr. He showed that strong bisimilarity of BPP is co-NP-hard [20]. No nontrivial lower bound was known for unnormed BPA.

We improve Mayr’s co-NP lower bound for BPP and show that the complexity of bisimilarity checking of BPA is indeed different (unless P=PSPACE) from the case of normed BPA by demonstrating that strong bisimilarity of BPA and BPP is PSPACE-hard. We describe polynomial time reductions from the quantified satisfiability (QSAT) problem (for PSPACE-completeness see e.g. [24]) to strong bisimilarity checking problems for BPA and BPP. Given an instance C of QSAT, we construct a pair of BPA (BPP) processes P_{1} and P_{2} such that P_{1} and P_{2} are strongly bisimilar if and only if C is true.

The new contribution is a general technique which enables to imitate a generation of quantified assignments of boolean formulas in the context of bisimulation games of an attacker and a defender. While the truth value of a variable prefixed by the universal quantifier is being chosen, the attacker has the possibility to decide between two alternatives in the continuation of the bisimulation game. On the other hand, while choosing the truth value for an existentially quantified variable, the defender can force the attacker to continue the bisimulation game according to his decision^{1}. Satisfied clauses of the formula are remembered by means of process constants that are present in the current states of BPA and BPP systems. After the whole assignment of boolean variables was generated, the attacker can make a final check whether all clauses are indeed satisfied. This is easier to verify for BPP because we have a parallel access to all process constants contained in the current state. To achieve the same result for BPA, we have to encode satisfied clauses in a unary way.

Another decidability problem that has attracted much attention is that of regularity checking. The question is whether a given BPA (or BPP)

1 Similar ideas appeared independently also due to Jančar in connection with high undecidability of weak bisimilarity for Petri nets [15].

process is strongly bisimilar to some finite-state process. Strong regularity checking is decidable in 2-EXPTIME for BPA [5, 4] and in polynomial time for normed BPA and BPP [18]. Decidability of strong regularity for BPP follows from the fact that the problem is decidable even for Petri nets [16], a proper superclass of BPP. However, no elementary upper bound has been established so far. It is known that strong regularity is co-NP-hard for BPP [20] and no hardness result was available for BPA. We describe polynomial time reductions from strong bisimilarity of regular BPA (BPP) processes to strong regularity checking of BPA (BPP). By using our PSPACE-hardness of strong bisimilarity for BPA and BPP, and by the fact that the involved processes are strongly regular, we conclude that strong regularity of BPA and BPP are PSPACE-hard problems.

Finally, we also investigate the complexity of regularity checking problems for normed BPA and BPP and show their NL-completeness.

The paper is structured as follows. Basic background is introduced in Section 2 and the general idea of our reduction from QSAT to strong bisimilarity checking is explained in the beginning of Section 3. Next two subsections further develop the idea and show PSPACE-hardness of strong bisimilarity for BPP (Subsection 3.2) and then also for the more involved case of BPA (Subsection 3.3). Regularity checking problems are studied in Section 4: proofs of PSPACE-hardness for BPP and BPA are given in Subsections 4.1 and 4.2, respectively, and NL-completeness of regularity checking under the assumption of normedness is discussed in Subsection 4.3. An overview of the state of the art of bisimilarity and regularity checking problems for BPA and BPP is presented in Section 5.

2 Basic Definitions

2.1 Transition Systems, Bisimilarity

Semantics to process algebras is usually given in terms of (infinite-state) labelled transition systems [26]. Processes are understood as nodes of a certain labelled transition system and the transition relation is defined in a compositional way.

Definition 1 (Labelled transition system). A labelled transition system T is a triple T = (S, Act, ⟶) where

– S is a set of states (or processes),

– Act is a set of labels (or actions), and

– ⟶ ⊆ S × Act × S is a transition relation, written α ⟶^{a} β, for (α, a, β) ∈ ⟶.

As usual we extend the transition relation to the elements of Act^{∗}, i.e., α ⟶^{ϵ} α for every α ∈ S, and α ⟶^{aw} β iff α ⟶^{a} α′ and α′ ⟶^{w} β for every α, β ∈ S, a ∈ Act and w ∈ Act^{∗}.

We write α ⟶^{∗} β iff α ⟶^{w} β for some w ∈ Act^{∗}. We also write α −̸→^{a} whenever there is no β such that α ⟶^{a} β, and α −̸→ whenever α −̸→^{a} for all a ∈ Act.

Definition 2 (Process and its reachable states). A process is a pair (α, T) where T = (S, Act, ⟶) is a labelled transition system and α ∈ S. We say that β ∈ S is reachable in (α, T) iff α ⟶^{∗} β.

Definition 3 (Finite-state process). Whenever (α, T) has only finitely many reachable states, we call it a finitestate process.

Definition 4 (Strong bisimilarity). Let T = (S, Act, ⟶) be a labelled transition system. A binary relation R ⊆ S × S is a strong bisimulation iff whenever (α, β) ∈ R then for each a ∈ Act:

– if α ⟶^{a} α′ then β ⟶^{a} β′ for some β′ such that (α′, β′) ∈ R

– if β ⟶^{a} β′ then α ⟶^{a} α′ for some α′ such that (α′, β′) ∈ R.

Processes (α_{1}, T) and (α_{2}, T) are strongly bisimilar, written (α_{1}, T) ∼ (α_{2}, T) (or simply α_{1} ∼ α_{2} if T is clear from the context), iff there is a strong bisimulation R such that (α_{1}, α_{2}) ∈ R. Given a pair of processes (α_{1}, T_{1}) and (α_{2}, T_{2}) such that T_{1} and T_{2} are different labelled transition systems, we write (α_{1}, T_{1}) ∼ (α_{2}, T_{2}) iff (α_{1}, T) ∼ (α_{2}, T) where T is a disjoint union of T_{1} and T_{2}.

Definition 5 (Strong regularity). We say that a process (α, T) is strongly regular iff there exists some finite-state process bisimilar to it.

Bisimulation equivalence has an elegant characterisation in terms of bisimulation games.

Definition 6 (Bisimulation game). A bisimulation game on a pair of processes (α_{1}, T) and (α_{2}, T) where T = (S, Act, ⟶) is a two-player game of an ‘attacker’ and a ‘defender’. The game is played in rounds on pairs of states from S × S. In each round the players change the current states β_{1} and β_{2} (initially α_{1} and α_{2}) according to the following rule.

1. The attacker chooses an i ∈ {1, 2}, a ∈ Act and β′_{i} ∈ S such that

β_{i} ⟶^{a} β′_{i}.

2. The defender responds by choosing β′_{3−i} ∈ S such that β_{3−i} ⟶^{a} β′_{3−i}.

3. The states β′_{1} and β′_{2} become the current states.

A play is a maximal sequence of pairs of states formed by the players according to the rule described above, and starting from the initial states α_{1} and α_{2}. The defender is the winner in every infinite play. A finite play is lost by the player who is stuck. Note that the attacker gets stuck in current states β_{1} and β_{2} if and only if both β_{1} −̸→ and β_{2} −̸→.

The following proposition is a standard one (see e.g. [30, 31]).

Proposition 1. Processes (α_{1}, T) and (α_{2}, T) are strongly bisimilar iff the defender has a winning strategy (and nonbisimilar iff the attacker has a winning strategy).

2.2 Process Rewrite Systems

Let Act and Const be sets of actions and process constants, respectively, such that Act ∩ Const = ∅.

Definition 7 (Process expressions). We define the class of process expressions G over Const by the following abstract syntax

E ::= ϵ | X | E.E | E||E

where ‘ϵ’ is the empty process, X ranges over Const, the operator ‘.’ stands for a sequential composition and ‘||’ stands for a parallel composition.

Definition 8 (Structural congruence). We do not distinguish between process expressions related by a structural congruence, which is the smallest congruence over process expressions such that the following laws hold:

– ‘.’ is associative,

– ‘||’ is associative and commutative, and

– ‘ϵ’ is a unit for ‘.’ and ‘||’.

Definition 9 (Classes of process expressions). We distinguish the following classes of process expression:

G, the class of general process expressions introduced in Definition 7,

[figure: G; S; P; 1]

Fig. 1. Classes of Process Expressions

S, a subclass of G which contains all process expressions from G that do

not contain the ‘||’ operator, P, a subclass of G which contains all process expressions from G that do

not contain the ‘.’ operator, and 1, a subclass of G which contains only the process constants from Const

and the empty process ‘ϵ’.

Obviously, 1 ⊂ S, 1 ⊂ P, S ⊂ G and P ⊂ G. The classes S and P are incomparable and S ∩ P = 1. See Figure 1.

Remark 1. We use the notation G(Const), S(Const), P(Const) and 1(Const) whenever we need to explicitly specify from which process constants the expressions are formed.

Definition 10 (Process rewrite system (PRS) [21]). Let α, β ∈ {1, S, P, G} such that α ⊆ β. An (α, β)-PRS is a finite set Δ ⊆ α × Act × β of rewrite rules, written E ⟶^{a} F for (E, a, F) ∈ Δ. Moreover, we require that E ≠ ϵ.

Remark 2. Let us denote the set of actions and process constants that appear in Δ by Act(Δ) and Const(Δ), respectively. Note that Act(Δ) and Const(Δ) are finite sets.

Definition 11 (Transition system T (Δ)). Let Δ be an (α, β)-PRS. The system Δ determines a labelled transition system T (Δ) = (β, Act(Δ), ⟶), where states are process expressions from the class β (modulo the structural congruence introduced in Definition 8), Act(Δ) is the set of labels, and transition relation is the least relation satisfying the SOS rules from Figure 2 — recall that ‘||’ is commutative.

Definition 12 ((α, β)-process). An (α, β)-process is a process (P, T (Δ)) — see Definition 2 — where Δ is an (α, β)-PRS and P ∈ β is a process expression.

\frac{(E ⟶^{a} E′) ∈ Δ}{E ⟶^{a} E′}  \frac{E ⟶^{a} E′}{E.F ⟶^{a} E′.F}  \frac{E ⟶^{a} E′}{E||F ⟶^{a} E′||F}

Fig. 2. SOS rules

[figure: {(G, G)-PRS \atop PRS}; {(S, G)-PRS \atop PAD}; {(P, G)-PRS \atop PAN}; {(S, S)-PRS \atop PDA}; {(1, G)-PRS \atop PA}; {(P, P)-PRS \atop PN}; {(1, S)-PRS \atop BPA}; {(1, P)-PRS \atop BPP}; {(1, 1)-PRS \atop FS}]

Fig. 3. Hierarchy of process rewrite systems

We remind the reader of the fact that Definitions 2 to 5 define the corresponding process properties also for (α, β)-processes. Moreover, in the rest of this paper we denote an (α, β)-process (P, T (Δ)) by only (P, Δ), or even P if Δ is clear from the context.

Definition 13 (Normed (α, β)-process). An (α, β)-process (P, Δ) is normed iff from every reachable state E in (P, Δ) there is a terminating computation, i.e., E ⟶^{∗} ϵ.

Many classes of infinite-state systems studied so far — e.g. basic process algebra (BPA), basic parallel processes (BPP), pushdown automata (PDA), Petri nets (PN) and process algebra (PA) — are contained in the hierarchy of process rewrite systems presented in Figure 3. This hierarchy is strict w.r.t. strong bisimilarity and we refer the reader to [21] for further discussions.

In this paper we study the two bottom classes BPA and BPP.

2.3 Basic Process Algebra

Basic Process Algebra (BPA) — or equivalently (1, S)-PRS — represents the class of processes introduced by Bergstra and Klop (see [2]). This class corresponds to the transition systems associated with context-free grammars in Greibach normal form (GNF), in which only left-most derivations are allowed.

Let Δ be a BPA process rewrite system. Every rewrite rule from Δ is of the form

X ⟶^{a} E

where X ∈ Const(Δ), a ∈ Act(Δ) and E ∈ S(Const(Δ)). It is usually assumed that for each X ∈ Const(Δ) there is at least one rewrite rule in Δ, i.e., that there is some a ∈ Act(Δ) and E ∈ S(Const(Δ)) such that (X, a, E) ∈ Δ. If it is not the case, we say that the system contains deadlocks. A study of decidability problems for BPA with deadlocks is provided in [27].

Remark 3. Let m be a natural number and A ∈ Const be a process constant. Whenever it is clear from the context that we consider only the ‘.’ operator, we use the notation A^{m} for a sequential composition of m occurrences of A, i.e., A^{0} =^{def} ϵ and A^{m+1} =^{def} A^{m}.A.

A simple BPA system is presented in the following example.

Example 1. Let Const(Δ) = {Q_{1}, Q_{2}, …, Q_{k}} for a natural number k > 0 and let Act(Δ) = {a}. Consider the following BPA system Δ containing the rewrite rules:

\begin{matrix}Q_{1} ⟶^{a} ϵ \\ Q_{j+1} ⟶^{a} Q_{j} & for all j, 1 ≤ j < k. \end{matrix}

Observe that Q_{j} ⟶^{a^{j}} ϵ for every j, 1 ≤ j ≤ k, and no other transitions are possible. Also notice that e.g. (Q_{1}^{5}, Δ) ∼ (Q_{1}.Q_{2}^{2}, Δ) — see Remark 3.

Assume now that m_{1}, m_{2} > 0 are natural numbers. For every ℓ_{1}, 1 ≤ ℓ_{1} ≤ m_{1}, and every ℓ_{2}, 1 ≤ ℓ_{2} ≤ m_{2}, let i_{ℓ_{1}} ∈ {1, 2, …, k} and j_{ℓ_{2}} ∈ {1, 2, …, k}. It is an easy observation that

(Q_{i_{1}}.Q_{i_{2}}. · · · .Q_{i_{m_{1}}} , Δ) ∼ (Q_{j_{1}}.Q_{j_{2}}. · · · .Q_{j_{m_{2}}} , Δ)

if and only if

∑_{ℓ_{1}=1}^{m_{1}} i_{ℓ_{1}} = ∑_{ℓ_{2}=1}^{m_{2}} j_{ℓ_{2}}.

This example demonstrates that even though the BPA class is non-commu-tative, we can achieve a restricted commutative behaviour by assuming that Act(Δ) is a singleton set and by encoding process constants in this unary alphabet.

2.4 Basic Parallel Processes

Basic Parallel Processes (BPP) — or equivalently (1, P)-PRS — are a fragment of CCS [22] without restriction, relabelling and communication. This class was first studied by Christensen [7], and it is equivalent to the communication-free subclass of Petri nets (each transition has exactly one input place).

Let Δ be a BPP process rewrite system. Every rewrite rule from Δ is of the form

X ⟶^{a} E

where X ∈ Const(Δ), a ∈ Act(Δ) and E ∈ P(Const(Δ)). Unlike BPA, the presence of deadlocks in BPP systems is not essential. Assume that D ∈ Const(Δ) is a deadlock, i.e., D −̸→. Then (E, Δ) ∼ (E||D, Δ) for any expression E ∈ P(Const(Δ)) and we can safely replace all occurrences of such deadlocks in Δ by the empty process ‘ϵ’.

Remark 4. Let m be a natural number and A ∈ Const be a process constant. Whenever it is clear from the context that we consider only the ‘||’ operator, we use the notation A^{m} for a parallel composition of m occurrences of A, i.e., A^{0} =^{def} ϵ and A^{m+1} =^{def} A^{m}||A.

The following example aims to demonstrate that the operator ‘||’ in BPP systems allows a parallel access to all process constants contained in the current state.

Example 2. Let Const(Δ) = {Q_{1}, Q_{2}, …, Q_{k}} for a natural number k > 0 and let Act(Δ) = {q_{1}, q_{2}, …, q_{k}}. The set of rewrite rules Δ is defined by:

Q_{j} ⟶^{q_{j}} Q_{j} for all j, 1 ≤ j ≤ k.

Assume now that m_{1}, m_{2} > 0 are natural numbers. For every ℓ_{1}, 1 ≤ ℓ_{1} ≤ m_{1}, and every ℓ_{2}, 1 ≤ ℓ_{2} ≤ m_{2}, let i_{ℓ_{1}} ∈ {1, 2, …, k} and j_{ℓ_{2}} ∈ {1, 2, …, k}. We conclude that

(Q_{i_{1}}||Q_{i_{2}}|| ⋯ ||Q_{i_{m_{1}}} , Δ) ∼ (Q_{j_{1}}||Q_{j_{2}}|| ⋯ ||Q_{j_{m_{2}}} , Δ)

if and only if

{i_{1}, i_{2}, …, i_{m_{1}}} = {j_{1}, j_{2}, …, j_{m_{2}}}.

In other words, the processes are strongly bisimilar if and only if for all j, 1 ≤ j ≤ k, the process constant Q_{j} appears either in both sides of the processes or in neither of them. In the first case the number of occurrences of Q_{j} is irrelevant since (Q_{j}^{m}, Δ) ∼ (Q_{j}, Δ) for any natural number m > 0 — see Remark 4.

2.5 Definitions of Problems

Problem: Strong bisimilarity of BPA (BPP)

Instance: Two BPA (BPP) processes (P_{1}, Δ) and (P_{2}, Δ).

Question: (P_{1}, Δ) ∼ (P_{2}, Δ) ?

Problem: Strong regularity of BPA (BPP) Instance: A BPA (BPP) process (P, Δ). Question: Is there a finite-state process (F, Δ′) such that

(P, Δ) ∼ (F, Δ′) ?

The main results of Section 3 are proved by polynomial time reductions from a PSPACE-complete problem called quantified satisfiability (QSAT) [24]. We use a version where the prefix of quantifiers starts with the existential one.

Problem: \underline{QSAT}

Instance: A natural number n > 0 and a boolean formula ϕ in conjunctive normal form with boolean variables x_{1}, …, x_{n} and y_{1}, …, y_{n}.

Question: Is ∃x_{1}∀y_{1}∃x_{2}∀y_{2} … ∃x_{n}∀y_{n}.ϕ true?

A literal is a variable or the negation of a variable. An instance of QSAT is a formula C of the form

C ≡ ∃x_{1}∀y_{1}∃x_{2}∀y_{2} … ∃x_{n}∀y_{n}. C_{1} ∧ C_{2} ∧ … ∧ C_{k}

where each clause C_{j}, 1 ≤ j ≤ k, is a disjunction of literals.

   [figure: X; a; a; a; Y^{choice}; one; two; Y^{one}; Y^{two}; Z⊕α_{one}; Z⊕α_{two}]

                                    \xymatrix{ &  &  & X′ \ar[dll]_{a} \ar[drr]^{a} \\  & Y^{one} \ar[dl]_{one} \ar[dr]^{two} &  &  &  & Y^{two} \ar[dl]_{two} \ar[dr]^{one} \\ Z′⊕α_{one} &  & Z⊕α_{two} &  & Z′⊕α_{two} &  & Z⊕α_{one}}

Fig. 4. Processes (X, Δ) and (X′, Δ)

3 Lower Bounds for Strong Bisimilarity

In this section we study strong bisimilarity problems for BPA and BPP.

3.1 The Main Idea

We try to explain here the main idea of PSPACE-hardness proofs given in Subsections 3.2 and 3.3. Our aim is to make the rewrite rules defined in this paper more readable, by demonstrating a general pattern used heavily (with small modifications) later on. Let us consider the following process rewrite system Δ where α_{one} and α_{two} are some fixed process expressions and ⊕ is either a sequential or parallel composition.

             X ⟶^{a} Y^{choice}

X ⟶^{a} Y^{one}  X′ ⟶^{a} Y^{one}
X ⟶^{a} Y^{two}  X′ ⟶^{a} Y^{two}

             Y^{choice} ⟶^{one} Z⊕α_{one} Y^{one} ⟶^{one} Z′⊕α_{one}
             Y^{choice} ⟶^{two} Z⊕α_{two} Y^{two} ⟶^{two} Z′⊕α_{two}
             Y^{one} ⟶^{two} Z⊕α_{two}  Y^{two} ⟶^{one} Z⊕α_{one}

Transition systems generated by processes (X, Δ) and (X′, Δ) are depicted in Figure 4. The intuition behind the construction can be nicely explained in terms of bisimulation games. Consider a bisimulation game starting from the pair X and X′.

The attacker is forced to make the first move by playing X ⟶^{a} Y^{choice} because in all other possible moves, either from X or X′, the defender can make the resulting processes syntactically equal and hence bisimilar. The defender’s answer to the move X ⟶^{a} Y^{choice} is either (i) X′ ⟶^{a} Y^{one} or

(ii) X′ ⟶^{a} Y^{two}.

In the next round starting from (i) Y^{choice} and Y^{one} or (ii) Y^{choice} and Y^{two}, the attacker can use either the action one or two — obviously it is irrelevant whether the chosen action is performed in the first or in the second process. In case (i), if the attacker chooses the action one then the players reach the pair Z⊕α_{one} and Z′⊕α_{one}. If he chooses the action two then the players reach a pair of syntactically equal states, namely Z⊕α_{two} and Z⊕α_{two}, from which the defender has an obvious winning strategy. In case (ii), if the attacker chooses the action two then the players reach the pair Z ⊕α_{two} and Z′⊕α_{two}. If he chooses the action one then he loses as in case (i). Now, either the defender won by reaching syntactically equal states, or the resulting processes after two rounds are (i) Z ⊕α_{one} and Z′⊕α_{one} or (ii) Z⊕α_{two} and Z′⊕α_{two}. Note that it was the defender who had the possibility to decide between adding α_{one} or α_{two}.

We can repeat this construction several times in a row, which is explained in more detail in the following two subsections.

3.2 Strong Bisimilarity of BPP

In this subsection we show that strong bisimilarity of BPP is a PSPACEhard problem. We prove it by reduction from QSAT. Let

C ≡ ∃x_{1}∀y_{1}∃x_{2}∀y_{2} … ∃x_{n}∀y_{n}. C_{1} ∧ C_{2} ∧ … ∧ C_{k}

be an instance of QSAT. We define the following BPP processes (X_{1}, Δ) and (X′_{1}, Δ) where

Const(Δ) =^{def} {Q_{1}, …, Q_{k}} ∪
{X_{1}, …, X_{n+1}, Y_{1}^{choice}, …, Y_{n}^{choice}, Z_{1}, …, Z_{n}} ∪

{X′_{1}, …, X′_{n+1}, Y_{1}^{tt}, …, Y_{n}^{tt}, Y_{1}^{ff}, …, Y_{n}^{ff}, Z′_{1}, …, Z′_{n}}

and Act(Δ) =^{def} {q_{1}, …, q_{k}, a, tt, ff}. For each i, 1 ≤ i ≤ n, let

α_{i} be a parallel composition Q_{i_{1}}||Q_{i_{2}}|| ⋯ ||Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where x_{i} occurs positively,

\overline{α_{i}} be a parallel composition Q_{i_{1}}||Q_{i_{2}}|| ⋯ ||Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where x_{i} occurs negatively, β_{i} be a parallel composition Q_{i_{1}}||Q_{i_{2}}|| ⋯ ||Q_{i_{ℓ}} such that

1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where y_{i} occurs positively, and

\overline{β_{i}} be a parallel composition Q_{i_{1}}||Q_{i_{2}}|| ⋯ ||Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where y_{i} occurs negatively.

Example 3. Let us consider a quantified boolean formula

∃x_{1}∀y_{1}∃x_{2}∀y_{2}. (x_{1} ∨ ¬y_{1} ∨ y_{2}) ∧ (¬x_{1} ∨ y_{1} ∨ y_{2}) ∧ (x_{1} ∨ y_{1} ∨ y_{2} ∨ ¬y_{2})

where n = 2, k = 3, C_{1} = x_{1} ∨ ¬y_{1} ∨ y_{2}, C_{2} = ¬x_{1} ∨ y_{1} ∨ y_{2} and C_{3} = x_{1} ∨ y_{1} ∨ y_{2} ∨ ¬y_{2}. Then

\begin{matrix}α_{1} = Q_{1}||Q_{3} & \overline{α_{1}} = Q_{2} & β_{1} = Q_{2}||Q_{3} & \overline{β_{1}} = Q_{1} \\ α_{2} = ϵ & \overline{α_{2}} = ϵ & β_{2} = Q_{1}||Q_{2}||Q_{3} & \overline{β_{2}} = Q_{3}. \end{matrix}

The set Δ is given by the following rewrite rules:

– for all j such that 1 ≤ j ≤ k:

Q_{j} ⟶^{q_{j}} Q_{j}

– for all i such that 1 ≤ i ≤ n:

             X_{i} ⟶^{a} Y_{i}^{choice}

X_{i} ⟶^{a} Y_{i}^{tt}  X′_{i} ⟶^{a} Y_{i}^{tt}
X_{i} ⟶^{a} Y_{i}^{ff}  X′_{i} ⟶^{a} Y_{i}^{ff}
Y_{i}^{choice} ⟶^{tt} Z_{i}||α_{i}  Y_{i}^{tt} ⟶^{tt} Z′_{i}||α_{i}
Y_{i}^{choice} ⟶^{ff} Z_{i}||\overline{α_{i}}  Y_{i}^{ff} ⟶^{ff} Z′_{i}||\overline{α_{i}}
Y_{i}^{tt} ⟶^{ff} Z_{i}||\overline{α_{i}}  Y_{i}^{ff} ⟶^{tt} Z_{i}||α_{i}
Z_{i} ⟶^{tt} X_{i+1}||β_{i}  Z′_{i} ⟶^{tt} X′_{i+1}||β_{i}
Z_{i} ⟶^{ff} X_{i+1}||\overline{β_{i}}  Z′_{i} ⟶^{ff} X′_{i+1}||\overline{β_{i}}

– and

X_{n+1} ⟶^{a} Q_{1}||Q_{2}|| … ||Q_{k−1}||Q_{k} X′_{n+1} ⟶^{a} ϵ.

We can see the processes (X_{1}, Δ) and (X′_{1}, Δ) in Figure 5 (if we set i = 1 and γ_{1} = ϵ). The intuition behind the construction will be explained in terms of bisimulation games and follows the main idea from Subsection 3.1. Consider a bisimulation game starting from the pair of processes X_{1} and X′_{1}.

The attacker is forced to make the first move by playing X_{1} ⟶^{a} Y_{1}^{choice} because in all other possible moves, either from X_{1} or X′_{1}, the defender can make the resulting processes syntactically equal and hence bisimilar. The defender’s answer to the move X_{1} ⟶^{a} Y_{1}^{choice} is either (i) X′_{1} ⟶^{a} Y_{1}^{tt} (this corresponds to setting the variable x_{1} to true) or (ii) X′_{1} ⟶^{a} Y_{1}^{ff} (this corresponds to setting the variable x_{1} to false).

In the next round the attacker is forced to take the action (i) tt or (ii) ff, according to the defender’s choice in the first round. Otherwise the attacker loses. The defender can only imitate the same action in the other process. The resulting processes after two rounds are (i) Z_{1}||α_{1} and Z′_{1}||α_{1} or (ii) Z_{1}||\overline{α_{1}} and Z′_{1}||\overline{α_{1}}. Note that it was the defender who had the possibility to decide between adding α_{1} (i.e. setting x_{1} to true) or \overline{α_{1}} (i.e. setting x_{1} to false).

In the third round the attacker has the choice of playing either along the action tt or ff, which corresponds to the universal quantifier in front of y_{1}. It does not matter in which process the attacker performs the move. The defender has only one possibility how to answer to this move — he must imitate the corresponding move in the other process. The resulting processes are X_{2}||γ_{2} and X′_{2}||γ_{2} such that γ_{2} = α̃_{1}||β̃_{1} where α̃_{1} ∈ \{α_{1}, \overline{α_{1}}\} and β̃_{1} ∈ \{β_{1}, \overline{β_{1}}\} according to the truth values chosen for x_{1} (by the defender) and for y_{1} (by the attacker). Now the game continues in similar fashion from X_{2}||γ_{2} and X′_{2}||γ_{2}. Playing some of the actions q_{1}, …, q_{k} cannot make the attacker win since the defender has always the possibility to imitate the same move in the other processes.

Hence if the attacker wants to win he has to reach eventually the states

X_{n+1}||γ_{n+1} and X′_{n+1}||γ_{n+1}, and then he performs the move X_{n+1}||γ_{n+1} ⟶^{a}

Q_{1}||Q_{2}|| … ||Q_{k−1}||Q_{k}||γ_{n+1} to which the defender has only one answer,

namely X′_{n+1}||γ_{n+1} ⟶^{a} γ_{n+1}. From the states Q_{1}||Q_{2}|| … ||Q_{k−1}||Q_{k}||γ_{n+1}

and γ_{n+1} the attacker has the possibility to check whether every clause C_{j}, 1 ≤ j ≤ k, in C is indeed satisfied under the generated truth assignment by using the rule Q_{j} ⟶^{q_{j}} Q_{j} in the first process. If the clause C_{j} is not satisfied then Q_{j} does not appear in γ_{n+1} and the defender loses. If all the clauses in C are satisfied then Q_{1}||Q_{2}|| … ||Q_{k−1}||Q_{k}||γ_{n+1} ∼ γ_{n+1} and the defender wins.

In what follows we formally prove that C is true iff (X_{1}, Δ) ∼ (X′_{1}, Δ).

[figure: X_{i}||γ_{i}; a; a; a; Y_{i}^{choice}||γ_{i}; tt; ff; Y_{i}^{tt}||γ_{i}; Y_{i}^{ff}||γ_{i}; Z_{i}||γ_{i}||α_{i}; tt; ff; Z_{i}||γ_{i}||\overline{α_{i}}; tt; ff; X_{i+1}||γ_{i}||α_{i}||β_{i}; X_{i+1}||γ_{i}||α_{i}||\overline{β_{i}}; X_{i+1}||γ_{i}||\overline{α_{i}}||β_{i}; X_{i+1}||γ_{i}||\overline{α_{i}}||\overline{β_{i}}]

[figure: X′_{i}||γ_{i}; a; a; Y_{i}^{tt}||γ_{i}; tt; ff; Y_{i}^{ff}||γ_{i}; ff; tt; Z′_{i}||γ_{i}||α_{i}; tt; ff; Z_{i}||γ_{i}||\overline{α_{i}}; Z′_{i}||γ_{i}||\overline{α_{i}}; tt; ff; Z_{i}||γ_{i}||α_{i}; X′_{i+1}||γ_{i}||α_{i}||β_{i}; X′_{i+1}||γ_{i}||α_{i}||\overline{β_{i}}; X′_{i+1}||γ_{i}||\overline{α_{i}}||β_{i}; X′_{i+1}||γ_{i}||\overline{α_{i}}||\overline{β_{i}}]

Fig. 5. Processes (X_{i}||γ_{i}, Δ) and (X′_{i}||γ_{i}, Δ)

Lemma 1. If (X_{1}, Δ) ∼ (X′_{1}, Δ) then the formula C is true.

Proof. We show that (X_{1}, Δ) ≁ (X′_{1}, Δ) under the assumption that C is false. If C is false then C′ defined by

C′ =^{def} ∀x_{1}∃y_{1}∀x_{2}∃y_{2} … ∀x_{n}∃y_{n}. ¬(C_{1} ∧ C_{2} ∧ … ∧ C_{k})

is true and we claim that the attacker has a winning strategy in the bisimulation game starting from (X_{1}, Δ) and (X′_{1}, Δ). The attacker’s strategy starts with performing a sequence of actions

a, x̃_{1}, ỹ_{1}, …, a, x̃_{i}, ỹ_{i}, …, a, x̃_{n}, ỹ_{n}, a

where x̃_{i}, ỹ_{i} ∈ {tt, ff} for all i, 1 ≤ i ≤ n. The attacker is playing only in the first process (X_{1}, Δ). The choice of x̃_{i} is done by the defender and of ỹ_{i} by the attacker — see the discussion above. This means that whatever values for x̃_{1}, …, x̃_{n} are chosen by the defender, the attacker can still decide on values for ỹ_{1}, …, ỹ_{n} such that the generated assignment satisfies the formula ¬(C_{1} ∧C_{2} ∧…∧C_{k}). Hence there must be some j, 1 ≤ j ≤ k, such that the clause C_{j} is not satisfied. This implies that Q_{j} does not occur in the second process. However, the attacker can perform the action q_{j} in the first process by using the rule Q_{j} ⟶^{q_{j}} Q_{j}. Thus the attacker has a winning strategy in the bisimulation game and (X_{1}, Δ) ≁ (X′_{1}, Δ). ⊓ ⊔

Lemma 2. If the formula C is true then (X_{1}, Δ) ∼ (X′_{1}, Δ).

Proof. Let us define sets AS_{i}, corresponding to the assignments of variables from x_{1}, y_{1} to x_{i}, y_{i}, 1 ≤ i ≤ n, such that the formula

∃x_{i+1}∀y_{i+1} … ∃x_{n}∀y_{n}. C_{1} ∧ C_{2} ∧ … ∧ C_{k}

is still true. The set AS_{i} for i ∈ {1, …, n} is defined by

AS_{i} =^{def} { α̃_{1}||β̃_{1}||α̃_{2}||β̃_{2}|| … ||α̃_{i}||β̃_{i} |

such that for all j, 1 ≤ j ≤ i, it holds that α̃_{j} ∈ \{α_{j}, \overline{α_{j}}\} and β̃_{j} ∈ \{β_{j}, \overline{β_{j}}\}, and under the assignment

x_{j} = \begin{cases}tt & if α̃_{j} = α_{j} \\ ff & if α̃_{j} = \overline{α_{j}} \end{cases} and y_{j} = \begin{cases}tt & if β̃_{j} = β_{j} \\ ff & if β̃_{j} = \overline{β_{j}} \end{cases}

the formula ∃x_{i+1}∀y_{i+1} … ∃x_{n}∀y_{n}. C_{1} ∧ C_{2} ∧ … ∧ C_{k} is true }.

By definition AS_{0} =^{def} {ϵ}. In particular, AS_{n} contains all the assignments for which the unquantified formula C_{1}∧C_{2}∧…∧C_{k} is true. The following relation is a strong bisimulation.

{(X_{i}||γ_{i}, X′_{i}||γ_{i}) | 1 ≤ i ≤ n ∧ γ_{i} ∈ AS_{i−1}} ∪ \{(Y_{i}^{choice}||γ_{i}, Y_{i}^{tt}||γ_{i}) | 1 ≤ i ≤ n ∧ γ_{i}||α_{i}||β_{i} ∈ AS_{i} ∧ γ_{i}||α_{i}||\overline{β_{i}} ∈ AS_{i}\} ∪ \{(Y_{i}^{choice}||γ_{i}, Y_{i}^{ff}||γ_{i}) | 1 ≤ i ≤ n ∧ γ_{i}||\overline{α_{i}}||β_{i} ∈ AS_{i} ∧ γ_{i}||\overline{α_{i}}||\overline{β_{i}} ∈ AS_{i}\} ∪ \{(Z_{i}||γ_{i}||α_{i}, Z′_{i}||γ_{i}||α_{i}) | 1 ≤ i ≤ n ∧ γ_{i}||α_{i}||β_{i} ∈ AS_{i} ∧ γ_{i}||α_{i}||\overline{β_{i}} ∈ AS_{i}\} ∪ \{(Z_{i}||γ_{i}||\overline{α_{i}}, Z′_{i}||γ_{i}||\overline{α_{i}}) | 1 ≤ i ≤ n ∧ γ_{i}||\overline{α_{i}}||β_{i} ∈ AS_{i} ∧ γ_{i}||\overline{α_{i}}||\overline{β_{i}} ∈ AS_{i}\} ∪ {(X_{n+1}||γ_{n+1}, X′_{n+1}||γ_{n+1}) | γ_{n+1} ∈ AS_{n}} ∪ {(Q_{1}||Q_{2}|| … ||Q_{k−1}||Q_{k}||γ_{n+1}, γ_{n+1}) | γ_{n+1} ∈ AS_{n}} ∪ {(E, E) | E ∈ P(Const(Δ))}

Since AS_{0} = {ϵ}, we get that the pair (X_{1}, X′_{1}) is an element of this relation. Hence we proved that (X_{1}, Δ) ∼ (X′_{1}, Δ). ⊓ ⊔

Theorem 1. Strong bisimilarity of BPP is PSPACE-hard.

Proof. By Lemma 1 and Lemma 2. ⊓ ⊔

Remark 5. Notice that there are only finitely many reachable states from both (X_{1}, Δ) and (X′_{1}, Δ). Hence (X_{1}, Δ) and (X′_{1}, Δ) are strongly regular processes.

Remark 6. Theorem 1 can be easily extended to 1-safe Petri nets where each transition has exactly one input place (for related results about 1safe Petri nets see e.g. [17]). It is enough to introduce for each α_{i}, \overline{α_{i}}, β_{i} and \overline{β_{i}}, 1 ≤ i ≤ n, a new set of process constants \{Q_{1}, …, Q_{k}\} to ensure that in each reachable marking there is at most one token in every place.

3.3 Strong Bisimilarity of BPA

In this subsection we show that strong bisimilarity of BPA is a PSPACEhard problem. The proof is again by reduction from QSAT, using the main idea from Subsection 3.1. However, there is a substantial difference from the proof for BPP explained in the previous subsection. In case of BPP it is easier to check which clauses of a given boolean formula are satisfied because we have a parallel access to all process constants contained in the current state. This technique has to be modified to work for BPA since we have only a sequential access to the process constants contained in the current state, and there is no possibility of remembering any information in e.g. a finite-state control unit as in pushdown systems. Hence we have to encode the information about satisfied clauses in a unary way to achieve our result.

Let

C ≡ ∃x_{1}∀y_{1}∃x_{2}∀y_{2} … ∃x_{n}∀y_{n}. C_{1} ∧ C_{2} ∧ … ∧ C_{k}

be an instance of QSAT. Assume that Q_{1}, …, Q_{k} are process constants. For each i, 1 ≤ i ≤ n, let

α_{i} be a sequential composition Q_{i_{1}}.Q_{i_{2}}. · · · .Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where x_{i} occurs positively,

\overline{α_{i}} be a sequential composition Q_{i_{1}}.Q_{i_{2}}. · · · .Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where x_{i} occurs negatively,

β_{i} be a sequential composition Q_{i_{1}}.Q_{i_{2}}. · · · .Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where y_{i} occurs positively, and

\overline{β_{i}} be a sequential composition Q_{i_{1}}.Q_{i_{2}}. · · · .Q_{i_{ℓ}} such that 1 ≤ i_{1} < i_{2} < ⋯ < i_{ℓ} ≤ k and C_{i_{1}}, C_{i_{2}}, …, C_{i_{ℓ}} are all the clauses where y_{i} occurs negatively.

Example 4. Let us consider a quantified formula

∃x_{1}∀y_{1}∃x_{2}∀y_{2}. (x_{1} ∨ ¬y_{1} ∨ y_{2}) ∧ (¬x_{1} ∨ y_{1} ∨ y_{2}) ∧ (x_{1} ∨ y_{1} ∨ y_{2} ∨ ¬y_{2})

where n = 2, k = 3, C_{1} = x_{1} ∨ ¬y_{1} ∨ y_{2}, C_{2} = ¬x_{1} ∨ y_{1} ∨ y_{2} and C_{3} = x_{1} ∨ y_{1} ∨ y_{2} ∨ ¬y_{2}. Then

\begin{matrix}α_{1} = Q_{1}.Q_{3} & \overline{α_{1}} = Q_{2} & β_{1} = Q_{2}.Q_{3} & \overline{β_{1}} = Q_{1} \\ α_{2} = ϵ & \overline{α_{2}} = ϵ & β_{2} = Q_{1}.Q_{2}.Q_{3} & \overline{β_{2}} = Q_{3}. \end{matrix}

Let SF(γ) be the set of all suffixes of a sequential composition γ ∈

S({Q_{1}, …, Q_{k}}), i.e., SF(γ) =^{def} {γ′ | ∃γ′′ such that γ′′.γ′ = γ}. Let M be

the least natural number such that M ≥ 2n + 1 and M = 2^{K} for some natural number K > 0. Of course, M > 1.

We define BPA processes (X_{1}.S, Δ) and (X′_{1}.S, Δ), where Const(Δ) =^{def}

{A_{0}, A_{1}, A_{2}, …, A_{kK−1}} ∪ {Q_{1}, …, Q_{k}} ∪ \{V_{i}^{γ}, V_{i}^{γ,choice}, V_{i}^{′γ}, V_{i}^{γ,yes}, V_{i}^{γ,no} | 1 ≤ i ≤ n ∧ γ ∈ SF(α_{i}) ∪ SF(\overline{α_{i}})\} ∪ \{W_{i}^{γ}, W_{i}^{γ,choice}, W_{i}^{′γ}, W_{i}^{γ,yes}, W_{i}^{γ,no} | 1 ≤ i ≤ n ∧ γ ∈ SF(β_{i}) ∪ SF(\overline{β_{i}})\} ∪ {X_{i}, Y_{i}^{choice}, Z_{i}, X′_{i}, Y_{i}^{tt}, Y_{i}^{ff}, Z′_{i} | 1 ≤ i ≤ n} ∪ {X_{n+1}, X′_{n+1}, S} and Act(Δ) =^{def} {a, c, tt, ff, yes, no, s}. The first part of the rewrite system Δ consists of the rewrite rules:

A_{0} ⟶^{c} ϵ

A_{ℓ} ⟶^{c} A_{ℓ−1}.A_{ℓ−2}. · · · .A_{1}.A_{0}  for all ℓ, 1 ≤ ℓ ≤ kK − 1
Q_{j} ⟶^{c} A_{jK−1}.A_{jK−2}. · · · .A_{1}.A_{0} for all j, 1 ≤ j ≤ k.

Remark 7. Notice that the size of the previously introduced rewrite rules

is polynomial w.r.t. the size of the formula C. Moreover A_{ℓ} ⟶^{c^{2^{ℓ}}} ϵ for all ℓ, 0 ≤ ℓ ≤ kK − 1, which implies by using the equation 2^{jK} = M^{j}

that Q_{j} ⟶^{c^{M^{j}}} ϵ for all j, 1 ≤ j ≤ k. Hence Q_{j} can perform exactly M^{j} transitions labelled by the “counting” action c and then disappears.

The intuition is that each clause C_{j}, 1 ≤ j ≤ k, is coded by the process constant Q_{j}, which enables to perform exactly M^{j} of c actions. The key idea of our proof is then that the defender and the attacker will choose truth values for the variables x_{1}, …, x_{n} and y_{1}, …, y_{n}, respectively. During this process some of the clauses C_{1}, …, C_{k} become satisfied, and the defender will have the possibility to add the corresponding process constants Q_{1}, …, Q_{k} to the current state.

Moreover, the defender will be able to select which of the process constants (corresponding to the satisfied clauses) appear in the current state in such a way that each of them appears there exactly once.

The following lemma shall be essential for proving our reduction correct.

Lemma 3. Assume that M and k are constants introduced above, i.e., M > 1 and k > 0. Let a_{j}, 1 ≤ j ≤ k, be natural numbers such that 0 ≤ a_{j} ≤ M − 1 for all j. The following two statements are equivalent:

(i) ∑_{j=1}^{k} a_{j}M^{j} = ∑_{j=1}^{k} M^{j} (ii) a_{j} = 1 for all j, 1 ≤ j ≤ k.

Proof. By uniqueness of M-ary representations. Obviously (ii) implies (i). By induction on k we prove the other direction. If k = 1 then a_{1}M = M

immediately gives that a_{1} = 1. Let ∑_{j=1}^{k+1} a_{j}M^{j} = ∑_{j=1}^{k+1} M^{j}. Since a_{j} ≤ M − 1

for all j, 1 ≤ j ≤ k + 1, we get that

∑_{j=1}^{k} a_{j}M^{j} ≤ ∑_{j=1}^{k}(M − 1)M^{j} = (M − 1)M · ∑_{j=0}^{k−1} M^{j} =

(M − 1)M · \frac{M^{k} − 1}{M − 1} = M^{k+1} − M < M^{k+1}.

Let us now consider the equation

∑_{j=1}^{k} a_{j}M^{j} + a_{k+1}M^{k+1} = ∑_{j=1}^{k} M^{j} + M^{k+1}.

The fact that ∑_{j=1}^{k} a_{j}M^{j} < M^{k+1} gives that a_{k+1} ≥ 1. On the other hand

∑_{j=1}^{k} M^{j} = M · ∑_{j=0}^{k−1} M^{j} = M · \frac{M^{k}−1}{M−1} < M^{k+1}, which implies that a_{k+1} ≤ 1.

Hence a_{k+1} = 1 and the following equation must be satisfied

∑_{j=1}^{k} a_{j}M^{j} = ∑_{j=1}^{k} M^{j}.

By induction hypothesis a_{j} = 1 also for all j, 1 ≤ j ≤ k. ⊓ ⊔

We continue with the definition of the set of rewrite rules Δ. For all i, 1 ≤ i ≤ n, and Q.γ ∈ SF(α_{i}) ∪ SF(\overline{α_{i}}) where Q ∈ \{Q_{1}, …, Q_{k}\} and γ ∈ S({Q_{1}, …, Q_{k}}), Δ contains the rules:

V_{i}^{Q.γ} ⟶^{a} V_{i}^{Q.γ,choice}

V_{i}^{Q.γ} ⟶^{a} V_{i}^{Q.γ,yes}  V_{i}^{′Q.γ} ⟶^{a} V_{i}^{Q.γ,yes}
V_{i}^{Q.γ} ⟶^{a} V_{i}^{Q.γ,no}  V_{i}^{′Q.γ} ⟶^{a} V_{i}^{Q.γ,no}
V_{i}^{Q.γ,choice} ⟶^{yes} V_{i}^{γ}.Q V_{i}^{Q.γ,yes} ⟶^{yes} V_{i}^{′γ}.Q
V_{i}^{Q.γ,choice} ⟶^{no} V_{i}^{γ}  V_{i}^{Q.γ,no} ⟶^{no} V_{i}^{′γ}
V_{i}^{Q.γ,yes} ⟶^{no} V_{i}^{γ}  V_{i}^{Q.γ,no} ⟶^{yes} V_{i}^{γ}.Q.

Similarly, for all i, 1 ≤ i ≤ n, and Q.γ ∈ SF(β_{i}) ∪ SF(\overline{β_{i}}) where Q ∈ {Q_{1}, …, Q_{k}} and γ ∈ S({Q_{1}, …, Q_{k}}), Δ contains the rules:

W_{i}^{Q.γ} ⟶^{a} W_{i}^{Q.γ,choice}

W_{i}^{Q.γ} ⟶^{a} W_{i}^{Q.γ,yes}  W_{i}^{′Q.γ} ⟶^{a} W_{i}^{Q.γ,yes}
W_{i}^{Q.γ} ⟶^{a} W_{i}^{Q.γ,no}  W_{i}^{′Q.γ} ⟶^{a} W_{i}^{Q.γ,no}
W_{i}^{Q.γ,choice} ⟶^{yes} W_{i}^{γ}.Q W_{i}^{Q.γ,yes} ⟶^{yes} W_{i}^{′γ}.Q
W_{i}^{Q.γ,choice} ⟶^{no} W_{i}^{γ}  W_{i}^{Q.γ,no} ⟶^{no} W_{i}^{′γ}
W_{i}^{Q.γ,yes} ⟶^{no} W_{i}^{γ}  W_{i}^{Q.γ,no} ⟶^{yes} W_{i}^{γ}.Q.

Assume now a bisimulation game starting from (V_{i}^{α_{i}}, Δ) and (V_{i}^{′α_{i}}, Δ). As shown in Subsection 3.1, either in some round the states become syntactically equal, or the defender has the possibility to choose in the first round the next states (i) V_{i}^{α_{i},choice} and V_{i}^{α_{i},yes} or (ii) V_{i}^{α_{i},choice} and V_{i}^{α_{i},no}. This means that in the next round a process constant Q such that α_{i} = Q.α′_{i} for some α′_{i} is either (i) added to the current state or (ii) left out. Now the game continues either from (i) V_{i}^{α′_{i}}.Q and V_{i}^{′α′_{i}}.Q or from (ii) V_{i}^{α′_{i}} and V_{i}^{′α′_{i}}. This repeats in similar fashion until the states V_{i}^{ϵ}.γ_{i} and V_{i}^{′ϵ}.γ_{i} are reached, such that γ_{i} is some subsequence of α_{i} (in a reverse order) and it was the defender who had the possibility to decide which of the process constants contained in α_{i} appear also in γ_{i}.

The same happens if we start playing the bisimulation game from the

pairs (V \overline{α_{i}} ; i, Δ) and (V_{i}^{′\overline{α_{i}}}, Δ), or (W_{i}^{β_{i}}, Δ) and (W_{i}^{′β_{i}}, Δ), or (W \overline{β_{i}} ; i, Δ) and

(W_{i}^{′\overline{β_{i}}}, Δ).

We finish the definition of Δ by adding the rules:

– for all i, 1 ≤ i ≤ n:

                  X_{i} ⟶^{a} Y_{i}^{choice}

X_{i} ⟶^{a} Y_{i}^{tt}  X′_{i} ⟶^{a} Y_{i}^{tt}
X_{i} ⟶^{a} Y_{i}^{ff}  X′_{i} ⟶^{a} Y_{i}^{ff}
Y_{i}^{choice} ⟶^{tt} V_{i}^{α_{i}} Y_{i}^{tt} ⟶^{tt} V_{i}^{′α_{i}}
Y_{i}^{choice} ⟶^{ff} V \overline{α_{i}} ; i Y_{i}^{ff} ⟶^{ff} V_{i}^{′\overline{α_{i}}}
Y_{i}^{tt} ⟶^{ff} V \overline{α_{i}} ; i  Y_{i}^{ff} ⟶^{tt} V_{i}^{α_{i}}
V_{i}^{ϵ} ⟶^{a} Z_{i}  V_{i}^{′ϵ} ⟶^{a} Z′_{i}
Z_{i} ⟶^{tt} W_{i}^{β_{i}}  Z′_{i} ⟶^{tt} W_{i}^{′β_{i}}
Z_{i} ⟶^{ff} W \overline{β_{i}} ; i  Z′_{i} ⟶^{ff} W_{i}^{′\overline{β_{i}}}
W_{i}^{ϵ} ⟶^{a} X_{i+1}  W_{i}^{′ϵ} ⟶^{a} X′_{i+1}

– and X_{n+1} ⟶^{a} Q_{1}.Q_{2}. . . . .Q_{k−1}.Q_{k}.S X′_{n+1} ⟶^{a} ϵ S ⟶^{s} S.

Lemma 4. If (X_{1}.S, Δ) ∼ (X′_{1}.S, Δ) then the formula C is true.

Proof. We show that (X_{1}.S, Δ) ≁ (X′_{1}.S, Δ) under the assumption that C is false. If C is false then C′ defined by

C′ =^{def} ∀x_{1}∃y_{1}∀x_{2}∃y_{2} … ∀x_{n}∃y_{n}. ¬(C_{1} ∧ C_{2} ∧ … ∧ C_{k})

is true and we claim that the attacker has a winning strategy in the bisimulation game starting from (X_{1}.S, Δ) and (X′_{1}.S, Δ). As mentioned in Subsection 3.1, in the first round the attacker is forced to perform the move X_{1}.S ⟶^{a} Y_{1}^{choice}.S. The defender can respond either by (i) X′_{1}.S ⟶^{a} Y_{1}^{tt}.S (which corresponds to setting the variable x_{1} to true) or by (ii) X′_{1}.S ⟶^{a} Y_{1}^{ff}.S (which corresponds to setting the variable x_{1} to false). In the second round the attacker performs the action (i) tt or (ii) ff, and the defender must answer by the same action in the other process. Now the game continues from (i) V_{1}^{α_{1}}.S and V_{1}^{′α_{1}}.S or (ii) V \overline{α_{1}} ; 1.S and V_{1}^{′\overline{α_{1}}}.S. Within the next (i) 2 · |α_{1}| or (ii) 2 · |\overline{α_{1}}| rounds (where |w| is the length of w) the defender has the possibility to choose some subsequence of (i) α_{1} or (ii) \overline{α_{1}} and add it in a reverse order to the current state. Then the game continues either from (i) V_{1}^{ϵ}.γ_{1}.S and V_{1}^{′ϵ}.γ_{1}.S or (ii) V_{1}^{ϵ}.\overline{γ_{1}}.S and V_{1}^{′ϵ}.\overline{γ_{1}}.S, such that (i) γ_{1} is a subsequence (in a reverse order and chosen by the defender) of α_{1} or (ii) \overline{γ_{1}} is a subsequence (in a reverse order and chosen by the defender) of \overline{α_{1}}. The players have only one possible continuation of the game by using the rewrite rules V_{1}^{ϵ} ⟶^{a} Z_{1} and V_{1}^{′ϵ} ⟶^{a} Z′_{1}, thus reaching the states (i) Z_{1}.γ_{1}.S and Z′_{1}.γ_{1}.S or (ii) Z_{1}.\overline{γ_{1}}.S and Z′_{1}.\overline{γ_{1}}.S.

Now, it is the attacker who has the possibility of making a choice between the rewrite rules Z_{1} ⟶^{tt} W_{1}^{β_{1}} or Z_{1} ⟶^{ff} W \overline{β_{1}} ; 1 in the first process. This corresponds to setting the variable y_{1} to true or false. The defender can only imitate the same action by using the rules Z′_{1} ⟶^{tt} W_{1}^{′β_{1}} or Z′_{1} ⟶^{ff} W_{1}^{′\overline{β_{1}}} in the other process. From the current states starting with W_{1}^{β_{1}} and W_{1}^{′β_{1}}, or W \overline{β_{1}} ; 1 and W_{1}^{′\overline{β_{1}}}, the same happens as before: the defender has the possibility of choosing a subsequence δ_{1} (in a reverse order) of β_{1} or a subsequence \overline{δ_{1}} (in a reverse order) of \overline{β_{1}}. So precisely after 2 · |β_{1}| or 2 · |\overline{β_{1}}| rounds the following four possible pairs of states can be reached: (1) W_{1}^{ϵ}.δ_{1}.γ_{1}.S and W_{1}^{′ϵ}.δ_{1}.γ_{1}.S, or (2) W_{1}^{ϵ}.δ_{1}.\overline{γ_{1}}.S and W_{1}^{′ϵ}.δ_{1}.\overline{γ_{1}}.S, or (3) W_{1}^{ϵ}.\overline{δ_{1}}.γ_{1}.S and W_{1}^{′ϵ}.\overline{δ_{1}}.γ_{1}.S, or (4) W_{1}^{ϵ}.\overline{δ_{1}}.\overline{γ_{1}}.S and W_{1}^{′ϵ}.\overline{δ_{1}}.\overline{γ_{1}}.S. We have now only one possible continuation of the game in the next round, reaching the states (1) X_{2}.δ_{1}.γ_{1}.S and X′_{2}.δ_{1}.γ_{1}.S, or (2) X_{2}.δ_{1}.\overline{γ_{1}}.S and X′_{2}.δ_{1}.\overline{γ_{1}}.S, or (3) X_{2}.\overline{δ_{1}}.γ_{1}.S and X′_{2}.\overline{δ_{1}}.γ_{1}.S, or (4) X_{2}.\overline{δ_{1}}.\overline{γ_{1}}.S and X′_{2}.\overline{δ_{1}}.\overline{γ_{1}}.S.

We remind the reader of the fact that the defender had the possibility to set the variable x_{1} to true or false, and the attacker decided on the truth value for the variable y_{1}. In the meantime, all the process constants from {Q_{1}, …, Q_{k}} corresponding to the clauses that became satisfied by this assignment could have been potentially added to the current state, but it was the defender who had the possibility to filter some of them out.

In the next rounds the same schema of the game repeats, until we reach the states X_{n+1}.ω.S and X′_{n+1}.ω.S. The defender decides on the truth values for each of the variables x_{2}, …, x_{n}, and the attacker has the possibility to respond by choosing the truth values for the variables y_{2}, …, y_{n}. During this some of the clauses appear to be satisfied and ω consists of a selection (made by the defender) of process constants corresponding to these clauses.

Since we assume that the formula C′ is true, the attacker can decide on the truth values for y_{1}, …, y_{n} in such a way that at least one of the clauses C_{1}, …, C_{k} is not satisfied. Let us suppose that it is C_{m} for some m, 1 ≤ m ≤ k, that is not satisfied. Hence Q_{m} cannot appear in ω and the attacker has the following winning strategy. He plays

X_{n+1}.ω.S ⟶^{a} Q_{1}.Q_{2}. . . . .Q_{k−1}.Q_{k}.S.ω.S, to which the defender can only

answer by X′_{n+1}.ω.S ⟶^{a} ω.S.

The state Q_{1}.Q_{2}. . . . .Q_{k−1}.Q_{k}.S.ω.S can perform exactly ∑_{j=1}^{k} M^{j} of actions c (see Remark 7) followed by an infinite sequence of actions s. On the other hand, ω.S can never perform exactly ∑_{j=1}^{k} M^{j} of actions c and then the infinite sequence of actions s. This follows from the fact that Q_{m} does not appear in ω and from Lemma 3 — obviously, any process constant from {Q_{1}, …, Q_{k}} can occur at most 2n times in ω (2n ≤ M −1), which justifies the assumption of Lemma 3.

Hence the attacker has a winning strategy and (X_{1}.S, Δ) ≁ (X′_{1}.S, Δ).

⊓ ⊔

Lemma 5. If the formula C is true then (X_{1}.S, Δ) ∼ (X′_{1}.S, Δ).

Proof. Assume a bisimulation game starting from the pair (X_{1}.S, Δ) and (X′_{1}.S, Δ). We show that the defender has a winning strategy. As mentioned in Subsection 3.1 and in the proof above, the attacker is forced to play according to a strictly defined strategy, otherwise the defender can make the resulting processes immediately syntactically equal and hence bisimilar. As shown before the defender can make the choices between setting the variables x_{1}, …, x_{n} to true or false, whereas the attacker can decide on truth values for y_{1}, …, y_{n}. Thus the defender can play the bisimulation game such that finally every clause C_{1}, …, C_{k} in C is satisfied. The defender has the possibility to add the corresponding process constants Q_{1}, …, Q_{k} to the current state in such a way that when reaching the states X_{n+1}.ω.S and X′_{n+1}.ω.S, the sequential composition ω contains every Q_{j} exactly once for each j, 1 ≤ j ≤ k. This can be easily achieved by following the strategy: “add Q_{j} to the current state if and only if it is not already present there”. After performing the

moves X_{n+1}.ω.S ⟶^{a} Q_{1}.Q_{2}. . . . .Q_{k−1}.Q_{k}.S.ω.S and X′_{n+1}.ω.S ⟶^{a} ω.S,

the defender wins since S.ω.S ∼ S and both Q_{1}.Q_{2}. . . . .Q_{k−1}.Q_{k} and ω can perform the same number of actions c and then become ϵ. Hence (X_{1}.S, Δ) ∼ (X′_{1}.S, Δ). ⊓ ⊔

Theorem 2. Strong bisimilarity of BPA is PSPACE-hard.

Proof. By Lemma 4 and Lemma 5. ⊓ ⊔

Remark 8. Notice that there are only finitely many reachable states from both (X_{1}.S, Δ) and (X′_{1}.S, Δ). Hence (X_{1}.S, Δ) and (X′_{1}.S, Δ) are strongly regular processes.

4 Lower Bounds for Strong Regularity

The idea to reduce bisimilarity to regularity first appeared in the literature due to Mayr [20]. He showed a technique for reducing weak bisimilarity of regular BPP to weak regularity of BPP. However, in his reduction τ actions are used. Building upon Mayr’s approach we provide a polynomial time reduction from strong bisimilarity of regular BPP (BPA) to strong regularity of BPP (BPA).

4.1 Strong Regularity of BPP

Theorem 3 (Reduction from bisimilarity to regularity). Let (P_{1}, Δ) and (P_{2}, Δ) be strongly regular BPP processes. We can construct in polynomial time a BPP process (P, Δ′) such that

(P_{1}, Δ) ∼ (P_{2}, Δ) if and only if (P, Δ′) is strongly regular.

Proof. Assume that (P_{1}, Δ) and (P_{2}, Δ) are strongly regular. We construct a BPP process (P, Δ′) with

Const(Δ′) =^{def} Const(Δ) ∪ {X, A, A_{c}, B_{c}, P′_{1}, P′_{2}}

and

Act(Δ′) =^{def} Act(Δ) ∪ {a, b}

where X, A, A_{c}, B_{c}, P′_{1}, P′_{2} are new process constants and a, b are new actions. We define Δ′ =^{def} Δ ∪ Δ^{1} ∪ Δ^{2} where the set of rewrite rules Δ^{1} is

[figure: X||A^{i}||B_{c}; a^{i′}; ∼^{?}; X||A^{j}||B_{c}; a^{i′}; P′_{1}||A^{i−i′+1}||A_{c}||B_{c}; a^{j−i′}; X||A^{j−i′}||B_{c}; a^{j−i′}; P′_{1}||A^{i′′}||A_{c}||B_{c}; a; X||B_{c}; a; P_{1}||A^{i′′}||A_{c}||B_{c}; ≁; P_{2}||A_{c}||B_{c}]

Fig. 6. Winning strategy for the attacker (i < j)

given by

\begin{matrix}X ⟶^{b} X||A & A ⟶^{a} ϵ & A_{c} ⟶^{a} A_{c} & B_{c} ⟶^{b} B_{c} \\ X ⟶^{a} P′_{1}||A_{c} & X ⟶^{a} P_{1}||A_{c} & P′_{1} ⟶^{a} P_{1} \end{matrix}

and Δ^{2} is given by

X ⟶^{a} P′_{2}||A_{c}  X ⟶^{a} P_{2}||A_{c}  P′_{2} ⟶^{a} P_{2}.

Let P =^{def} X||B_{c}.

Lemma 6. If (P_{1}, Δ) ≁ (P_{2}, Δ) then (P, Δ′) is not strongly regular.

Proof. Let (P_{1}, Δ) ≁ (P_{2}, Δ). For simplicity (and without loss of generality) we assume that P_{1} ≁ ϵ and P_{2} ≁ ϵ. We demonstrate that there are infinitely many strongly nonbisimilar states reachable from (P, Δ′).

Let us consider an infinite number of states of the form X||A^{i}||B_{c} for any natural number i. Of course P ⟶^{∗} X||A^{i}||B_{c} and we claim that (X||A^{i}||B_{c}, Δ′) ≁ (X||A^{j}||B_{c}, Δ′) for any i ≠ j. Without loss of generality assume that i < j. The attacker has the following winning strategy (playing only in the second process — see Figure 6).

He performs a sequence of j actions a from X||A^{j}||B_{c}, thus reaching a state X||B_{c}. The defender playing from X||A^{i}||B_{c} cannot do this sequence of a-actions without using some rule for X. This is because B_{c} −̸→^{a} and A^{i} can perform at most i a-actions (i < j). As we assume that P_{1} ≁ ϵ and P_{2} ≁ ϵ, process constants P_{1} and P_{2} cannot appear in the defender’s process during the first j rounds, otherwise he loses immediately. So the defender has to make a choice between the rules X ⟶^{a} P′_{1}||A_{c} and X ⟶^{a} P′_{2}||A_{c} sometime within the first j moves (let us say in round i′ where i′ ≤ i + 1). Assume that the defender chooses X ⟶^{a} P′_{1}||A_{c} — the other case is symmetric. Now, the defender must perform j − i′ of a-actions by using the rules A_{c} ⟶^{a} A_{c} or A ⟶^{a} ϵ.

After j rounds the resulting states are P′_{1}||A^{i′′}||A_{c}||B_{c} for i′′ ≤ i − i′ + 1, and X||B_{c}. The attacker wins by performing the move X||B_{c} ⟶^{a} P_{2}||A_{c}||B_{c}. Again, since we assume that P_{2} ≁ ϵ the defender has to answer

with P′_{1}||A^{i′′}||A_{c}||B_{c} ⟶^{a} P_{1}||A^{i′′}||A_{c}||B_{c}. The attacker has now a winning

strategy from P_{1}||A^{i′′}||A_{c}||B_{c} and P_{2}||A_{c}||B_{c}: the fact that P_{1} ≁ P_{2} and that the actions a and b are fresh ones implies that P_{1}||A^{i′′}||A_{c}||B_{c} ≁ P_{2}||A_{c}||B_{c}.

⊓ ⊔

Lemma 7. If (P_{1}, Δ) ∼ (P_{2}, Δ) then (P, Δ′) is strongly regular.

Proof. Assume that (P_{1}, Δ) ∼ (P_{2}, Δ) which implies that (P, Δ′) ∼ (P, Δ′′) where Δ′′ =^{def} Δ′ ∖ Δ^{2} (strong bisimilarity is a congruence w.r.t. the parallel operator). It is enough to show that (P, Δ′′) is strongly regular. Observe that (A^{i}||A_{c}, Δ′′) ∼ (A_{c}, Δ′′) for any i such that 0 ≤ i. Then also (P_{1}||A^{i}||A_{c}||B_{c}, Δ′′) ∼ (P_{1}||A_{c}||B_{c}, Δ′′) and (P′_{1}||A^{i}||A_{c}||B_{c}, Δ′′) ∼ (P′_{1}||A_{c}||B_{c}, Δ′′) for any i such that 0 ≤ i. This implies that

(X||A^{i}||B_{c}, Δ′′) ∼ (P′_{1}||A_{c}||B_{c}, Δ′′)  (1)

for any i such that 0 ≤ i. Since (P_{1}, Δ) is a strongly regular process then (P′_{1}||A_{c}||B_{c}, Δ′′) is also strongly regular. This by using (1) in particular gives that (X||A^{0}||B_{c}, Δ′′) = (X||B_{c}, Δ′′) = (P, Δ′′) is strongly regular.

⊓ ⊔

Theorem 3 follows from Lemma 6 and Lemma 7. ⊓ ⊔

Theorem 4. Strong regularity of BPP is PSPACE-hard.

Proof. By Theorem 1, Remark 5 and Theorem 3. ⊓ ⊔

4.2 Strong Regularity of BPA

Theorem 5 (Reduction from bisimilarity to regularity). Let (P_{1}, Δ) and (P_{2}, Δ) be strongly regular BPA processes. We can construct in polynomial time a BPA process (P, Δ′) such that

(P_{1}, Δ) ∼ (P_{2}, Δ) if and only if (P, Δ′) is strongly regular.

Proof. Assume that (P_{1}, Δ) and (P_{2}, Δ) are strongly regular BPA processes. We construct a BPA process (P, Δ′) with

Const(Δ′) =^{def} Const(Δ) ∪ {X, A, C, S, P′_{1}, P′_{2}}

and

Act(Δ′) =^{def} Act(Δ) ∪ {a, s}

where X, A, C, S, P′_{1}, P′_{2} are new process constants and a, s are new actions. We define Δ′ =^{def} Δ ∪ Δ^{1} ∪ Δ^{2} where the set of transition rules Δ^{1} is given by

X ⟶^{a} X.A  X ⟶^{a} ϵ  A ⟶^{a} ϵ  S ⟶^{s} S
A ⟶^{a} P′_{1}.S  A ⟶^{a} P_{1}.S P′_{1} ⟶^{a} P′_{1}  P′_{1} ⟶^{a} P_{1}
X ⟶^{a} P′_{1}.S  X ⟶^{a} P_{1}.S
C ⟶^{a} P′_{1}.S  C ⟶^{a} P_{1}.S

and Δ^{2} is given by

A ⟶^{a} P′_{2}.S  A ⟶^{a} P_{2}.S  P′_{2} ⟶^{a} P′_{2}  P′_{2} ⟶^{a} P_{2}
X ⟶^{a} P′_{2}.S  X ⟶^{a} P_{2}.S
C ⟶^{a} P′_{2}.S  C ⟶^{a} P_{2}.S.

Let P =^{def} X.C.

Lemma 8. If (P_{1}, Δ) ≁ (P_{2}, Δ) then (P, Δ′) is not strongly regular.

Proof. Let (P_{1}, Δ) ≁ (P_{2}, Δ). Without loss of generality assume that P_{1} ≁ ϵ and P_{2} ≁ ϵ. We show that there are infinitely many strongly nonbisimilar states reachable from (P, Δ′). Consider the states of the form A^{i}.C for any natural number i. Of course, P ⟶^{∗} A^{i}.C. In order to prove that (P, Δ′) is not strongly regular, it is enough to show that (A^{i}.C, Δ′) ≁ (A^{j}.C, Δ′) for any i < j. Next paragraph describes attacker’s winning strategy from the states A^{i}.C and A^{j}.C.

The attacker is playing only in the second process A^{j}.C. He performs a sequence of actions a of the length j by using the rule A ⟶^{a} ϵ and reaches the state C. By examining all possible moves of the defender from the process A^{i}.C, we get that a different rule from A ⟶^{a} ϵ must be used within the first j rounds since i < j. Using the assumption that P_{1} ≁ ϵ and P_{2} ≁ ϵ we derive that only four types of states (reachable by the defender from A^{i}.C after j rounds) must be considered. Namely – P′_{1}.S.A^{i′}.C for some i′, 0 ≤ i′ < i

– P′_{2}.S.A^{i′}.C for some i′, 0 ≤ i′ < i

– P′_{1}.S or

– P′_{2}.S.

Notice that S.α ∼ S for any process expression α, which in particular means that P′_{1}.S.A^{i′}.C ∼ P′_{1}.S and P′_{2}.S.A^{i′}.C ∼ P′_{2}.S. Hence it is enough to examine only the states P′_{1}.S and P′_{2}.S. Let us consider the bisimulation game continuing from the pair of states P′_{1}.S and C — the other case (from states P′_{2}.S and C) is symmetric. The attacker wins by performing the move C ⟶^{a} P_{2}.S. The defender has to answer by P′_{1}.S ⟶^{a} P_{1}.S since the move P′_{1}.S ⟶^{a} P′_{1}.S means an immediate loss for the defender (we assume that P_{1} ≁ ϵ and P_{2} ≁ ϵ). Now the resulting states after j + 1 rounds are P_{1}.S and P_{2}.S. The attacker has a winning strategy from this pair by our assumption that P_{1} ≁ P_{2} and by the fact that S ⟶^{s} S is the only rewrite rule for S and the action s is a fresh one. ⊓ ⊔

Lemma 9. If (P_{1}, Δ) ∼ (P_{2}, Δ) then (P, Δ′) is strongly regular.

Proof. Assume that (P_{1}, Δ) ∼ (P_{2}, Δ) which implies that (P, Δ′) ∼ (P, Δ′′) where Δ′′ =^{def} Δ′ ∖ Δ^{2} (strong bisimilarity is a congruence w.r.t. the sequential operator^{2}). It is enough to show that (P, Δ′′) is strongly regular. In what follows we often use (without explicitly mentioning it) the fact that S.α ∼ S for any process expression α.

Let us first observe that (C, Δ′′) ∼ (P′_{1}.S, Δ′′) which implies that (A^{i}.C, Δ′′) ∼ (P′_{1}.S, Δ′′) for all i, i ≥ 0. Using this fact we get that

(X.A^{i}.C, Δ′′) ∼ (P′_{1}.S, Δ′′)  (2)

for all i, i ≥ 0. Recall that (P_{1}, Δ) is a strongly regular process. It is easily seen now that (P′_{1}.S, Δ′′) is also a strongly regular process. Hence (2) in particular gives that (X.A^{0}.C, Δ′′) = (X.C, Δ′′) = (P, Δ′′) is strongly regular. ⊓ ⊔

Theorem 5 follows from Lemma 8 and Lemma 9. ⊓ ⊔

Theorem 6. Strong regularity of BPA is PSPACE-hard.

Proof. By Theorem 2, Remark 8 and Theorem 5. ⊓ ⊔

2 Under the usual assumption that Δ′ contains no deadlocks — see Subsection 2.3. This is obviously the case for processes from Theorem 2.

4.3 Strong Regularity of Normed BPA and BPP

This subsection aims to show that under the condition of normedness, strong regularity of BPA and BPP are complete problems for nondeterministic logarithmic space (NL). Kučera in [18] argues that strong regularity of BPA and BPP is decidable in polynomial time but it is easy to see that a test whether a BPA (BPP) process contains an accessible and growing process constant (a condition equivalent to regularity) can be performed even in nondeterministic logarithmic space. In [19] the previous results are extended to normed PA processes, and again it can be shown that the decision algorithm for strong regularity of normed PA can be implemented in NL.

Theorem 7. Strong regularity of normed BPA and normed BPP is NLhard.

Proof. In order to prove NL-hardness, we reduce the reachability problem for acyclic directed graphs (NL-complete problem, see e.g. [24]) to strong regularity checking of normed BPA (BPP).

Problem: Reachability for acyclic directed graphs Instance: An acyclic directed graph G = (V, E) such that

V = {v_{1}, …, v_{n}}, 1 ≤ n, and E ⊆ V × V.

Question: Is it the case that (v_{1}, v_{n}) ∈ E^{∗} where E^{∗} is a reflexive and transitive closure of E?

Let G = (V, E) be an instance of the reachability problem for acyclic directed graphs. For u ∈ V we define its out-degree by

u^{+} =^{def} |{v ∈ V | (u, v) ∈ E}|

and without loss of generality assume that v_{1}^{+}, v_{n}^{+} > 0. Let Δ be a finitestate system such that Const(Δ) =^{def} {X_{u} | u ∈ V ∧ u^{+} > 0} ∪ {X}, Act(Δ) =^{def} {a} and

Δ =^{def} {X_{u} ⟶^{a} X_{v} | (u, v) ∈ E ∧ v^{+} > 0} ∪

{X_{u} ⟶^{a} ϵ | (u, v) ∈ E ∧ v^{+} = 0} ∪

{X_{v_{n}} ⟶^{a} X}.

Obviously, (v_{1}, v_{n}) ∈ E^{∗} if and only if X_{v_{1}} ⟶^{∗} X. Let us define a BPA system

Δ_{1} =^{def} Δ ∪ {X ⟶^{a} X.X, X ⟶^{a} ϵ}

and a BPP system

Δ_{2} =^{def} Δ ∪ {X ⟶^{a} X||X, X ⟶^{a} ϵ}.

It is an easy observation that (X, Δ_{1}) and (X, Δ_{2}) are normed and nonregular processes. This implies that (X_{v_{1}}, Δ_{1}) and (X_{v_{1}}, Δ_{2}) are also normed processes (G is acyclic) such that (v_{1}, v_{n}) ∈ E^{∗} iff (X_{v_{1}}, Δ_{1}) is not strongly regular, and (v_{1}, v_{n}) ∈ E^{∗} iff (X_{v_{1}}, Δ_{2}) is not strongly regular. Recall that NL=co-NL (see e.g. [24]). Hence the problems of strong regularity for normed BPA and BPP are NL-hard (our reductions are obviously in logarithmic space). ⊓ ⊔

5 Conclusion

We proved that strong bisimilarity and regularity problems for BPA and BPP are PSPACE-hard. Our proofs are by reduction from the problem of quantified satisfiability (QSAT). The general idea (Subsection 3.1) for generating quantified instances of QSAT applies to both BPA and BPP. However, the proofs for BPA and BPP differ in checking that all clauses are indeed satisfied. This is due to the fact that BPP enables parallel access to all process constants contained in the current state whereas BPA does not.

We expect that the technique for generation of QSAT instances can be used in similar contexts, e.g. for showing lower bounds of weak bisimilarity.

An interesting observation is that only one unnormed process constant (namely S) is used in the hardness proofs for BPA. In contrast, the hardness proofs for strong bisimilarity of BPP (see [20] and Subsection 3.2) require a polynomial number of unnormed process constants.

In Figure 7 we present the state of the art of strong bisimilarity and regularity checking for BPA, BPP and PA and their normed subclasses. Results proved in this paper are in boldface. Obviously, all the lower bounds for BPA and BPP apply also to PA.

Acknowledgement. I would like to thank my advisor Mogens Nielsen for his kind supervision and useful suggestions, and Pawel Sobocinski and Jan Strejček for their remarks on some earlier drafts. I also thank the anonymous referees of STACS’02 and ICALP’02 for useful comments and suggestions.

strong bisimilarity  strong regularity

BPA ∈ 2-EXPTIME [4] PSPACE-hard ∈ 2-EXPTIME [5, 4] PSPACE-hard

normed BPA

\begin{matrix}∈ P [11] \\ P-hard [1] \end{matrix}
∈ NL [18] ; NL-hard

BPP

decidable [8] PSPACE-hard decidable [16] PSPACE-hard

normed BPP

\begin{matrix}∈ P [12] \\ P-hard [1] \end{matrix}
∈ NL [18] ; NL-hard

PA

? PSPACE-hard

? PSPACE-hard

normed PA 2-NEXPTIME [10] P-hard [1]

∈ NL [19] ; NL-hard

Fig. 7. Summary of results for BPA, BPP and PA

References

[1] J. Balcazar, J. Gabarro, and M. Santha. Deciding bisimilarity is P-complete. Formal Aspects of Computing, 4(6A):638–648, 1992.

[2] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.

[3] O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545–623. Elsevier Science, 2001.

[4] O. Burkart, D. Caucal, and B. Steffen. An elementary decision procedure for arbitrary context-free processes. In Proceedings of MFCS’95, volume 969 of LNCS, pages 423–433. Springer-Verlag, 1995.

[5] O. Burkart, D. Caucal, and B. Steffen. Bisimulation collapse and the process taxonomy. In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 247– 262. Springer-Verlag, 1996.

[6] D. Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106(1):61–86, 1992.

[7] S. Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, The University of Edinburgh, 1993.

[8] S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation is decidable for basic parallel processes. In Proceedings of CONCUR’93, volume 715 of LNCS, pages 143–157. Springer-Verlag, 1993.

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

[10] Y. Hirshfeld and M. Jerrum. Bisimulation equivalence is decidable for normed process algebra. In Automata, Languages and Programming, 26th International Colloquium (ICALP’99), volume 1644 of LNCS, pages 412–421. Springer-Verlag, 1999.

[11] Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 158(1–2):143–159, 1996.

[12] Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial-time algorithm for deciding bisimulation equivalence of normed basic parallel processes. Mathematical Structures in Computer Science, 6(3):251–259, 1996.

[13] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

[14] H. Hüttel. Undecidable equivalences for basic parallel processes. In Proceedings of TACS’94, volume 789 of LNCS, pages 454–464. Springer-Verlag, 1994.

[15] P. Jančar. High undecidability of weak bisimilarity for Petri nets. In Proceedings of Colloquium on Trees in Algebra and Programming (CAAP’95), volume 915 of LNCS, pages 349–363. Springer-Verlag, 1995.

[16] P. Jančar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. In Proceedings of ICALP’96, volume 1099 of LNCS, pages 478–489. Springer-Verlag, 1996.

[17] Lalita Jategaonkar and Albert R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154(1):107–143, 1996.

[18] A. Kučera. Regularity is decidable for normed BPA and normed BPP processes in polynomial time. In Proceedings of SOFSEM’96, volume 1175 of LNCS, pages 377–384. Springer-Verlag, 1996.

[19] A. Kučera. Regularity is decidable for normed PA processes in polynomial time. In Proceedings of FST&TCS’96, volume 1180 of LNCS, pages 111–122. Springer-Verlag, 1996.

[20] R. Mayr. On the complexity of bisimulation problems for basic parallel processes. In Proceedings of 27st International Colloquium on Automata, Languages and Programming (ICALP’00), volume 1853 of LNCS, pages 329–341. Springer-Verlag, 2000.

[21] R. Mayr. Process rewrite systems. Information and Computation, 156(1):264– 286, 2000.

[22] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[23] F. Moller. Infinite results. In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 195–216. Springer-Verlag, 1996.

[24] Ch.H. Papadimitriou. Computational Complexity. Addison-Wesley, New York, 1994.

[25] D.M.R. Park. Concurrency and automata on infinite sequences. In Proceedings 5^{th} GI Conference, volume 104 of LNCS, pages 167–183. Springer-Verlag, 1981.

[26] G. Plotkin. A structural approach to operational semantics. Technical Report Daimi FN-19, Department of Computer Science, University of Aarhus, 1981.

[27] J. Srba. Basic process algebra with deadlocking states. Theoretical Computer Science, 266(1–2):605–630, 2001.

[28] J. Srba. Strong bisimilarity and regularity of basic parallel processes is PSPACEhard. In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), volume 2285 of LNCS, pages 535–546. Springer-Verlag, 2002.

[29] J. Srba. Strong bisimilarity and regularity of basic process algebra is PSPACEhard. In Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP’02), LNCS. Springer-Verlag, 2002. To appear.

[30] C. Stirling. Local model checking games. In Proceedings of the 6th International Conference on Concurrency Theory (CONCUR’95), volume 962 of LNCS, pages 1–11. Springer-Verlag, 1995.

[31] W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract). In Proceedings of the 4th International Joint Conference CAAP/FASE, Theory and Practice of Software Development (TAPSOFT’93), volume 668 of LNCS, pages 559–568. Springer-Verlag, 1993.

[32] R.J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, CWI/Vrije Universiteit, 1990.

[33] R.J. van Glabbeek. The linear time—branching time spectrum. In Proceedings of CONCUR’90, volume 458 of LNCS, pages 278–297. Springer-Verlag, 1990.

Recent BRICS Report Series Publications

RS-02-16 Jiří Srba. Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds. April 2002. 33 pp. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-15 Jesper Makholm Nielsen. On the Number of Maximal Independent Sets in a Graph. April 2002. 10 pp.

RS-02-14 Ulrich Berger and Paulo B. Oliva. Modified Bar Recursion. April 2002. 23 pp.

RS-02-13 Gerth Stølting Brodal, Rune B. Lyngsø, Anna Östlin, and Christian N. S. Pedersen. Solving the String Statistics Problem in Time O(n log n). March 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-12 Olivier Danvy and Mayer Goldberg. There and Back Again. March 2002. This report supersedes the earlier report BRICS RS-01-39.

RS-02-11 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Extending Java for High-Level Web Service Construction. March 2002.

RS-02-10 Ulrich Kohlenbach. Uniform Asymptotic Regularity for Mann Iterates. March 2002. 17 pp.

RS-02-9 Anna Östlin and Rasmus Pagh. One-Probe Search. February 2002. 17 pp.

RS-02-8 Ronald Cramer and Serge Fehr. Optimal Black-Box Secret Sharing over Arbitrary Abelian Groups. February 2002. 19 pp.

RS-02-7 Anna Ingólfsdóttir, Anders Lyhne Christensen, Jens Alsted Hansen, Jacob Johnsen, John Knudsen, and Jacob Illum Rasmussen. A Formalization of Linkage Analysis. February 2002. vi+109 pp.