BRICS RS-00-16 J. Srba: Complexity of Weak Bisimilarity and Regularity for BPA and BPP BRICS

Basic Research in Computer Science

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

Jiří Srba BRICS Report Series RS-00-16 ISSN 0909-0878 June 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, 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/00/16/

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

Jiří Srba

BRICS^{⋆} Department of Computer Science University of Aarhus Ny Munkegade bld. 540 DK-8000 Aarhus C, Denmark

                        srba@brics.dk

Abstract. It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Π_{2}^{P} -hard. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP. Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a Π_{2}^{P} -hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and co-NP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed processes.

Keywords: BPA, BPP, weak bisimulation, weak regularity, complexity

1 Introduction

An intensive study of a variety of process algebras based on the interleaving model of CCS (see [Mil89]) has taken place in the last couple of years. Lots of activity has been focused on the analysis of infinite state systems. The two central questions are decidability and complexity of certain behavioural equivalences (for a survey see [Mol96]) and verification of system properties expressed in suitable logics (for a survey see [BE97]).

⋆

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

In this paper we address the first question with a special focus on the bisimulation equivalence. Strong bisimulation equivalence is known to be decidable for the classes of Basic Process Algebra (BPA)

[CHS95] and Basic Parallel Processes (BPP) [CHM93]. If we restrict ourself to normed processes, there are even polynomial time algorithms for bisimilarity of BPA and BPP [HJM96a,HJM96b]. However, we draw our attention towards the notion of weak bisimilarity, which is a more general equivalence than strong bisimilarity, in the sense that it allows to abstract from internal behaviour of processes by introducing a silent action τ, which is not observable [Mil89]. Decidability of weak bisimulation equivalence and weak regularity (finiteness) for BPA and BPP are well known open problems. There are partial results, e.g. by Hirshfeld [Hir96], showing decidability of weak bisimilarity for restricted classes of so called totally normed BPA and BPP. Stribrna proved in [Str98] NP-hardness for these restricted classes. Also, some results are known about weak bisimilarity of BPA/BPP with finite state systems [JKM98,KM99]. In spite of the fact that weak bisimilarity and regularity are not known to be decidable, only a few lower bounds have been found. For weak bisimilarity in the BPA class, PSPACE-hardness was proved by Stribrna [Str98], using a reduction from totality problem for finite nondeterministic automata. No lower bound has previously been established for weak regularity in this class. In the class of BPP, weak bisimilarity appeared to be NP-hard [Str98]. This result was recently improved by Mayr [May00a] to Π_{2}^{P} (in polynomial hierarchy). In the same paper, Π_{2}^{P} -hardness for weak regularity is proved.

Our contribution. We show PSPACE-hardness of weak bisimilarity for BPP, thus improving the Π_{2}^{P} -hardness result by Mayr, and moreover we prove our result for the restricted class of normed BPP. This result can be transformed to weak regularity for BPP, thus achieving PSPACE lower bound (again even for normed processes). For the class of BPA we prove DP-hardness of weak regularity, which in particular means both NP and co-NP-hardness. Moreover NPhardness can be transformed to the normed case.

All these results hold also for PA (Process Algebra [BW90]), which is a natural “union” of BPA and BPP, where we are allowed to use both sequential and parallel composition.

2 Basic definitions

Let Act and Const be countable sets of actions and process constants such that Act ∩ Const = ∅. Moreover suppose that Act contains a distinguishable silent action τ. Let Op ⊆ {. , ||}. We define the class of process expressions over Op as

E_{Op} ::= ϵ | X | E ⊗ E

where ϵ is the empty process, X ranges over Const and ⊗ ranges over Op. The operator ‘.’ is a sequential composition, and ‘||’ stands for a parallel composition. In what follows we will not distinguish between process expressions related by a structural congruence, which is the smallest congruence over process expressions such that the following lows hold:

– ‘.’ is associative

– ‘||’ is associative and commutative

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

In this paper we consider the class of PA (Process Algebra [BW90]) expressions E_{{., ||}} and its natural subclasses; BPA (Basic Process Algebra, also known as context-free processes) expressions E_{{.}} with only sequential composition; and BPP (Basic Parallel Processes) expressions E_{{||}} with only parallel composition. A PA (resp. BPA or BPP) process rewrite system (PRS) [May00b] is a finite set Δ of rules of the form X ⟶^{a} E, where X ∈ Const, a ∈ Act and E ∈ E_{{., ||}} (resp. E ∈ E_{{.}} or E ∈ E_{{||}}). Let us denote the set of actions and process constants that appear in Δ as Act(Δ) resp. Const(Δ) (note that these sets are finite). A process rewrite system Δ determines a transition system [Plo81,Mol96] where the states are process expressions over Const(Δ), and Act(Δ) is the set of labels. The transition relation is the least relation satisfying the following SOS rules (recall that ‘||’ is commutative).

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

