Using PO Methods for Verifying Behavioural Equivalences

The modelling of concurrent systems by synchronized distributed automata generates naturally an independence notion between the events of the global system. The theory of (Mazurkiewicz) traces suggests that such an independence relation induces a nice equivalence relation over the sequences of events of the system. Two sequences will be equivalent just in case they constitute two different interleavings of the same stretch of partially ordered behavior. We want to use reductions of the interleaved global system by this independence relation for verification means. The allowed reduction depends on the property to conserve, the prime condition being to retain at least one representative for each trace. Others recent published works on these methods (often called Partial-Order methods) have proposed the checking of particular linear temporal properties on these reduced models. We study it here in the context of equivalence checking, where a concurrent process description is confronted to ..