A Compositional Sweep-Line State Space Exploration Method
State space exploration is a main approach to verification of finite-state systems. The sweep-line method exploits a certain kind of progress present in many systems to reduce peak memory usage during state space exploration. We present a new sweep-line algorithm for a compositional setting where systems are composed of subsystems. The compositional setting makes it possible to divide subsystem progress measures into monotone and non-monotone progress measures to further reduce peak memory usage. We show that in a compositional setting, it is possible to automatically obtain a progress measure for the system by combining the progress measure for each subsystem to a progress measure for the full system.
- 1.S. Christensen, L.M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Proc. of TACAS’01, volume 2031 of LNCS, pages 450–464. Springer-Verlag, 2001.Google Scholar
- 2.E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetries in Temporal Logic Model Checking. In Proc. of CAV’93, pages 450–462. Springer-Verlag, 1993.Google Scholar
- 3.P. Godefroid, G.J. Holzman, and D. Pirottin. State Space Caching Revisited. In Proc. of CAV’92, volume 663 of LNCS, pages 178–191. Springer-Verlag, 1992.Google Scholar
- 4.S. Gordon, L.M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol. In Proc. of ICATPN’02, volume 2360 of LNCS, pages 182–202. Springer-Verlag, 2002.Google Scholar
- 5.C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
- 6.G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.Google Scholar
- 7.C. Jard and T. Jeron. Bounded-memory Algorithms for Verification On-the-fly. In Proc. of CAV’91, volume 575 of LNCS, pages 192–202. Springer-Verlag, 1991.Google Scholar
- 8.L.M. Kristensen and T. Mailund. A Compositional Sweep-Line State Space Exploration Method. Technical report, Department of Computer Science, University of Aarhus, 2002. Available via: http://www.daimi.au.dk/~mailund/ps/lmktm_compo.ps.
- 9.L.M. Kristensen and T. Mailund. A Generalised Sweep-Line Method for Safety Properties. In Proc. of FME’02, volume 2391 of LNCS, pages 549–567. Springer-Verlag, 2002.Google Scholar
- 11.T. Mailund. SweepChecker. http://sweepchecker.sourceforge.net.
- 12.K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
- 13.R. Milner. Communication and Concurrency. Prentice-Hall International Series in Computer Science. Prentice-Hall, 1989.Google Scholar
- 14.D. Peled. All from One, One for All: On Model Checking Using Representatives. In Proc. of CAV’93, volume 697 of LNCS, pages 409–423. Springer-Verlag, 1993.Google Scholar
- 16.A. Valmari. Stubborn Sets for Reduced State Space Generation. In Advances in Petri Nets’ 90, volume 483 of LNCS, pages 491–515. Springer-Verlag, 1990.Google Scholar
- 17.A. Valmari. Compositionality in State Space Verification Methods. In Proc. of ICATPN’96, volume 1091 of LNCS, pages 29–56. Springer-Verlag, 1996.Google Scholar
- 18.M. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verifcation. In Proc. of IEEE Symposium on Logic in Computer Science, pages 322–331, 1986.Google Scholar
- 19.P. Wolper and P. Godefroid. Partial Order Methods for Temporal Verification. In Proc. of CONCUR’93, volume 715 of LNCS, pages 233–246. Springer-Verlag, 1993.Google Scholar