Hardness results for weak bisimilarity of simple process algebras

Jitka Stříbrná LFCS, Department of Computer Science University of Edinburgh, UK email: js@dcs.ed.ac.uk

We do not know whether weak bisimilarity (denoted ≈) is decidable for general BPA and BPP but we may try to estimate what would be a least complexity of a decision procedure that might exist. That is achieved by taking problems complete for some complexity classes and reducing them to ≈. In this way we will show that the problem of deciding weak bisimilarity would be NP-hard for BPP, and PSPACE-hard for BPA.

1 Background

There has been much effort devoted to the study of decidability of various bisimulation equivalences for many process calculi. The majority of the results concern strong bisimilarity which was shown to be decidable for the two classes of Basic process algebras (BPA)

[2] and Basic parallel process algebras (BPPA) [1] that we will be considering in this paper. However, we want to focus our attention on a more interesting notion of observation

that is weak bisimilarity. So far, the decidability of weak bisimilarity for the subclass of totally normed BPP and BPA was established in [5], and a semidecision procedure for weak bisimilarity of BPP was manifested in [3]. The question for general BPA and BPP remains open, however we may at least try to establish some lower bounds on a decision procedure that might exist.

Decidability of bisimulation equivalences so far seems to be consistent with polynomialtime decision procedures. Polynomial algorithms deciding strong bisimilarity for normed BPP and BPA were manifested in [6], [7], [8], and even though there is no polynomial decision procedure for the class of all BPP and BPA, there is no lower bound that contradicts its existence. It would be a weak negative result to show that weak bisimilarity cannot be decidable in polynomial time. To our best knowledge even this weak result hasn’t been proved yet, however in this paper we provide a strong evidence that the problem of deciding weak bisimilarity cannot be solved in polynomial time. More specifically, we will show that for weak bisimilarity and (totally normed) BPP and BPA the decision problem is at least NP-hard and for general BPA, at least PSPACE-hard.

Before we proceed to demonstrate these claims we will recall the necessary notions from process algebra and computational complexity.

We will start with the process algebras. We presuppose a fixed set of actions Act = {a, b, c, …} that contains a special silent action τ, and a finite set of process variables or atoms Σ = {X_{1}, …, X_{n}}. Then we say that a basic process algebra or BPA is a pair (Σ^{∗}, Δ) where Σ^{∗} is the free monoid generated by Σ, and Δ = {X ⟶^{α} P | X ∈ Σ, P ∈ Σ^{∗}, α ∈ Act} is a finite set of transitions. We call words from Σ^{∗} BPA-processes. The transition rules of Δ determine a transition relation on general BPA-processes in this way:

XQ ⟶^{α} P Q if there is a rule X ⟶^{α} P in Δ

A basic parallel process algebra or BPPA is a pair (Σ̂, Δ), where Σ̂ = {X_{1}^{i_{1}} … X_{n}^{i_{n}} | i_{1}, …, i_{n} ∈ ℕ} is the commutative algebra generated by Σ, and Δ = {X ⟶^{α} P | X ∈ Σ, P ∈ Σ̂, α ∈ Act} is a finite set of transitions. We call multisets from Σ̂ basic parallel processes or BPP. In the algebra Σ̂ there is a natural operation which we shall call parallel composition and denote with ∥:

P ∥ Q = X_{1}^{i_{1}+j_{1}} … X_{n}^{i_{n}+j_{n}}, where P ≡ X_{1}^{i_{1}} … X_{n}^{i_{n}} and Q ≡ X_{1}^{j_{1}} … X_{n}^{j_{n}}.

We can extend the rules of Δ to all BPP in the obvious way:

P ∥ X ∥ Q ⟶^{α} P ∥ R ∥ Q if there is a rule X ⟶^{α} R in Δ

For both BPA and BPPA we use capital letters X, Y to range over process variables and P, Q, R to range over processes.

A process variable X is said to be totally normed if there is no transition X ⟶^{τ} ϵ and if there exists a derivation X ⟹^{s} ϵ for some non-empty sequence of actions s. A process algebra is totally normed if all its variables are totally normed.

Now we will introduce the concepts of strong and weak bisimilarity. We say that a binary relation R over pairs of processes is a strong bisimulation relation if the following condition holds for every pair (P, Q) from R and every action α from Act:

• for every P ⟶^{α} P′ there exists Q ⟶^{α} Q′ so that (P′, Q′) ∈ R

• for every Q ⟶^{α} Q′ there exists P ⟶^{α} P′ so that (P′, Q′) ∈ R

