Abstract
Partial order based reduction techniques to reduce time and memory in model-checking procedures are becoming quite popular. Partial order reduction techniques exploit the independence of actions. Symmetry based reduction techniques exploit the inherent structure of the system to reduce the state space explored during model checking. We provide an abstract framework for combining partial-order and symmetry reductions. We also present algorithms which exploit both reduction techniques simultaneously.
The research of the first author was supported by NSF under grant no. CCR-9415496 and Semiconductor Research Corporation under contract 96-DP-388.
The reseach of the second author was sponsored in part by the National Science Foundation under grant no. CCR-8722633, by the Semiconductor Research Corporation under contract 92-DJ-294, and by the Wright Laboratory, Aeronautical Systems Center, Air Force Materiel Command, USAF, and the Advanced Research Projects Agency (ARPA) under grant F33615-93-1-1330.
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
M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.
E.M. Clarke, T.Filkorn, and S.Jha. Exploiting symmetry in temporal logic model checking. In Courcoubetis [4].
C. Courcoubetis, editor. Proceedings of the Fifth Workshop on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, June 1993.
E. Allen Emerson and A. Prasad Sistla. Symmetry and model checking. In Courcoubetis [4].
Rob Gerth, Ruurd Kuiper, Doron Peled, and Wojciech Penczek. A partial order approach to branching time logic model checking. In Third Israel Symposium on Theory on Computing and Systems, pages 130–139, Tel Aviv, Israel, 1995. IEEE.
P. Godefroid. Using partial orders to improve automatic verification methods. In Kurshan and Clarke [10].
P. Huber, A.M. Jensen, L.O. Jepsen, and K. Jensen. Towards reachability trees for high-level petri nets. In G. Rozenberg, editor, Advances on Petri Nets, pages 215–233, 1984.
C.W. Ip and D. Dill. Better verification through symmetry. In L. Claesen, editor, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.
R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification. Springer-Verlag, June 1990.
Doron Peled. All from one, one from all: on model checking using representatives. In 5th International Conference on Computer Aided Verification, Greece, number 697 in LNCS, pages 409–423, Elounda Crete, Greece, 1993. Springer-Verlag.
Doron Peled. Partial order reduction: Linear and branching temporal logics and process algebras. In Partial Orders Methods in Verification, DIMACS, Princeton, NJ, USA, 1996. American Mathematical Society.
P.H. Starke. Reachability analysis of petri nets using symmetries. Syst. Anal. Model. Simul., 8(4/5):293–303, 1991.
A. Valmari. Stubborn sets for reduced state space generation. In Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, 1989.
A. Valmari. A stubborn attack on the state explosion problem. In Kurshan and Clarke [10].
A. Valmari. Stubborn sets of colored petri nets. In Proceedings of the 12th International Conference on Application and Theory of Petri Nets, pages 102–121, Gjern, Denmark, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Jha, S., Peled, D. (1997). Combining partial order and symmetry reductions. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035378
Download citation
DOI: https://doi.org/10.1007/BFb0035378
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive