Decidability of Strong Bisimulation of Basic Parallel Processes using Hilbert’s Basis Theorem

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

We will apply some algebraic results, namely Hilbert’s basis theorem and Gröbner bases, to get a different technique for proving decidability of strong bisimulation of basic parallel processes.

1 Introduction

Basic Parallel Processes (BPP) were introduced by Christensen in his PhD. dissertation [2] as a very natural subclass of CCS processes. The decidability of strong bisimulation for BPP was first proved for a special case of normed processes in [3]. Later improvement is a polynomial decision procedure [8]. Decidability for general, unnormed BPP was demonstrated in [2], [4], [7]. In this case, there is not even a primitive recursive upper bound on the procedure.

The approach described in this paper is a new, shorter decision procedure for the general case. We hope that it might give better complexity bounds and also it might extend to situations not covered by existing decidability results (eg. weak bisimulation).

2 Preliminaries

In this section we give all the basic definitions, namely a Basic Parallel Process and strong bisimulation for the process algebra part and an ideal and a basis of an ideal for the algebraic part. Then we will show how we can relate them and use some algebraic results to obtain a new decision procedure. We will start with the process algebra.

We presuppose a fixed set of actions Act = {a, b, c, …} and a finite set of variables Σ = {X_{1}, …, X_{n}}.

A basic parallel process algebra is a pair (Σ̂, Δ), where Σ̂ = {X_{1}^{i_{1}} … X_{n}^{i_{n}} | i_{1}, … i_{n} ∈ N} is the commutative algebra generated by Σ and Δ = {X ⟶^{α} P | X ∈ Σ, P ∈ Σ̂, α ∈ Act} is a finite set of transitions. We call elements of Σ̂ basic parallel processes or BPP and we use capital letters P, Q, R to range over BPP.

We define a (binary) operation on Σ̂ that we call parallel composition: 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}}. Since we only work with parallel composition in this paper we will leave out the symbol ∥ and write P Q for P ∥ Q. We can extend the rules of Δ to all BPP in the obvious way:

PXQ ⟶^{α} PRQ if there is a rule X ⟶^{α} R in Δ.

A binary relation R over Σ̂ is called a strong bisimulation if for every (P, Q) ∈ R, for every α ∈ Act

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

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

We say that P and Q are strongly bisimilar if there is a strong bisimulation containing the pair (P, Q). The union of all strong bisimulation relations is in fact a strong bisimulation relation itself and also the largest such relation. It is denoted by ∼.

For the algebraic part we start with the two-element field F_{2} = ({0, 1}, +, ·) and the polynomial ring F_{2}[x_{1}, …, x_{n}], where the variables x_{1}, …, x_{n} are meant to correspond to the basic parallel process algebra variables (Σ). Polynomials of the form x_{1}^{i_{1}} … x_{n}^{i_{n}}, where i_{1}, …, i_{n} ∈ N, are called power products. Capital letters P, Q, R, S range over power products, small letters p, q, r range over polynomials.

We say that a nonempty subset I of F_{2}[x_{1}, …, x_{n}] is an ideal if

(i) p_{1}, p_{2} ∈ I ⟹ p_{1} + p_{2} ∈ I

(ii) p ∈ I ⟹ ∀λ ∈ F_{2}[x_{1}, …, x_{n}]. λp ∈ I

If A = {p_{j} | j ∈ J} is a subset of F_{2}[x_{1}, …, x_{n}] then the ideal generated by A is defined to be Id(A) = {∑ λ_{i}p_{i} | λ_{i} ∈ F_{2}[x_{1}, …, x_{n}], p_{i} ∈ A}, the set of all finite sums over elements of F_{2}[x_{1}, …, x_{n}]. We say that a subset A ⊆ F_{2}[x_{1}, …, x_{n}] is a basis of an ideal I if A generates I, that is I = Id(A).