Two processes P and Q are strongly bisimilar if there exists a strong bisimulation relation containing the pair (P, Q). The union of all bisimulation relations gives rise to the maximal bisimulation which is denoted by ∼.

A weak bisimulation relation is defined analogously as a strong bisimulation relation with the single transitions ⟶^{α} being replaced with ⟹^{α}, where ⟹^{α} is an abbreviation of (⟶^{τ})^{∗} ⟶^{α} (⟶^{τ})^{∗} in case of α ≠ τ and (⟶^{τ})^{∗} in case of α = τ. Then we say that processes P and Q are weakly bisimilar if there exists a weak bisimulation relation containing the pair (P, Q). There also exists a maximal weak bisimulation relation which is obtained as a union of all weak bisimulation relations and it is denoted by ≈.

Now we will recall some notions from computational complexity (consult [4], [9] and [11] for more details). Informally, we say that a problem P is C-hard for some complexity class C if to solve P is as difficult as to solve any problem from C. If on top of that we know that the complexity of solving P is C, in other words P belongs to C, we say that P is C-complete. Often when we try to estimate a lower bound on a complexity of some problem P we transform another problem P′ to P where we know the complexity of P′ already. For this purpose we use the concept of reduction.

Assume two languages L_{1} over some alphabet Σ_{1} and L_{2} over an alphabet Σ_{2}. A reduction from L_{1} to L_{2} is a function f from Σ_{1}^{∗} to Σ_{2}^{∗} such that

for all w ∈ Σ_{1}^{∗}, w ∈ L_{1} ⟺ f(w) ∈ L_{2}.

When reducing one problem to another we need a function that can be efficiently computed. As we will see later, it suffices for the reduction f to be polynomial time, that is we can construct a polynomial-time bound Turing machine that computes the function f. We will denote the fact that L_{1} is polynomial-time reducible to L_{2} by L_{1} ⋞ L_{2}.

We say that a language L is complete for a class C (with respect to polynomial-time reduction) if L is in C and every language in C is reducible to L. A language L is hard for C (wrt polynomial-time reduction) if every language in C is reducible to L, but L is not necessarily in C. The complexity classes that we will be dealing with are the classes NP and PSPACE. The following theorem [9] confirms that polynomial-time reduction is suitable for our purposes.

Lemma 1 If L′ ∈ P and L ⋞ L′ then also L ∈ P, where P is the class of problems that can be solved in polynomial time.

2 Weak bisimilarity of BPP is NP-hard

There is a plethora of known problems that fall into the class of NP-complete problems. We need to choose a problem that is in some way related to the principle of bisimilarity. Clearly, any two processes that are bisimilar must be capable of performing sequences of actions of identical lengths therefore we will reduce a ‘counting’ problem to weak bisimilarity.

One problem that suits our purpose is Knapsack which reads as follows: given a sequence of values m_{1}, m_{2}, …, m_{n} and a total t, we want to find out whether we can choose a subsequence m_{i_{1}}, …, m_{i_{k}} that adds up to t. That brings us to the idea of having two processes, one simulating the total t by being defined as a trace of the length of t, and the other simulating the choices of subsequences of m_{1}, m_{2}, …, m_{n} and hence being equivalent to a tree whose branches correspond to traces of lengths specified by the individual subsequences.

Knapsack is known to be NP-complete (cf. [4], [11]) and we will demonstrate a polynomial-time reduction to weak bisimilarity of basic parallel processes. As we have explained earlier that will establish that the problem of deciding ≈ for BPP is at least NP-hard. The formal definition of Knapsack is as follows:

Definition 2 Knapsack is the following problem:

Instance: t, m_{1}, m_{2}, …, m_{n} ∈ ℕ

Question: ∃i_{1}, i_{2}, …, i_{n} ∈ {0, 1}. ∑_{j=1}^{n} i_{j}m_{j} = t?

The fact that this simple problem is NP-complete is due to the fact that there may occur arbitrarily large numbers on the input. If we consider the input encoded in unary then we can find an algorithm that solves Knapsack in time polynomial in size of the input. The possibility of arbitrarily large values of m_{i} or t will require a trick in the definition of processes so that we remain within the limits of polynomial-time reduction. We will now proceed to demonstrate a polynomial time many-one reduction. of Knapsack to weak bisimilarity of BPP.

Lemma 3 Knapsack ⋞ ≈.