As usual we extend the transition relation to the elements of Act^{∗}. We also write E ⟶^{∗} E′, whenever E ⟶^{w} E′ for some w ∈ Act^{∗}. A state E′ is reachable from a state E iff E ⟶^{∗} E′. A weak transition relation is defined as follows.

⟹^{a}=^{def} \{ \begin{matrix}⟶^{τ^{∗}} ∘ ⟶^{a} ∘ ⟶^{τ^{∗}} & if a ≠ τ \\ ⟶^{τ^{∗}} & if a = τ \end{matrix}

We define a process as a pair (P, Δ), where P is a process expression and Δ is a process rewrite system. States of (P, Δ) are the states of the corresponding transition system. We say that a state E is reachable iff P ⟶^{∗} E. Whenever (P, Δ) has only finitely many reachable states, we call it a finite-state process. Important subclasses of process algebras can be obtained by an extra restriction on the involved processes - normedness. A process expression E is normed iff there is w ∈ Act^{∗} such that E ⟶^{w} ϵ. A process (P, Δ) is normed if all its process constants Const(Δ) are normed. We say that (P, Δ) is totally normed iff it is normed and moreover there is no transition X ⟹^{τ} ϵ for any X ∈ Const(Δ). Now we will introduce the concept of weak bisimilarity [Par81,Mil89]. A binary relation R over process expressions is a weak bisimulation iff whenever (E, F) ∈ R then for each a ∈ Act:

– if E ⟹^{a} E′ then F ⟹^{a} F′ and (E′, F′) ∈ R

– if F ⟹^{a} F′ then E ⟹^{a} E′ and (E′, F′) ∈ R.

Processes (P_{1}, Δ_{1}) and (P_{2}, Δ_{2}) are weakly bisimilar, and we write (P_{1}, Δ_{1}) ≈ (P_{2}, Δ_{2}), iff there is a weak bisimulation R such that (P_{1}, P_{2}) ∈ R. Note that without loss of generality we can suppose that Δ_{1} = Δ_{2} since we can always consider a disjoint union of Δ_{1} and Δ_{2} as a new Δ. Bisimulation equivalence has an elegant characterisation in terms of bisimulation games [Tho93,Sti95]. A bisimulation game on a pair of processes (P_{1}, Δ) and (P_{2}, Δ) is a two-player game of an ‘attacker’ and a ‘defender’. The attacker chooses one of the processes and makes an ⟹^{a}-move for some a ∈ Act(Δ). The defender must respond by making an ⟹^{a}-move in the other process under the same action a. Now the game repeats, starting from the new processes. If one player cannot move, the other player wins. If the game is infinite, the defender wins. The processes (P_{1}, Δ) and (P_{2}, Δ) are weakly bisimilar iff the defender has a winning strategy (and non-bisimilar iff the attacker has a winning strategy).

3 Hardness of Weak Bisimilarity and Regularity for BPP

Problem: Weak bisimilarity of (normed) BPP Instance: Two (normed) BPP processes (P_{1}, Δ) and (P_{2}, Δ).

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

In what follows we show that weak bisimilarity of normed BPP is PSPACE-hard. We prove it by reduction from QSAT^{1}, which is known to be PSPACE-complete [Pap94].

Problem: \underline{QSAT}

Instance: A natural number n 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?

Literal is a variable or the negation of a variable. 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, where each clause C_{j}, 1 ≤ j ≤ k, is a disjunction of literals. We define the following BPP processes (P_{1}, Δ) and (P_{2}, Δ), where

Const(Δ) = {Q_{1}, …, Q_{k}, X_{1}, …, X_{n}, Y_{1}, …, Y_{n}}

and

Act(Δ) = \{q_{1}, …, q_{k}, x_{1}, …, x_{n}, \overline{x}_{1}, …, \overline{x}_{n}, y\}.

For each i, 1 ≤ i ≤ n, let

1 This problem is known also as QBF, for Quantified Boolean formula.

α_{i} be a parallel composition of process constants from {Q_{1}, …, Q_{k}} such that Q_{j} appears in α_{i} iff the literal x_{i} occurs in C_{j} (i.e. if x_{i} is set to true then C_{j} is satisfied),

\overline{α_{i}} be a parallel composition of process constants from \{Q_{1}, …, Q_{k}\} such that Q_{j} appears in \overline{α_{i}} iff the literal ¬x_{i} occurs in C_{j} (i.e. if x_{i} is set to false then C_{j} is satisfied),

β_{i} be a parallel composition of process constants from {Q_{1}, …, Q_{k}}

such that Q_{j} appears in β_{i} iff the literal y_{i} occurs in C_{j}, \overline{β_{i}} be a parallel composition of process constants from \{Q_{1}, …, Q_{k}\}

such that Q_{j} appears in \overline{β_{i}} iff the literal ¬y_{i} occurs in C_{j}.

The set of transition rules Δ is given by

X_{i} ⟶^{x_{i}} Y_{i}||α_{i}  X_{i} ⟶^{\overline{x}_{i}} Y_{i}||\overline{α_{i}}  for 1 ≤ i ≤ n
Y_{i} ⟶^{y} X_{i+1}||β_{i} Y_{i} ⟶^{y} X_{i+1}||\overline{β_{i}} for 1 ≤ i ≤ n − 1
Y_{n} ⟶^{y} β_{n}  Y_{n} ⟶^{y} \overline{β_{n}}
X_{i} ⟶^{q_{j}} X_{i}  Y_{i} ⟶^{q_{j}} Y_{i}  for 1 ≤ i ≤ n and 1 ≤ j ≤ k
Q_{j} ⟶^{q_{j}} Q_{j}  Q_{j} ⟶^{τ} ϵ  for 1 ≤ j ≤ k.

Finally, let

P_{1} =^{def} X_{1}||Q_{1}||Q_{2}|| … ||Q_{k} and P_{2} =^{def} X_{1}.

We can see the processes P_{1} and P_{2} using Petri net notation in Figure 1. This figure is only illustrative, and some transitions, namely X_{i} ⟶^{q_{j}} X_{i} and Y_{i} ⟶^{q_{j}} Y_{i} for 1 ≤ i ≤ n, 1 ≤ j ≤ k are missing. The curly lines stand for the corresponding sets of arrows for α_{i}, \overline{α_{i}}, β_{i} resp. \overline{β_{i}}. The intuition is that the attacker will be forced to play only in the process P_{1} and if C is true then the defender will have the possibility to add all the process constants {Q_{1}, …, Q_{k}}. Let γ be a parallel composition of elements from Const(Δ). We define the set of process constants that occur in γ as set(γ) =^{def} {X ∈ Const(Δ) | X occurs in γ} and we also define set_{Q}(γ) =^{def} set(γ) ∩ {Q_{1}, …, Q_{k}}. The following proposition is an immediate consequence of the definition of Δ.

[figure: X_{1}; •; x_{1}; \overline{x}_{1}; q_{1}; Y_{1}; •; Q_{1}; y; y; τ; X_{2}; ⋮; ⋮; q_{k}; X_{n}; •; Q_{k}; x_{n}; \overline{x}_{n}; τ; Y_{n}; y; y; X_{1}; •; x_{1}; \overline{x}_{1}; q_{1}; Y_{1}; Q_{1}; y; y; τ; X_{2}; ⋮; ⋮; q_{k}; X_{n}; Q_{k}; x_{n}; \overline{x}_{n}; τ; Y_{n}; y; y]

Fig. 1. The processes (P_{1}, Δ) and (P_{2}, Δ) as Petri nets.

Proposition 1. Let γ resp. γ′ be a parallel composition of some process constants from {Q_{1}, …, Q_{k}}. If set_{Q}(γ) = set_{Q}(γ′) then (γ, Δ) ≈ (γ′, Δ).

We want to show that C is true if and only if (P_{1}, Δ) ≈ (P_{2}, Δ).

Lemma 1. If (P_{1}, Δ) ≈ (P_{2}, Δ) then C is true.

Proof. We show that (P_{1}, Δ) ≉ (P_{2}, Δ), supposing that C is false. If

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

is true and from this we claim that the attacker has a winning strategy in the bisimulation game for (P_{1}, Δ) and (P_{2}, Δ). The attacker plays only in the process P_{1} (without using τ actions) performing the following sequence of actions

x̃_{1}, y, x̃_{2}, y, …, x̃_{n}, y

where x̃_{i}, 1 ≤ i ≤ n, corresponds to either x_{i} or \overline{x}_{i}, depending on the truth values for which the formula C′ is true. It does not matter, how the choice of the rule for the action y is solved. The defender can only respond by performing the same actions x̃_{1}, y, x̃_{2}, y, …, x̃_{n}, y (eventually using some τ actions). The actions x̃_{1}, …, x̃_{n} are forced. For the action y there are always two possibilities, corresponding to assigning a truth value for some y_{i}, 1 ≤ i ≤ n. Finally the processes P_{1} and P_{2} are in states P′_{1} and P′_{2}, respectively, such that set(P′_{1}) = {Q_{1}, …, Q_{k}} and set(P′_{2}) ⊆ {Q_{1}, …, Q_{k}}. Since we assume that C′ is true, there must be a clause C_{j}, 1 ≤ j ≤ k, which is not satisfied. Hence Q_{j} ∉ set(P′_{2}) and P′_{2} cannot perform q_{j}. However, q_{j} is enabled in P′_{1} and thus the attacker has a winning strategy. This implies that (P_{1}, Δ) ≉ (P_{2}, Δ). ⊓ ⊔

For the proof of the opposite direction let us first observe the following property of (P_{1}, Δ) and (P_{2}, Δ) above. Let δ be some state such that set(δ) ∩ {Q_{1}, …, Q_{k}} = ∅ and let γ and γ′ be a parallel composition of some process constants from {Q_{1}, …, Q_{k}} satisfying the condition that set_{Q}(γ) ⊇ set_{Q}(γ′). Let us consider the processes δ||γ and δ||γ′. Whenever the attacker chooses any move in the second one, the defender has an answer, which makes these two processes weakly bisimilar (exploiting τ actions to eliminate the extra process constants Q_{j} from the first process and then using Proposition 1). We are now ready to prove the following lemma.

Lemma 2. If C is true then (P_{1}, Δ) ≈ (P_{2}, Δ).

Proof. Let P′_{1} and P′_{2} denote successors of P_{1} and P_{2}, respectively, in the bisimulation game. The defender’s strategy is to satisfy the following conditions during the game

– set_{Q}(P′_{1}) ⊇ set_{Q}(P′_{2}) and

– never delete (using τ actions) any process constant Q_{j}, 1 ≤ j ≤ k, in the process P′_{2}, unless it is necessary for satisfying the first condition.

Of course these conditions are true at the beginning of the game. Using the argument above this lemma, we can see that whenever the attacker makes a move in the process P′_{2}, he immediately looses, since the defender can make the resulting processes weakly bisimilar. This means that the only possible winning strategy for the attacker is to keep playing in P′_{1}. However, now the defender can always fulfil the conditions of his strategy. On a move containing x_{i} resp. \overline{x}_{i} there is only one possible response for the defender. Whenever the attacker makes a y move, the defender chooses one of the rules Y_{i} ⟶^{y} X_{i+1}||β_{i} and Y_{i} ⟶^{y} X_{i+1}||\overline{β_{i}}, such that the formula ∀x_{i+1}∃y_{i+1} … ∀x_{n}∃y_{n}.C_{1} ∧ … ∧ C_{k} is still true. Since we have the rules X_{i} ⟶^{q_{j}} X_{i} and Y_{i} ⟶^{q_{j}} Y_{i} for any i, j such that 1 ≤ i ≤ n and 1 ≤ j ≤ k, the only possibility for the attacker to win is to perform some sequence

x̃_{1}, y, x̃_{2}, y, …, x̃_{n}, y

possibly including also some τ actions and then reach some state P′_{1}, where set(P′_{1}) ⊆ {Q_{1}, …, Q_{k}}. Since C is true the defender can always get to a corresponding state P′_{2}, where set(P′_{1}) = set(P′_{2}). Hence (using Proposition 1) the attacker looses again. This means that the defender has a winning strategy and so (P_{1}, Δ) ≈ (P_{2}, Δ).

⊓ ⊔

Theorem 1. Weak bisimilarity of normed BPP is PSPACE-hard.

Proof. Observe that all the process constants in Δ are normed and that the reduction is in polynomial time. The theorem is then an immediate consequence of Lemma 1 and Lemma 2. ⊓ ⊔

Corollary 1. Weak bisimilarity of BPP is PSPACE-hard.

Proof. Directly from Theorem 1. ⊓ ⊔

Remark 1. Theorem 1 can be easily extended to 1-safe Petri nets where each transition has exactly one input place (for the definition of 1-safe Petri nets see e.g. [JM96]). It is enough to introduce for each α_{i}/\overline{α_{i}} and β_{i}/\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. Related results about 1-safe Petri nets can be found in [JM96].

Another problem we will analyse, is weak regularity of BPP processes.

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

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

Mayr has proved that weak regularity of BPP is Π_{2}^{P} -hard [May00a], demonstrating a reduction from the weak bisimilarity problem between a pair of special processes with finitely many reachable states. It can be easily seen that his proof works also for a general pair of weakly regular processes and moreover it preserves normedness.

Theorem 2 ([May00a]). Let (P_{1}, Δ) and (P_{2}, Δ) be weakly regular BPP processes. We can construct in polynomial time a BPP process (P, Δ′) such that

(P_{1}, Δ) ≈ (P_{2}, Δ) ⟺ (P, Δ′) is weakly regular.

Moreover, if (P_{1}, Δ) and (P_{2}, Δ) are normed, so is (P, Δ′).

Observe that the processes P_{1} and P_{2} from the proof of PSPACEhardness of weak bisimilarity (Theorem 1) are regular and moreover they are normed. This gives the following theorem with an immediate corollary.

Theorem 3. Weak regularity of normed BPP is PSPACE-hard.

Proof. Because of Theorem 2, there is a reduction from a PSPACEhard problem of weak bisimilarity for normed BPP to weak regularity of normed BPP. ⊓ ⊔

Corollary 2. Weak regularity of BPP is PSPACE-hard.

4 Hardness of Weak Bisimilarity and Regularity for BPA

In this section we consider the same problems for BPA, as we did for BPP.

Problem: Weak bisimilarity of (normed) BPA Instance: Two (normed) BPA processes (P_{1}, Δ) and (P_{2}, Δ).

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

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

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

First, we show that there is a reduction from weak bisimilarity of regular BPA to weak regularity. The idea of the proof is similar to the case of BPP mentioned above from [May00a].

Theorem 4. Let (P_{1}, Δ) and (P_{2}, Δ) be weakly regular BPA processes. We can construct in polynomial time a BPA process (P, Δ′) such that

(P_{1}, Δ) ≈ (P_{2}, Δ) ⟺ (P, Δ′) is weakly regular.

Moreover, if (P_{1}, Δ) and (P_{2}, Δ) are normed, so is (P, Δ′).

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

Const(Δ′) =^{def} Const(Δ) ∪ {A, B, C, B_{1}, B_{2}}

and

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

where A, B, C, B_{1}, B_{2} are new process constants and a is a new action. Then Δ′ =^{def} Δ ∪ Δ^{1} ∪ Δ^{2}, where Δ^{1} and Δ^{2} are defined as follows. The set of transition rules Δ^{1} is given by

\begin{matrix}A ⟶^{a} A.B & A ⟶^{τ} ϵ \\ B ⟶^{a} ϵ & B ⟶^{τ} ϵ \\ C ⟶^{a} B_{1} & C ⟶^{a} P_{1} \\ B_{1} ⟶^{a} B_{1} & B_{1} ⟶^{a} P_{1} \end{matrix}

and Δ^{2} is given by

\begin{matrix}C ⟶^{a} B_{2} & C ⟶^{a} P_{2} \\ B_{2} ⟶^{a} B_{2} & B_{2} ⟶^{a} P_{2}. \end{matrix}

Let P =^{def} A.C. Observe that if (P_{1}, Δ) and (P_{2}, Δ) are normed, so is (P, Δ′). We show now that our reduction is correct.

Lemma 3. If (P_{1}, Δ) ≉ (P_{2}, Δ) then (P, Δ′) is not weakly regular.

Proof. Suppose that (P_{1}, Δ) ≉ (P_{2}, Δ). Then we demonstrate that there are infinitely many weakly nonbisimilar states reachable from P. Let us consider B^{i}.C for any natural number i. Of course P ⟶^{∗} B^{i}.C and we claim that (B^{i}.C, Δ′) ≉ (B^{j}.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 2). He performs a sequence of j actions a in B^{j}.C, thus

[figure: B^{i}.C; a^{i′}; ≈^{?}; B^{j}.C; a^{i′}; C; a; B^{j−i′}.C; a; B_{1}; a^{j−i′−1}; B^{j−i′−1}.C; a^{j−i′−1}; B_{1}; a; C; a; P_{1}; ≉; P_{2}]

Fig. 2. The winning strategy for the attacker (i < j).

reaching C. Since B^{i} cannot do this sequence, the defender has to reach C eventually (let us say after i′ steps, where i′ ≤ i). As neither P_{1} nor P_{2} can perform a, he has only two choices when responding to the action a – either C ⟶^{a} B_{1} or C ⟶^{a} B_{2}. Assume that he chooses B_{1} (the other case is symmetric). Now the defender’s only possibility is to stay in B_{1} for another a^{j−i′−1} moves of the attacker. After the attacker has reached C (in the second process), he chooses to go to P_{2} in the next round. If the defender stays in B_{1} he looses immediately and if he moves to P_{1} he looses as well, since (P_{1}, Δ′) ≉ (P_{2}, Δ′). ⊓ ⊔

Lemma 4. If (P_{1}, Δ) ≈ (P_{2}, Δ) then (P, Δ′) is weakly regular.

Proof. Assume that (P_{1}, Δ) ≈ (P_{2}, Δ), which implies that (P, Δ′) ≈ (P, Δ′′), where Δ′′ = Δ′ − Δ^{2} (weak bisimilarity is a congruence on BPA). Notice that (B_{1}, Δ′′) is weakly regular, so it is enough to show that (A.C, Δ′′) ≈ (B_{1}, Δ′′). Obviously, (C, Δ′′) ≈ (B_{1}, Δ′′), which implies that for any n ≥ 0, (B^{n}.C, Δ′′) ≈ (B_{1}, Δ′′) since B_{1} ⟶^{a} B_{1} and B^{n} ⟶^{τ^{∗}} ϵ. This gives that (A.B^{n}.C, Δ′′) ≈ (B_{1}, Δ′′) for any n ≥ 0, which in particular means that (A.C, Δ′′) ≈ (B_{1}, Δ′′). ⊓ ⊔

Theorem 4 is an immediate consequence of Lemma 3 and Lemma 4. ⊓ ⊔

In the paper by Stribrna [Str98] it is shown (Theorem 2.5) that weak bisimilarity for totally normed BPA is NP-hard. The proof is by reduction from a variant of the bin-packing (knapsack) problem and the processes in this proof have finitely many reachable states (and so they are weakly regular). Thus we can use Theorem 4 to obtain the following result with an obvious corollary.

Theorem 5. Weak regularity of normed BPA is NP-hard.

Corollary 3. Weak regularity of BPA is NP-hard.

We remind the reader of the fact that PSPACE-hardness of weak bisimilarity for BPA achieved by Stribrna [Str98] does not imply PSPACE-hardness of weak regularity for BPA, since the described processes are not regular. In the next theorem, however, we prove that weak regularity for BPA is not only NP-hard but also co-NP-hard. This we demonstrate by showing that weak bisimilarity for BPA is co-NP-hard, where the involved processes are finite-state (nevertheless they are unnormed in this case).

Theorem 6. Weak regularity of BPA is co-NP-hard.

Proof. We reduce the complement of 3-SAT [Pap94] to weak bisimilarity of BPA and then we use Theorem 4.

Problem: 3-SAT COMPLEMENT Instance: A natural number n and a Boolean formula ϕ in

disjunctive normal form with implicants of length 3 and with Boolean variables x_{1}, …, x_{n}.

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

Let

D ≡ ∀x_{1}∀x_{2} … ∀x_{n}.D_{1} ∨ D_{2} ∨ … ∨ D_{k}

be an instance of 3-SAT COMPLEMENT, where each implicant D_{j}, 1 ≤ j ≤ k, is a conjunction of three literals. Let us define the following BPA processes (X_{1}, Δ) and (X′_{1}, Δ), where

\begin{aligned}Const(Δ) =^{def} \{ & D_{1}^{1}, …, D_{k}^{1}, D_{1}^{2}, …, D_{k}^{2}, D_{1}^{3}, …, D_{k}^{3}, \\ & X_{1}, …, X_{n}, X_{n+1}, X′_{1}, …, X′_{n}, X′_{n+1}, Y_{1}, …, Y_{k}, A, S \} \end{aligned}

and

\begin{aligned}Act(Δ) =^{def} \{ & d_{1}^{1}, …, d_{k}^{1}, d_{1}^{2}, …, d_{k}^{2}, d_{1}^{3}, …, d_{k}^{3}, \\ & x_{1}, …, x_{n}, \overline{x}_{1}, …, \overline{x}_{n}, a, s\}. \end{aligned}

For each i, 1 ≤ i ≤ n, let

α_{i} be a sequential composition (in some fixed ordering) of process constants D_{j}^{r} (1 ≤ r ≤ 3 and 1 ≤ j ≤ k) such that

• D_{j}^{1} appears in α_{i} iff the literal x_{i} occurs in D_{j} in the first position

• D_{j}^{2} appears in α_{i} iff the literal x_{i} occurs in D_{j} in the second position

• D_{j}^{3} appears in α_{i} iff the literal x_{i} occurs in D_{j} in the third

position \overline{α_{i}} be a sequential composition (in some fixed ordering) of process

constants D_{j}^{r} (1 ≤ r ≤ 3 and 1 ≤ j ≤ k) such that

• D_{j}^{1} appears in \overline{α_{i}} iff the literal ¬x_{i} occurs in D_{j} in the first position

• D_{j}^{2} appears in \overline{α_{i}} iff the literal ¬x_{i} occurs in D_{j} in the second position

• D_{j}^{3} appears in \overline{α_{i}} iff the literal ¬x_{i} occurs in D_{j} in the third position.

The set of transition rules Δ is given by

X_{i} ⟶^{x_{i}} X_{i+1}.α_{i}  X′_{i} ⟶^{x_{i}} X′_{i+1}.α_{i} for 1 ≤ i ≤ n
X_{i} ⟶^{\overline{x}_{i}} X_{i+1}.\overline{α_{i}}  X′_{i} ⟶^{\overline{x}_{i}} X′_{i+1}.\overline{α_{i}} for 1 ≤ i ≤ n
X_{n+1} ⟶^{a} Y_{j}  X′_{n+1} ⟶^{a} Y_{j} for 1 ≤ j ≤ k

X′_{n+1} ⟶^{a} A

A ⟶^{a} A

A ⟶^{τ} ϵ

S ⟶^{s} S

Y_{j} ⟶^{d_{j}^{1}} S  Y_{j} ⟶^{d_{j}^{2}} S Y_{j} ⟶^{d_{j}^{3}} S  for 1 ≤ j ≤ k
Y_{j} ⟶^{a} Y_{j}  for 1 ≤ j ≤ k
Y_{j} ⟶^{τ} ϵ  for 1 ≤ j ≤ k
D_{j}^{1} ⟶^{d_{j}^{1}} S  D_{j}^{2} ⟶^{d_{j}^{2}} S D_{j}^{3} ⟶^{d_{j}^{3}} S  for 1 ≤ j ≤ k
D_{j}^{1} ⟶^{τ} ϵ  D_{j}^{2} ⟶^{τ} ϵ D_{j}^{3} ⟶^{τ} ϵ  for 1 ≤ j ≤ k.

The intuition is that the attacker plays in X′_{1} and generates some truth assignment. When he reaches the process constant A, the defender chooses an implicant that is satisfied by the truth assignment by performing a transition X_{n+1} ⟶^{a} Y_{j}. The attacker can now test whether this implicant is indeed satisfied.

Lemma 5. If (X_{1}, Δ) ≈ (X′_{1}, Δ) then D is true.

Proof. For the sake of contradiction suppose that D is false, i.e. there is some assignment of truth values for x_{1}, …, x_{n} such that D_{1} ∨ D_{2} ∨ … ∨ D_{k} is false, which means that for each j, 1 ≤ j ≤ k, there is at least one false literal in D_{j}. We show that the attacker has a winning strategy in the bisimulation game. First, the attacker plays in X′_{1} generating this false assignment and finally he uses the transition X′_{n+1} ⟶^{a} A. The defender can only respond by performing the same actions x_{i}/\overline{x}_{i} with the final transition X_{n+1} ⟶^{a} Y_{j} for some j (observe that the defender cannot use the transition Y_{j} ⟶^{τ} ϵ, otherwise the attacker wins immediately). Now the attacker changes the processes and plays Y_{j} ⟶^{d_{j}^{r}} S, where r is a position of a false literal in D_{j}. This means that the defender looses, since he has no response to this move. ⊓ ⊔

Lemma 6. If D is true then (X_{1}, Δ) ≈ (X′_{1}, Δ).

Proof. We show that the defender has a winning strategy. Whatever the attacker performs during the first n moves the defender imitates in the other process. Finally we get a pair of processes X_{n+1}α and X′_{n+1}α. If the attacker chooses the rule X_{n+1} ⟶^{a} Y_{j} for some j then he looses, since the defender can do the same move in X′_{n+1}α and make the resulting processes equal. The same happens if the attacker chooses the rule X′_{n+1} ⟶^{a} Y_{j} for some j in the second process. So the only possibility for the attacker to win is to move under a to A.α in the second process. The defender answers by performing X_{n+1} ⟶^{a} Y_{j}, where D_{j} is the implicant which makes the formula D_{1} ∨ D_{2} ∨ … ∨ D_{k} true. Now the attacker has to switch processes since if he continues in A.α doing the τ action, he looses again (the defender can make the two processes equal). In the process Y_{j}.α the

attacker has essentially two possibilities. He can perform Y_{j} ⟶^{d_{j}^{r}} S for some r, 1 ≤ r ≤ 3. However, the defender can perform some sequence of τ actions to enable d_{j}^{r} in the second process and then he performs

the transition D_{j}^{r} ⟶^{d_{j}^{r}} S. As S is unnormed, the resulting processes are bisimilar (since (S.β, Δ) ≈ (S.β′, Δ) for any β and β′). The other attacker’s possibility is to perform first Y_{j} ⟶^{τ} ϵ, but then he looses as well (the resulting processes can be made equal). Thus the defender has a winning strategy, which means that (X_{1}, Δ) ≈ (X′_{1}, Δ). ⊓ ⊔

The proof of Theorem 6 is then a consequence of Lemma 5, Lemma 6, Theorem 4 and the fact that both (X_{1}, Δ) and (X′_{1}, Δ) are finitestate processes. ⊓ ⊔

Corollary 3 and Theorem 6 show that weak regularity for BPA is both NP and co-NP-hard. We use these results to obtain DPhardness. The class DP is defined as follows [Pap94]. A language L is in DP iff there are two languages L_{1} ∈ NP and L_{2} ∈ co-NP such that L = L_{1} ∩ L_{2}. Obviously NP ∪ co-NP is contained in DP and moreover the other inclusion is unlikely. We show that weak regularity is DP-hard by demonstrating a reduction from the SAT-UNSAT problem [Pap94].

Problem: \underline{SAT-UNSAT}

Instance: Two Boolean formulae ϕ_{1} and ϕ_{2}.

Question: Is ϕ_{1} satisfiable and ϕ_{2} is not?

Theorem 7. Weak regularity of BPA is DP-hard.

Proof. As we know that weak regularity is both NP and co-NP-hard, we can construct in polynomial time processes (P_{1}, Δ) and (P_{2}, Δ) such that (P_{1}, Δ) is weakly regular iff ϕ_{1} is satisfiable, and (P_{2}, Δ) is weakly regular iff ϕ_{2} is not satisfiable. Let us now construct a process (P, Δ′) such that (P, Δ′) is weakly regular iff ϕ_{1} is satisfiable and ϕ_{2} is not. We define Const(Δ′) =^{def} Const(Δ)∪{P } and Act(Δ′) =^{def} Act(Δ) ∪ {a_{1}, a_{2}} where P is a new process constant and a_{1}, a_{2} are new actions. The set Δ′ contains all the rules from Δ together with

P ⟶^{a_{1}} P_{1} P ⟶^{a_{2}} P_{2}.

Obviously (P, Δ′) is regular iff both (P_{1}, Δ) and (P_{2}, Δ) are regular. This proves that (P, Δ′) is weakly regular iff ϕ_{1} is satisfiable and ϕ_{2} is not. ⊓ ⊔

5 Conclusion

In the following tables we summarise known results about weak bisimilarity and regularity problems for BPA, BPP and PA. The results obtained in this paper are in boldface. Question mark means that there has not been any known lower bound yet.

≈

≈

of normed processes

BPA PSPACE-hard [Str98]  NP-hard [Str98]
NP-hard [Str98]  NP-hard [Str98]
BPP  Π_{2}^{P} -hard [May00a]
PSPACE-hard  PSPACE-hard
PA  PSPACE-hard [Str98]  NP-hard [Str98]
PSPACE-hard  PSPACE-hard

For the case of ≈ in the class of PA, the result in this paper is more general, since our processes are weakly regular, which is not the case for the result by Stribrna.

weak regularity

weak regularity of normed processes

BPA  ?  ?
DP-hard  NP-hard
BPP  Π_{2}^{P} -hard [May00a]  ?
PSPACE-hard  PSPACE-hard
PA  Π_{2}^{P} -hard [May00a]  ?
PSPACE-hard  PSPACE-hard

We remind the reader of the fact that DP-hardness means in particular both NP and co-NP-hardness.

Acknowledgement. I would like to thank my advisor Mogens Nielsen for his kind supervision and encouragement.

References

[BE97] Olaf Burkart and Javier Esparza. More infinite results. Bulletin of the European Association for Theoretical Computer Science, 62:138–159, June 1997. Columns: Concurrency.

[BW90] J.C.M. Baeten and W.P. Weijland. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

[CHM93] 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.

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

[Hir96] Yoram Hirshfeld. Bisimulation trees and the decidability of weak bisimulations. In Proceedings of the the First International Workshop on Verification of Infinite State Systems (Infinity’96), volume 5 of ENTCS. Springer-Verlag, 1996.

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

[HJM96b] Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. Mathematical Structures in Computer Science, 6(3):251–259, 1996.

[JKM98] P. Jancar, A. Kucera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. In Proceedings of the Annual International Colloquium on Automata, Languages and Programming (ICALP’98), volume 1443 of LNCS. Springer-Verlag, 1998.

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

[KM99] A. Kucera and R. Mayr. Weak bisimilarity with infinite-state systems can be decided in polynomial time. In Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99), volume 1664 of LNCS. Springer-Verlag, 1999.