Now we fix Σ and Δ and explain how the algebraic idea can be applied to strong bisimulation of basic parallel processes. We have a set of variables {x_{1}, …, x_{n}} that corresponds to Σ. Power products over F_{2}[x_{1}, …, x_{n}] correspond to Basic Parallel Processes and multiplication of power products corresponds to parallel composition of BPP. Since power products and Basic Parallel Processes are intuitively so closely related they will be freely interchanged in the following text.

We can express the largest bisimulation relation ∼ in terms of polynomials as the set B_{∼} = {P + Q | P ∼ Q}. B_{∼} is an infinite set and so we cannot effectively check the membership in a straightforward way. However, using some algebraic tools such as decidability of membership in polynomial ideals [6], [13] and Hilbert’s basis theorem we will be able to devise a finite condition for the membership check in B_{∼}. We are going to use the following theorem [10], [12]:

Hilbert’s basis theorem: (HBT)

If R is a field or the ring of integers, then any ideal in the polynomial ring R[x_{1}, …, x_{k}] has a finite set of generators.

The way to proceed is to take the ideal generated by B_{∼}, denoted here by I_{∼}. HBT guarantees that there is a finite set of polynomials B generating I_{∼}, that is I_{∼} = Id(B). We will show that I_{∼} doesn’t contain any two-term polynomials other than B_{∼} and finally we devise a finite Caucal-like condition for membership in I_{∼} which will be shown decidable using Gröbner bases [13]. The process algebra (Σ̂, Δ), the polynomial ring F_{2}[x_{1} … x_{n}], B_{∼} and I_{∼} remain fixed for the rest of the paper.

3 Main Results

Caucal in his paper [1] stated a condition that enables us to check when a set generates a bisimulation relation. This idea has been exploited for instance in [7]. We are going to use a similar idea here and so we will call it a Caucal-like condition (CC). This condition refers to finite sets of polynomials (bases) and will allow us to recognise when a given ideal represents a bisimulation. We will also show that it is enough to consider special cases of bases.

Let B be an arbitrary (finite) set of polynomials. We say that CC(B) if for all P +Q ∈ B for every α ∈ Act

• for all P ⟶^{α} P′ there exists Q ⟶^{α} Q′ with P′ + Q′ ∈ Id(B) and

• for all Q ⟶^{α} Q′ there exists P ⟶^{α} P′ with P′ + Q′ ∈ Id(B),

where Id(B) is the ideal generated by the (finite) set B. This condition only applies to two-term polynomials from B.

For the set B_{∼} defined above the elements of the polynomial ideal I_{∼} have special properties which is expressed in the following theorem. Firstly we will show that an ideal generated by a set A can be also defined inductively, as follows:

Lemma: For every set A ⊆ F_{2}[x_{1}, …, x_{n}] the polynomial ideal Id(A) = I(A), where I(A) is defined in the following way:

I_{0}  = A
I_{i+1} = I_{i} ∪ {p + q | p, q ∈ I_{i}} ∪ {P · p | p ∈ I_{i}, P a power product in F_{2}[x_{1}, …, x_{n}]}
I(A) = ⋃_{i∈ω} I_{i}

Proof: The proof is straightforward since a multiplication of two polynomials p and q can be replaced by a sum of products of power products of p with q, and finite sums of polynomials can be replaced by binary sums. □

Proposition 1: Let p be a polynomial. Then p ∈ I_{∼} if and only if there exist power products P_{1}, …, P_{k}, Q_{1}, …, Q_{k} such that p = P_{1} + Q_{1} + … + P_{k} + Q_{k} and P_{j} ∼ Q_{j} for all 1 ≤ j ≤ k.

Proof: We are going to use the inductive construction of I_{∼} as in the above Lemma with I_{0} = B_{∼}. One implication is easy. If a polynomial p can be expressed as P_{1} + Q_{1} + … + P_{k} + Q_{k} and P_{j} ∼ Q_{j} for all j then P_{j} + Q_{j} belong to B_{∼} = I_{0} and hence p will certainly be in I_{k}.