Proof: Let t, m_{1}, m_{2}, …, m_{n} ∈ ℕ be an instance of Knapsack. We will demonstrate two basic parallel processes P and Q such that there exist i_{1}, i_{2}, …, i_{n} ∈ {0, 1} with ∑_{j} i_{j}m_{j} = t if and only if P ≈ Q. Following the afore mentioned idea, the process P will simulate branching defined by individual subsequences, and the process Q will simulate the trace of length t. For the purpose of counting we will use a single visible action a that will help us to test if there is a branch in the tree defined by P of length t, ie. equivalent with Q.

For each m_{j}, resp. t, we will introduce a process variable M_{j}, resp. T, that will be able to perform exactly a sequence of ⟹^{a} transitions of length m_{j}, resp. t. The process P then will be capable of generating any subset of {M_{1}, …, M_{n}} whereas the process Q will be able to evolve into T. Finally we will demonstrate that P is weakly bisimilar to Q if and only if the answer to the respective instance is yes. Now we will present the transition rules that define the process variables P and Q:

\begin{aligned}P ⟶^{τ} P_{1} ∥ … ∥ P_{n} & Q ⟶^{τ} P & P_{j} ⟶^{τ} M_{j}, j = 1, …, n \\ & Q ⟶^{τ} T & P_{j} ⟶^{τ} ϵ, j = 1, …, n \end{aligned}

In order to complete the definitions of P and Q we have to define process variables M_{j} and T. Our only concern is that the resulting reduction is polynomial time hence we have to use a little trick in the definition. We define a sequence of variables S_{0}, S_{1}, …, S_{k} in this way:

S_{0} ⟶^{a} ϵ, S_{i+1} ⟶^{τ} S_{i} ∥ S_{i} for i < k, where k is taken to be ⌊log(max{t, m_{1}, …, m_{n}})⌋.

Thus we have obtained variables such that S_{i} ≈ a^{2^{i}}, where we use the expression a^{m} in the obvious meaning. Now we can define T ⟶^{τ} S_{k}^{e_{k}} ∥ … ∥ S_{1}^{e_{1}} ∥ S_{0}^{e_{0}} where e_{k} … e_{1}e_{0} is the binary encoding of t. The variables M_{0}, …, M_{n} are defined in a similar fashion: M_{j} ⟶^{τ} S_{k}^{e_{kj}} ∥ … ∥ S_{1}^{e_{1j}} ∥ S_{0}^{e_{0j}}, where e_{kj} … e_{0j} is the binary encoding of m_{j}, for j = 1, …, n. To summarise, we only need k + 1 extra variables in order to define the processes T and M_{j}.

It is easily seen from the construction that P can only perform sequences of ⟹^{a} transitions of length ∑_{j} i_{j}m_{j} for some i_{1}, i_{2}, …, i_{n} ∈ {0, 1}. Therefore if this sum never adds up to t the process Q can become T and thus force non-bisimilarity with P. On the other hand, if there exist i_{1}, i_{2}, …, i_{n} ∈ {0, 1} such that ∑_{j} i_{j}m_{j} = t the process P will generate the composition M_{1}^{i_{1}} ∥ … ∥ M_{n}^{i_{n}} as an answer to the move Q ⟶^{τ} T and preserve weak bisimilarity. If it is P that takes the initiative then the process Q simply makes use of the rule Q ⟶^{τ} P and then copies any move of P. □

It is quite easy to verify that the actual reduction can be carried out in polynomial time, however we will not present the full details of the reduction here. We can finally conclude with the following theorem:

Theorem 4 The decidability of weak bisimilarity of basic parallel processes is NP-hard.

We have to remark that the result we have just presented seems rather unimportant since we do not know whether weak bisimilarity of BPP is decidable at all. We can however adjust the reduction for the subclass of totally normed BPP. That means we have to get rid of zero-normed processes that are present in the process algebra constructed above. The problematic processes are P_{i} since they have at their disposal the transition rules P_{i} ⟶^{τ} ϵ. However, we can change the instance of Knapsack slightly in order to dispose of such processes. We can consider the instance ∑ i_{j}m_{j} + ∑ m_{j} = t + ∑ m_{j} to which the answer is ‘yes’ if and only if the answer to the original instance is ‘yes’. That means a shift in the required values of i_{j} from i_{j} ∈ {0, 1} to i_{j} ∈ {1, 2} which is expressed in terms of the transitions as P_{i} ⟶^{τ} M_{i} ∥ M_{i}, P_{i} ⟶^{τ} M_{i}, and we also need to alter the definition of Q to Q ⟶^{τ} T ∥ M_{1} ∥ … ∥ M_{n}. This change doesn’t have any impact on the size of the reduction as it can still be done in polynomial time. Hence we have removed all zero-norm processes and we can assert that ≈ is NP-hard even for totally normed processes.