[May00a] Richard Mayr. On the complexity of bisimulation problems for basic parallel processes. In Proceedings of 27st International Colloquium on Automata, Languages and Programming (ICALP’00), LNCS. Springer-Verlag, 2000. To appear.

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

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

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

[Pap94] Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, New York, 1994.

[Par81] 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.

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

[Sti95] Colin 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.

[Str98] Jitka Stribrna. Hardness results for weak bisimilarity of simple process algebras. In Proceedings of the MFCS’98 Workshop on Concurrency, volume 18 of ENTCS. Springer-Verlag, 1998.

[Tho93] Wolfgang 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,

Recent BRICS Report Series Publications

RS-00-16 Jiří Srba. Complexity of Weak Bisimilarity and Regularity for BPA and BPP. June 2000. 20 pp. To appear in Aceto and Victor, editors, Expressiveness in Concurrency: Fifth International Workshop EXPRESS ’00 Proceedings, ENTCS, 2000.

RS-00-15 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. June 2000. Extended version of an article to appear in Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, 2000.

RS-00-14 Ronald Cramer, Ivan B. Damgård, and Jesper Buus Nielsen. Multiparty Computation from Threshold Homomorphic Encryption. June 2000. ii+38 pp.

RS-00-13 Ondřej Klíma and Jiří Srba. Matching Modulo Associativity and Idempotency is NP-Complete. June 2000. 19 pp. To appear in Mathematical Foundations of Computer Science: 25 th International Symposium, MFCS ’00 Proceedings, LNCS, 2000.

RS-00-12 Ulrich Kohlenbach. Intuitionistic Choice and Restricted Classical Logic. May 2000. 9 pp.

RS-00-11 Jakob Pagter. On Ajtai’s Lower Bound Technique for R-way Branching Programs and the Hamming Distance Problem. May 2000. 18 pp.

RS-00-10 Stefan Dantchev and Søren Riis. A Tough Nut for Tree Resolution. May 2000. 13 pp.

RS-00-9 Ulrich Kohlenbach. Effective Uniform Bounds on the Krasnoselski-Mann Iteration. May 2000. 34 pp.

RS-00-8 Nabil H. Mustafa and Aleksandar Pekeč. Democratic Consensus and the Local Majority Rule. May 2000. 38 pp.

RS-00-7 Lars Arge and Jakob Pagter. I/O-Space Trade-Offs. April 2000. To appear in 7th Scandinavian Workshop on Algorithm Theory, SWAT ’98 Proceedings, LNCS, 2000.

RS-00-6 Ivan B. Damgård and Jesper Buus Nielsen. Improved Non-Committing Encryption Schemes based on a General Complexity Assumption. March 2000. 24 pp.