The other direction will be proved by induction on I_{i}.

1. p ∈ I_{0} iff p ∈ B_{∼} iff p = P + Q and P ∼ Q.

2. p ∈ I_{i+1} if and only if p ∈ I_{i} or p = q + r with q, r ∈ I_{i} or p = Rq where q ∈ I_{i} and R is a power product. The case of p ∈ I_{i} is trivial so the proof falls into two parts:

2.1. Assume p = q + r, where q = P_{1} + Q_{1} + … + P_{k} + Q_{k} with P_{j} ∼ Q_{j} and r = R_{1} + S_{1} + … + R_{l} + S_{l} with R_{j} ∼ S_{j}. The polynomial p can be expressed as U_{1} + V_{1} + … + U_{m} + V_{m}, where each sum U_{i} + V_{i} is either some P_{j} + Q_{j} or R_{h} + S_{h}, in which case by induction hypothesis U_{i} ∼ V_{i}, or it arises from some P_{j} + Q_{j} and R_{h} + S_{h} in the way that either P_{j} = R_{h} or P_{j} = S_{h} or Q_{j} = R_{h} or Q_{j} = S_{h}.

Assume that P_{j} = R_{h} and thus U_{i} + V_{i} = Q_{j} + S_{h}. As P_{j} ∼ Q_{j} and R_{h} ∼ S_{h} then by the transitivity of ∼ also Q_{j} ∼ S_{h}. All the other cases are symmetrical.

2.2. Assume p = Rq, where q = P_{1} + Q_{1} + … + P_{k} + Q_{k}, P_{j} ∼ Q_{j}. Then p = RP_{1} + RQ_{1} + … + RP_{k} + RQ_{k} and because strong bisimulation is closed under parallel composition also RP_{j} ∼ RQ_{j} for all j. That concludes the proof. □

By generating B we aim at the ideal I_{∼} and so we can assume that B only consists of two-term polynomials: if there is a polynomial with more than two terms (has to be of an even length) in B then, as it also belongs to I_{∼}, it has to be of the form P_{1}+Q_{1}+…+P_{k}+Q_{k} with P_{j} ∼ Q_{j} (Proposition 1). It follows from the definitions of B_{∼} and I_{∼} that all sums P_{j} + Q_{j} are in I_{∼}. Hence we can replace the polynomial in B with the two-element sums.

If P and Q are bisimilar then P + Q certainly belongs to B_{∼}. On the other hand, there might be a smaller bisimulation relation which contains (P, Q). We do not have any means of checking whether a set B generates the largest relation but we can find out when the subset of two-term polynomials of an ideal I corresponds to a bisimulation. That is captured in the following condition which will be denoted by CC′(I):

Every p ∈ I can be expressed as P_{1} + Q_{1} + … + P_{k} + Q_{k} such that P_{j} + Q_{j} ∈ I for all 1 ≤ j ≤ k, and for all α

• for all P_{j} ⟶^{α} P′_{j} there is Q_{j} ⟶^{α} Q′_{j} such that P′_{j} + Q′_{j} ∈ I and

• for all Q_{j} ⟶^{α} Q′_{j} there is P_{j} ⟶^{α} P′_{j} such that P′_{j} + Q′_{j} ∈ I

Clearly if CC′(I) for an ideal I then the set {(P, Q) | P +Q ∈ I} is a strong bisimulation. This condition doesn’t have to be finite and applies to all elements of a given ideal, as opposed to pairs P + Q in the case of CC.

Obviously, if CC′ holds for an ideal Id(B) then also CC holds for the basis B. The other direction is true as well which is stated in the following proposition:

Proposition 2: CC(B) ⟹ CC′(Id(B)).

Proof: We can assume that the ideal Id(B) is defined inductively with I_{0} = B. The proof is done by induction on i.

1. I_{0} = B and the condition corresponds to CC(B)

