Abstract
The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.
We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.
Chapter PDF
Keywords
- Partial Order
- Partial Order Reduction
- Predicate Transformer
- Reachability Algorithm
- Check Safety Property
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 O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254, pages 340–351, Haifa, Israel, 1997. Springer Verlag.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 414-425, Philadelphia, 1990.
Parosh Aziz Abdulla, Karlis Čerāns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11 th IEEE Int. Symp. on Logic in Computer Science, pages 313–321, 1996.
Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8 th IEEE Int. Symp. on Logic in Computer Science, pages 160–170, 1993.
Parosh Aziz Abdulla, Mats Kindahl, and Doron Peled. An improved search strategy for Lossy Channel Systems. In Tadanori Mizuno, Nori Shiratori, Teruo Hegashino, and Atsushi Togashi, editors, FORTE X / PST V XVII '97, pages 251–264. Chapman and Hall, 1997.
R.J.R. Back. A method for refining atomicity in parallel algorithms. In Proc. PARLE 89, volume 366 of Lecture Notes in Computer Science, pages 199–216. Springer Verlag, 1989.
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 102o states and beyond. Information and Computation, 98:142–170, 1992.
B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. 8 th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, 1996.
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144–179, 1990.
P. Godefroid, D. Pirottin. Refining Dependencies Improves Partial-Order Verification Methods. Proc. 5th Conference on Computer Aided Verification, Lecture Notes in Computer Science 697, Springer, 438–449. Elounda, Greece, 1993.
P. Godefroid and P. Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In Formal Methods in System Design, Kluwer, 2 (1993), 149–164.
G.J. Holzmann and D. Peled. An improvement in formal verification. In Proc. FORTE '94, pages 197–211, 1994.
[JZ92] W. Janssen and J. Zwiers. From sequential layers to distributed processes. In Proc. 11 th ACM Symp. on Principles of Distributed Computing, Canada, 1992.
Shmuel Katz and Doron Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337–359, 1992.
R.P. Kurshan, V. Levin, M. Minea and D. Peled, H. Yenigun,. Static Partial Order Reduction. TACAS'98, Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal.
L. Lamport. A theorem on atomicity in distributed algorithms. Distributed Computing, 4(2):59–68, 1990.
Lipton. Reduction, a method of proving properties of parallel programs. Communications of the ACM, 18(12):717–721, Dec. 1975.
K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In Proc. 18 th IEEE Real-Time Systems Symposium, pages 14–24, San Francisco, California, Dec. 1997.
K.L. McMillan. A technique of a state space search based on unfolding. Formal Methods in System Design, 6(1):45–65, 1995.
D. Peled. Combining Partial Order Reductions with On-the-fly Model-Checking. Journal of Formal Methods in Systems Design, 8 (1996), 39–64.
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, number 483 in Lecture Notes in Computer Science, pages 491–515. Springer-Verlag, 1990.
A. Valmari. On-the-fly verification with stubborn sets. In Courcoubetis, editor, Proc. 5 th Int. Conf. on Computer Aided Verification, number 697 in Lecture Notes in Computer Science, pages 59–70, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D. (1998). A general approach to partial order reductions in symbolic verification. 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/BFb0028760
Download citation
DOI: https://doi.org/10.1007/BFb0028760
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