Verification of Parallel Systems via Decomposition

Jan Friso Groote and Faron Moller

Abstract: Recently, Milner and Moller have presented several decomposition results for processes. Inspired by these, we investigate decomposition techniques for the verification of parallel systems. In particular, we consider those of the form

p1 || p2 || ... || pm = q1 || q2 || ... || qn
where each of the p and each of the q are (finite) state systems. We provide a decomposition procedure for all p and q and give criteria that must be checked on the decomposed processes to see whether the above equation does or does not hold. We analyse the complexity of our procedure and show that it is polynomial in n, m and the sizes of each of the p and q if there is no communication. We also show that with communication the verification of the above equation is co-NP hard, which makes it very unlikely that a polynomial complexity bound exists. But by applying our decomposition technique to Milner's cyclic scheduler we show that verification can become polynomial in space and time for practical examples, where standard techniques are exponential.

LFCS report ECS-LFCS-92-193

This report was published in the proceedings of CONCUR'92, W.R. Cleaveland (editor), Lecture Notes in Computer Science 630, pp62-76, Springer-Verlag, 1992.

Previous | Index | Next