2. p ∈ I_{i+1} if and only if p ∈ I_{i} or p = q + r with q, r ∈ I_{i} or p = Rq with q ∈ I_{i} and R a power product. The case of p ∈ I_{i} is trivial and we will consider the two following cases:

2.1. Assume that p = q+r, where q = P_{1}+Q_{1}+…+P_{k} +Q_{k}, r = R_{1}+S_{1}+…+R_{l}+S_{l} and q and r satisfy the claim. p = U_{1} + V_{1} + … + U_{m} + V_{m}, where each U_{i} + V_{i} is either some P_{j} + Q_{j} or R_{h} + S_{h}, in which case we can apply the induction hypothesis, or U_{i} + V_{i} arises from some P_{j} + Q_{j} and R_{h} + S_{h} so that either P_{j} = R_{h} or P_{j} = S_{h} or Q_{j} = R_{h} or Q_{j} = S_{h}.

Assume that P_{j} = R_{h} and U_{i} + V_{i} = Q_{j} + S_{h}. If U_{i} = Q_{j} ⟶^{α} U then by IH P_{j} ⟶^{α} P so that U + P ∈ Id(B). As P_{j} = R_{h} there has to be a move S_{h} = V_{i} ⟶^{α} S such that P + S ∈ Id(B). As the ideal Id(B) is closed under addition then both U_{i} + V_{i} = Q_{j} + S_{h} and U + S ∈ Id(B). Moves of V_{i} and all the other cases are symmetrical.

2.2. Assume that p = Rq, q ∈ I_{i}.

We may assume that q = P_{1} + Q_{1} + … + P_{k} + Q_{k} so that all P_{j} + Q_{j} ∈ Id(B). Let p = P′_{1} + Q′_{1} + … + P′_{k} + Q′_{k} = RP_{1} + RQ_{1} + … + RP_{k} + RQ_{k}. Since all P_{j} + Q_{j} ∈ Id(B) then also all RP_{j} + RQ_{j} ∈ Id(B) and hence it remains to check the moves:

P′_{j} ⟶^{α} P′: P′_{j} = RP_{j} so either R makes a move R ⟶^{α} R′ and P′ = R′P_{j} or P_{j} makes a move P_{j} ⟶^{α} P and P′ = RP. In the former case we use the fact that P_{j} + Q_{j} ∈ Id(B_{0}) hence also R′P_{j} + R′Q_{j} ∈ Id(B).

In the latter case by IH there is a corresponding move Q_{j} ⟶^{α} Q so that P + Q ∈ Id(B) and since Id(B) is closed under multiplication also RP + RQ ∈ Id(B). Similarly for moves of Q′_{j}. □

4 Semidecision Procedure

Before we describe the decision procedure we will show the semi-decidability of strong bisimulation for BPP. This in fact suffices to demonstrate decidability as BPP are imagefinite processes and for the class of image-finite processes we can easily construct a semidecision procedure for non-bisimilarity [2].

The following is a semidecision procedure that stops and gives a positive answer if and only if the two input BPP P and Q are strongly bisimilar:

1. Put B = {P + Q}.

2. Check whether CC(B).

3. If the condition holds then output P ∼ Q else enumerate another finite set B containing the sum P + Q and go to 2.

We will show that the semidecision procedure is correct.

Assume we are given a pair of processes P, Q such that P ∼ Q. Then P + Q is contained in the set B_{∼}. By Hilbert’s basis theorem, the ideal I_{∼} is generated by some finite set B. It is easy to see that CC′(I_{∼}) and hence also CC(B) for any finite basis B of I_{∼}. The Caucal-like condition can be verified since checking it for B means checking ideal membership finitely many times and ideal membership is decidable using Gröbner bases [13]. We can effectivelly generate all finite sets so eventually we will generate this B, verify that CC(B) and output P ∼ Q.

