Abstract
Checking the properties of concurrent systems is an ever growing challenge. Along with the development of improved verification methods, some critical systems that require careful attention have become highly concurrent and intricate. Partial order reduction methods were proposed for reducing the time and memory required to automatically verify concurrent asynchronous systems. We describe partial order reduction for various logical formalisms, such as LTL, CTL and process algebras. We show how one can combine partial order reduction with other efficient model checking techniques.
This survey was written while the author was visiting Carnegie Mellon University School of Computer Science Pittsburgh, PA 15213-3891, USA. Author's current address: Bell Laboratories, 700 Mountain Ave. Murray Hill, NJ 07974, USA
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, Partial order reduction in symbolic state space exploration. In Proceedings of the Conference on Computer Aided Verification (CAV'97), Haifa, Israel, June 1997.
M.C. Browne, E.M. Clarke, O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science 59 (1988), Elsevier, 115–131.
R.E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers, C-35(8), 1986, 677–691.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 102° states and beyond, Information and Computation, 98 (1992), 142–170.
C.T. Chou, D. Peled, Verifying a model-checking algorithm, Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, Springer, 1996, Passau, Germany. 241–257.
E.M. Clarke, E.A. Emerson, Design and synthesis of synchronous skeletons using branching time temporal logic, Logic of Programs, Yorktown Heights, NY, LNCS 131, Springer, 1981, 52–71.
C. Courcoubetis, M.Y. Vardi, P. Wolper, M, Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal methods in system design 1 (1992) 275–288.
E.A. Emerson, E.M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, Automata, Languages and Programming, LNCS 85, Springer, 1980, 169–181.
R. Gerth, R. Kuiper, W. Penczek, D. Peled, A partial order approach to branching time logic model checking, ISTCS'95, 3rd Israel Symposium on Theory on Computing and Systems, IEEE press, 1995, Tel Aviv, Israel, 130–139. A full version was accepted to Information and Computation.
R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, PSTV95, Protocol Specification Testing and Verification, Chapman & Hall, 1995, Warsaw, Poland, 3–18.
R.J. van Glabbeek, W.P. Weijland, Branching time and abstraction in bisimulation semantics, Information Processing 89. Elsevier Science Publishers, 1989, 613–618.
P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, LNCS 531, Springer, New Brunswick, NJ, 1990, 176–185.
P. Godefroid, D. Pirottin, Refining dependencies improves partial order verification methods, 5th Conference on Computer Aided Verification, LNCS 697, Elounda, Greece, 1993, 438–449.
P. Godefroid, D. Peled, M. Staskauskas, Using partial order methods in the formal validation of industrial concurrent programs, 1996, ISSTA'96, International Symposium on Software Testing and Analysis, ACM Press, San Diego, California, USA, 261–269.
P. Godefroid, P. Wolper, A Partial approach to model checking, 6th Annual IEEE Symposium on Logic in Computer Science, 1991, Amsterdam, 406–415.
G.J. Holzmann, P. Godefroid, D. Pirottin, Coverage preserving reduction strategies for reachability analysis, Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Orlando, Florida, 1992, 349–363.
G.J. Holzmann, D. Peled, An improvement in formal verification, 7th International Conference on Formal Description Techniques, Berne, Switzerland, 1994, 177–194.
S. Jha, D. Peled, Generalized stuttering equivalence for linear temporal logic specification, Submitted for publication.
S. Katz, D. Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing 6 (1992), 107–120. A preliminary version appeared in Temporal Logic in Specification, UK, 1987, LNCS 398, 21–43.
S. Katz, D. Peled, Defining conditional independence using collapses, Theoretical Computer Science 101 (1992), 337–359, a preliminary version appeared in BCS-FACS Workshop on Semantics for Concurrency, Leicester, England, July 1990, Springer, 262–280.
I. Kokkarinen, A. Valmari, D. Peled, Relaxed visibility enhances partial order reduction, CAV'97, June 1997, Israel, LNCS 1254, 328–339.
R.P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994.
R.P. Kurshan, V. Levin, M. Minea, D. Peled, H. Yenigün, Static partial order reduction, 345–357, 1997.
L. Lamport, What good is temporal logic, in R.E.A. Mason (ed.), Information Processing '83: Proc. of the IFIP 9th World Computer Congress,, Paris, France, North-Holland, Amsterdam, 1983, 657–668.
O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, Proceedings of the 11th Annual Symposium on Principles of Programming Languages, ACM Press, 1984, 97–107.
Z. Manna, A. Pnuefi, How to cook a temporal proof system for your pet language. Proceedings of the Symposium on Principles on Programming Languages, Austin, Texas, 1983, 141–151.
A. Mazurkiewicz, Trace theory, Advances in Petri Nets 1986, Bad Honnef, Germany, LNCS 255, Springer, 1987, 279–324.
R. Milner, A calculus of communicating system, LNCS, Springer, 92.
R. de Nicola, F. Vaandrager, Three logics for branching bisimulation, Logic in Computer Science '90, IEEE, 1990, 118–129.
D. Peled, On projective and separable properties, Theoretical Computer Science, 186(1-2), 1997, 135–155.
D. Peled, A. Pnueli, Proving partial order properties, Theoretical Computer Science, 126 (1994), 143–182.
D. Peled, All from one, one for all, on model-checking using representatives, 5th Conference on Computer Aided Verification, Greece, 1993, LNCS, Springer, 409–423.
D. Peled, Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8 (1996), 39–64. A preliminary version appeared in Computer Aided Verification 94, LNCS 818, Springer, Stanford, USA, 377–390.
D. Peled, Th. Wilke, Stutter-invariant temporal properties are expressible without the nexttime operator, Information Processing Letters 63 (1997), 243–246.
D. Peled, Th. Wilke, P. Wolper, An algorithmic approach for checking closure properties of w-Regular Languages, CONCUR'96, 7th International Conference on Concurrency Theory, Piza, Italy, LNCS 1119, Springer, August 1996, 596–610. A full version accepted to Theoretical Computer Science.
J.P. Quielle, J. Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th International Symposium on Programming, 1981, 337–350.
A. Valmari, Stubborn sets for reduced state space generation, 10th International Conference on Application and Theory of Petri Nets, Bonn, Germany, 1989, LNCS 483, Springer, 491–515.
A. Valmari, A stubborn attack on state explosion. Formal Methods in System Design, 1 (1992), 297–322.
A. Valmari, On-the-fly verification with stubborn sets, Proceedings of CAV '93, 5th International Conference on Computer-Aided Verification, Elounda, Greece, LNCS 697, Springer 1993, pp. 397–408.
A. Valmari, Stubborn set methods for process algebras, POMIV'96, Partial Orders Methods in Verification, American Mathematical Society, DIMACS, Princeton, NJ, USA, 1996, 213–232.
M.Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, 1st Annual IEEE Symposium on Logic in Computer Science, 1986, Cambridge, England, 322–331.
B. Willems, P. Wolper, Partial-order methods for model-checking: from linear time to branching time, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA, 1996, 294–303.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peled, D. (1998). Ten years of partial order reduction. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028727
Download citation
DOI: https://doi.org/10.1007/BFb0028727
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive