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 || ... || qnwhere 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.
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 An error occured whilst processing this directive