Assume we are given a pair of processes P, Q such that P ≁ Q. That means there is no bisimulation relation containing the pair (P, Q). We generate B so that it contains the sum P + Q. Therefore the Caucal-like condition will always fail for B because otherwise by Proposition 2 Id(B) would correspond to a bisimulation relating P and Q. Hence the procedure will never give a positive answer in the case of non-bisimilarity.

5 Decision Procedure

The principle of the decision procedure is to start from the set consisting of the input pair P + Q and gradually construct a finite basis of a bisimulation (if P and Q are bisimilar) by adding new pairs, appropriate derivatives of P and Q. This approach is closely related to Hirshfeld’s bisimulation trees [7]. The finiteness of this approach is guaranteed by the finite branching of BPP and the fact that every increasing chain of ideals has a finite length (Theorem 1).

To make the decision procedure more concise we will introduce the following notation. If ¬CC(B) then there exists P + Q ∈ B, α and P ⟶^{α} P′ such that for all Q ⟶^{α} Q′ P′ + Q′ ∉ Id(B) and we will say that CC fails on P + Q. We put

• F(B) = {P + Q ∈ B | CC fails on P + Q} and for P + Q ∈ F(B) and an action α we define

• P(P + Q, α) = {P′ | P ⟶^{α} P′ ∧ ∀Q ⟶^{α} Q′. P′ + Q′ ∉ Id(B)}

• Q(P + Q, α) = {Q′ | Q ⟶^{α} Q′ ∧ ∀P ⟶^{α} P′. P′ + Q′ ∉ Id(B)}

Now we can proceed to the decision procedure:

1. Input a pair P, Q.

2. Put B = {P + Q}.

3. Check CC(B).

If CC(B) then CC′(Id(B)) and so Id(B) represents a bisimulation relating P and Q, hence stop with a positive reply.

If ¬CC(B) then go to 4.

4. If there is a pair P + Q ∈ F(B) such that P ≁_{1} Q then stop else for every pair P + Q from F(B) define a set B(P + Q) in this way:

for every failed α define P_{α} = {P′ | P ⟶^{α} P′} and Q_{α} = {Q′ | Q ⟶^{α} Q′}.

Put

B_{α} = B ∪ ⋃_{P′∈P(P +Q,α)}(P′ + Q′) ∪ ⋃_{Q′∈Q(P +Q,α)}(P′ + Q′),

where all Q′, resp. P′, are taken from Q_{α}, resp. P_{α}. Finally, put B(P + Q) = ⋃ B_{α}, B = ⋃_{P +Q∈F(B)} B(P + Q) and go to 3.

Let us see how the procedure branches in step 4. If we have P ⟶^{α} P′ so that for no Q ⟶^{α} Q′ the pair P′ + Q′ lies in Id(B) then we pick one such Q′ and add the pair P′ + Q′ to the current basis B. We do this for all failed P ⟶^{α} P′, Q ⟶^{α} Q′ and P + Q.

We exhaust all possibilities by taking all combinations of appropriate pairs of derivatives which makes the procedure non-deterministic.

In order to prove the correctness of the decision procedure we will need the following theorem [12] which is an simple consequence of Hilbert’s basis theorem:

Theorem 1: Let I_{1}, I_{2}, I_{3}, … be a sequence of ideals such that I_{i} ⊆ I_{i+1} for every i. Then there exists an n such that I_{n} = I_{n+i} for every i. (Or, every strictly increasing sequence of ideals is finite.)

Theorem 2: This procedure will always stop for any given input pair P, Q and the output will be affirmative if and only if P ∼ Q.

Proof: The proof consists of two parts. First we show that the procedure is finite.

The computation of the procedure can be described by a tree whose nodes are either labelled by some finite set B or they are leaves. Leaves are either successful - if we manage to find a basis of a bisimulation, or unsuccessful - if we find out that P ≁_{1} Q for some pair P + Q. First we are going to show that all successor nodes of a node B can be constructed in a finite time.

