## 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

*p*_{1} || *p*_{2} || ... ||
*p*_{m} = *q*_{1} ||
*q*_{2} || ... ||
*q*_{n}

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