Theorem 5 The decidability of weak bisimilarity of totally normed basic parallel processes is NP-hard.

3 Weak bisimulation of BPA is PSPACE-hard

When we look carefully at the reduction of Knapsack onto weak bisimulation of BPP we can see that it could be easily modified into a reduction to weak bisimulation of BPA. There are these transition rules which contain parallel composition - the definitions of P and each M_{j} and T (and the auxiliary variables S_{i}). However, in the whole process algebra there is only a single visible action which is a and, moreover, the process variables M_{1}, …, M_{n} and T each determine a single string of ⟹^{a} moves with no available branching. Therefore it doesn’t make any difference to compose such processes in the sequential or parallel fashion. The final improvement when we remove all zero-norm processes also works for BPA and hence we come to the conclusion that deciding weak bisimilarity for totally normed BPA is NP-hard.

Sequential composition, however, enables us to go even further. With the sequential structure of BPA-processes we are able to encode finite automata and hence achieve a stronger result. We will use the totality problem for finite automata Tot which is PSPACEcomplete and construct a polynomial time reduction onto weak bisimilarity of BPA. Thus we will show that this problem is at least PSPACE-hard. First we will define the totality problem for finite automata:

Definition 6 Tot is the following problem:

Instance: A nondeterministic finite automaton A over some alphabet Σ.

Question: Is L(A), the language accepted by A, equal to the total language Σ^{∗}?

This problem is PSPACE-complete even a two-letter alphabet (cf. [4]) hence in the following we will assume that Σ = {a, b}. We will in fact demonstrate a linear time reduction of Tot onto weak bisimilarity of BPA.

Theorem 7 Tot ⋞ ≈.

Now we will explain the main idea behind the reduction. We presuppose a nondeterministic finite automaton A = (Σ, Q, δ, q_{0}, {q_{k}}), where Σ = {a, b} is the input alphabet, Q = {q_{0}, q_{1}, …, q_{k}} is the set of states with q_{0} being the initial and q_{k} the final states, and δ : Q × Σ → 2^{Q} is the transition function. We will write (q_{i}, x) ⟼ q_{j} to express the fact that the state q_{j} belongs to the set δ(q_{i}, x) with x being either a or b. Also note that wlog we can assume a single final state q_{k}.

We will simulate words over {a, b} by introducing two variables A and B such that A can only perform the transition A ⟶^{a} ϵ and B can only perform the transition B ⟶^{b} ϵ. Then any process over A and B will determine a single word from the alphabet Σ. To simulate the total language Σ^{∗} we will introduce a process P that will be capable of producing any string of atoms A and B. Next we would like to define a process Q that can generate all strings from L(A). However since we are only allowed the leftmost derivation in case of BPA-processes, we will define a process that generates exactly all the reverse words from L(A). Still, we will be able to show that L(A) = Σ^{∗} if and only if P ≈ Q.

For each state q_{0}, q_{1}, …, q_{k} of the automaton A we define a variable Q_{0}, Q_{1}, …, Q_{k} using the following rules:

if (q_{i}, a) ⟼ q_{j} then Q_{i} ⟶^{τ} Q_{j}A, and if (q_{i}, b) ⟼ q_{j} then Q_{i} ⟶^{τ} Q_{j}B.

For the variable Q_{k} that corresponds to the final state q_{k} we add a special rule Q_{k} ⟶^{s} ϵ, where s is a special initial action. The purpose of s is to synchronise the two processes P and Q. Finally, we put Q = Q_{0}. It is quite straightforward to observe that a word w is in L(A) if and only if we can via a τ sequence from the variable Q generate the process Q_{k}R where R ∈ {A, B}^{∗} and there is a unique transition sequence R ⟶^{w̄} ϵ with w̄ being the reverse of w.

To complete the reduction it remains to define the process P whose task is to be able to generate all strings from {A, B}^{∗} and simulate the process Q, and the variables A, resp. B, that simulate the letters a, resp. b.

\begin{matrix}P ⟶^{τ} QT & P ⟶^{τ} PA & A ⟶^{a} ϵ & T ⟶^{τ} T \\ P ⟶^{s} ϵ & P ⟶^{τ} PB & B ⟶^{b} ϵ \end{matrix}

For technical reasons we need a process that will block any sequence of variables that the process P may have generated. The process T forms such a block since it is defined as a τ loop and therefore it is clear that T R ≈ ϵ for any process R. The presence of T in the algebra means that the algebra fails to be totally normed which opens the question about the complexity of weak bisimilarity for totally normed processes. The final step is to show the correctness of the reduction.