Suppose we are at a node B. B contains a finite number of pairs P + Q. For any P + Q and P ⟶^{α} P′ we have to check if there is a Q ⟶^{α} Q′ so that P′ + Q′ ∈ Id(B), and vice versa. There are only finitely many possible derivatives P′ of P and Q′ of Q and the condition P′ + Q′ ∈ Id(B) can be decided using the method of Gröbner bases (in fact the complexity of the membership check is doubly exponential). Hence we can check CC(B) in a finite time.

If ¬CC(B) then we proceed to step 4 in which we construct all possible successors of B. Here we nondeterministically choose possible pairs P′ + Q′ such that P ⟶^{α} P′ and Q ⟶^{α} Q′ and P′ + Q′ ∉ Id(B) for all failed pairs P + Q and add them to B. As P and Q are finitely branching there is only a finite number of successors of every node and hence the tree is finitely branching.

It remains to show that all branches are of finite lengths. There are three types of nodes in the tree, successful leaves, unsuccessful leaves and nodes labelled by finite bases. Obviously a branch containing a leaf is finite. If there was an infinite branch B_{0}, B_{1}, B_{2}, … in the tree then each B_{i+1} would be constructed from a node B_{i} by adding at least one new pair P′ + Q′ to B_{i} that wouldn’t belong to Id(B_{i}). Trivially P′ + Q′ ∈ Id(B_{i+1}) and so this branch would generate an increasing chain of ideals Id(B_{0}) ⊂ Id(B_{1}) ⊂ Id(B_{2}) ⊂ . . .. From the statement of Theorem 1 we know that every such chain must be finite and hence there cannot be any infinite branch in the tree.

Correctness is a straightforward consequence of finiteness. If there is a branch in the tree that finishes with a successful leaf then that means we have found a set B containing P +Q such that CC(B) and by Proposition 2 that implies that the ideal Id(B) constitutes a witnessing bisimulation for P and Q.

On the other hand, if P and Q are bisimilar then, as in step 4 we consider all possible extensions of the current node, there will be at least one branch in the tree that consists of a chain of finite subsets of B_{∼}. Since all branches are finite at one point we will find a B so that CC(B) and stop the procedure.

Conclusion: The procedure that we have described will always stop and give a correct answer. □

6 Discussion

This new technique seems to be more general than the existing techniques. We hope that there might be some improvement of the complexity bound for decidability of strong bisimulation of general (unnormed) processes. We will also try to apply this technique to weak bisimulation of BPP where there is no known result for general processes.

Acknowledgements

I would like to thank my advisor Mark Jerrum for suggesting this line of research, proposing new ideas and always being very helpful.

References

[1] Caucal D. (1990) Graphes canoniques des graphes algébraiques, in Informatique Théorique at Applications (RAIRO) 24(4), 339-352.

[2] Christensen S. (1993) Decidability and Decomposition in Process Algebras, PhD Thesis, University of Edinburgh.

[3] Christensen S., Hirshfeld Y. and Moller F. (1993) Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes, in Proceedings of LICS, IEEE Computer Society Press 386-396.

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

[5] Christensen S., Hirshfeld Y. and Moller F. (1994) Decidable subsets of CCS, in The Computer Journal 37, No.4.

[6] Geddes K.O., Czapor S.R. and Labahn G. (1992) Algorithms for Computer Algebra, Kluwer Academic Publishers.

[7] Hirshfeld Y. (1994) Deciding equivalences in simple Process Algebras, in LFCS Report Series, University of Edinburgh.

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

[9] Hirshfeld Y., Jerrum M. and Moller F. (1996) 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.

[10] Jacobson N. (1980) Basic Algebra I, II, W.H. Freeman and Company.

[11] McAloon K. (1984) Petri nets and large finite sets, in Theoretical Computer Science 32, North-Holland.

[12] van der Waerden B.L. (1970) Algebra II, Ungar, New York.

[13] Winkler F. (1996) Polynomial Algorithms in Computer Algebra, Springer-Verlag.