Abstract
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 a specification by comparing their labeled transition systems together (relative to bisimulation for instance). We define a reduced global automaton with predicates on the states where transitions were suppressed, and conditions for retaining enough information for representing the global system for verification. The limits of the approach are shown as well as suggestions for practical applications and some experimental results on classical examples.
Chapter PDF
Similar content being viewed by others
References
Bednarczyk, M.A. (1988) Categories of asynchronous systems. U. of Sussex, 1/88.
Bouali, A. and Lara de Souza, M. and Madelaine, E. and Ressouche, A. and Roy, V. and de Simone, R. (1995) FC2 transformations for clever verification. Technical report, INRIA.
de Simone, R. and Vergamini, D. (1989) Aboard Auto. Technical report, INRIA.
Mazurkiewicz, A. (1986) Trace Theory. Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course.
Milner, R.. (1989) Communication and Concurrency. Prentice Hall, Englewood Cliffs.
Peled, D. (1993) All from One, One for All: On Model Checking Using Representatives. Proceedings of CAV’93, LNCS,697.
Peled, D. (1994) Combining Partial Order Reductions with On-the-fly Model-Checking. Proceedings of CAV’94, LNCS 818.
Gerth, R. and Kuiper, R. and Peled, R. and Penczek, W. (1995) A Partial Order Approach to Branching Time Model Checking. Proceedings of ISTCS, 330–339.
Shields, M.W. (1985) Concurrent machines. Computer Journal, 28.
Valmari, A. (1990) A Stubborn Attack on State Explosion. Lecture Notes in Computer Science, Springer-Verlag, 531.
Winskel, G. and Nielsen, M. (1993) Models for Concurrency. TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science.
Wolper, P. and Godefroid, P. (1993) Partial-Order Methods for Temporal Verification. Proceedings of Concur’93, 715.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
de Souza, M.L., de Simone, R. (1996). Using PO Methods for Verifying Behavioural Equivalences. In: Bochmann, G.v., Dssouli, R., Rafiq, O. (eds) Formal Description Techniques VIII. FORTE 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34945-9_6
Download citation
DOI: https://doi.org/10.1007/978-0-387-34945-9_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2958-9
Online ISBN: 978-0-387-34945-9
eBook Packages: Springer Book Archive