Theorem 8 Assume a given automaton A and P and Q defined as above. Then L(A) = {a, b}^{∗} iff P ≈ Q.

Proof: One implication is straightforward. Assume that L(A) ≠ {a, b}^{∗} and let w ∈ {a, b}^{∗} \ L(A). Since P is constructed to generate all strings of a and b it can produce a sequence of variables capable of performing the word sw^{R}. However, as Q simulates the automaton A it cannot produce this string and thus P ≉ Q.

In order to show the other direction we need to analyze the moves of P and Q. The idea is that P will wait for Q to make a move and then respond by doing P ⟶^{τ} QT which blocks anything which P may have generated in the meantime. Clearly Q ≈ QT R for any process R because we can never get past T. On the other hand, Q has to respond only when P decides to generate a sequence of A’s and B’s and then disappear. Hence the responses of Q are:

1. P ⟹^{τ} P R, R ∈ {A, B}^{∗} - in this case Q does the empty sequence Q ⟹^{ϵ} Q

2. P ⟹^{τ} QT R, R ∈ {A, B}^{∗} - in this case Q ≈ QT R and hence again the response is

Q ⟹^{ϵ} Q

3. P ⟹^{s} R, R ∈ {A, B}^{∗} - since Q can generate all strings over the alphabet {A, B} it will be able to generate the process R via ⟹^{s}.

Although this analysis is quite informal we could easily construct a binary relation as a union of three binary relations, each corresponding to one case of the above analysis, and verify that it is a weak bisimulation relation. That only requires to test that it is closed under expansion with ⟶^{α} which would again follow the structure of the proof. Therefore we have P and Q weakly bisimilar. Finally, we can conclude that the automaton generates the total language if and only if the processes P and Q are weakly bisimilar. □

It is not difficult to check that this construction can be done in time linear in the size of the input automaton as for each possible transition of the input automaton we construct a single rule of the process algebra and also the number of states only increases by a constant. Therefore we can conclude that the problem of deciding weak bisimilarity for BPA is PSPACE-hard.

4 Conclusion

We cannot draw any strong conclusions from the results presented in this paper. Although weak bisimilarity seems a rather complex notion and hence we might hope to prove that if indeed it was decidable for BPA and BPP, the complexity of a decision procedure would be rather high, there seem to be obstacles that prevent us from doing so. The idea of the Knapsack reduction to weak bisimilarity of BPP may be applied to more complex problems; one of them might be the verification of Presburger sentences which is known to require at least doubly exponential space.

To conclude this paper, we can draw the following comparisons: for strong bisimulation and normed BPP and BPA there exist polynomial decision procedures. When we move to totally normed BPP and BPA, for which weak bisimulation is decidable, the problem of deciding weak bisimilarity is NP-hard (which is to be expected since we are dealing with a more intricate notion). For general BPA-processes, if weak bisimilarity was decidable then the decision problem would be PSPACE-hard.

Acknowledgement

I would like to thank my advisor Mark Jerrum for suggesting this line of research and for helpful discussions throughout my work on the results presented in this paper.

References

[1] Christensen S., Hirshfeld Y. and Moller F. Bisimulation Equivalence is Decidable for Basic Parallel Processes, in Proceedings of CONCUR 93, LNCS 715, 143– 157, 1993.

[2] Christensen S., Hüttel H. and Stirling C. Bisimulation equivalence is decidable for all context-free processes, in Proceedings of CONCUR 92, LNCS 630, 138– 147, 1992.

[3] Esparza J. Petri nets, commutative context-free grammars and basic parallel processes. In Fundamentals of Computation Theory 95, LNCS 965, Springer Verlag, 221–232, 1995.

[4] Garey M.R. and Johnson D.S. Computers and Intractability: A Guide to the Theory of NP-completness. Freeman, San Francisco, 1979.

[5] Hirshfeld Y. Bisimulation Trees and the Decidability of Weak Bisimulations. Draft of a paper.

[6] Hirshfeld Y., Jerrum M. and Moller F. A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. In LFCS Report Series, University of Edinburgh, 1994.

[7] Hirshfeld Y., Jerrum M. and Moller F. A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. In Math. Struct. in Comp. Science 6, 251–259, Cambridge University Press, 1996.

[8] Hirshfeld Y., Jerrum M. and Moller F. A polynomial algorithm for deciding bisimilarity of normed context-free processes. In LFCS Report Series, University of Edinburgh, 1994.

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

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

[11] Papadimitriou C.H. Computational Complexity. Addison-Wesley, 1994.