Abstract
Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Baumgartner J, Kühlmann A, Abraham J (2002) Property checking via structural analysis. In: Brinksma E, Larsen K (eds) Proceedings of the 14th international conference on computer aided verification (CAV 2002), Copenhagen, Denmark, 27–31 July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 151–165
Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y (1999a) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th ACM/IEEE conference on design automation (DAC’99), New Orleans, 21–25 June 1999, pp 317–320. ACM Press, New York
Biere A, Cimatti A, Clarke E, Zhu Y (1999b) Symbolic model checking without BDDs. In: Cleaveland R (ed) Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS ’99), Amsterdam, 22–28 March 1999. Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 193–207
Biere A, Clarke E, Zhu Y (1999c) Multiple state and single state tableaux for combining local and global model checking. In: Olderog ER, Steffen B (eds) Correct system design, recent insight and advances. Lecture notes in computer science, vol 1710. Springer, Berlin Heidelberg New York, pp 163–179
Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: Cleaveland R, Garavel H (eds) Proceedings of the 7th international ERCIM workshop on formal methods for industrial critical systems (FMICS’02), Málaga, Spain, 12–13 July 2002. Electronic notes in theoretical computer science, 66(2). Elsevier, Amsterdam
Browne M, Clarke E, Grumberg O (1988) Characterizing finite Kripke structures in propositional logic. Theor Comput Sci 59(1–2):115–131
Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677–691
Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Halbwachs and Peled [15], pp 495–499
Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D (ed) Proceedings of the workshop on logic of programs, Yorktown Heights, NY, May 1981, Lecture notes in computer science, vol 131. Springer, Berlin Heidelberg New York, pp 52–71
Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA
Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Formal Meth Sys Des 1:275–288
Emerson A (1999) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science: Volume B. Formal methods and semantics, pp 995–1072. North-Holland, Amsterdam
Gerth R, Peled D, Vardi M, Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski P, Sredniawa M (eds) Proceedings of the 15th IFIP WG6.1 international symposium on protocol specification, testing and verification, Warsaw, Poland, June 1995. IFIP conference proceedings, 38:3–18. Chapman & Hall, London
Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE international conference on automated software engineering (ASE 2001), 26–29 November 2001, Coronado Island, San Diego, CA, pp 412–416. IEEE Press, New York
Halbwachs N, Peled D (eds) (1999) Proceedings of the 11th international conference on computer aided verification (CAV ’99), Trento, Italy, 6–10 July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York
Halbwachs N, Lagnier F, Raymond P (1994) Synchronous observers and the verification of reactive systems. In: Nivat M, Rattray C, Rus T, Scollo G (eds) Proceedings of the 3rd international conference on algebraic methodology and software technology (AMAST ’93), University of Twente, Enschede, The Netherlands, 21–25 June 1993. Workshops in computing. Springer, Berlin Heidelberg New York, pp 83–96
Havelund K, Roşu G (2001) Monitoring Java programs with Java PathExplorer. In: Havelund K, Roşu G (eds) Proceedings of the 1st international workshop on runtime verification (RV’01), Paris, France, 23 July 2001. Electronic notes in theoretical computer science, 55(2). Elsevier, 2001.
Havelund K, Roşu G (2002) Synthesizing monitors for safety properties. In: Katoen J-P, Stevens P (eds) Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2002), Grenoble, France, 8–12 April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 342–356
Henzinger T, Kupferman O, Qadeer S (1998) From pre-historic to post-modern symbolic model checking. In: Hu A, Vardi M (eds) Proceedings of the 10th international conference on computer aided verification (CAV ’98), Vancouver, BC, Canada, 28 June–2 July 1998. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 195–206
Iwashita H, Nakata T, Hirose F (1996) CTL model checking based on forward state traversal. In: Proceedings of the 1996 IEEE/ACM international conference on computer-aided design, San Jose, CA, 10–14 November 1996, pp 82–87. IEEE Press, New York
Jagadeesan L, Puchol C, von Olnhausen J (1995) Safety property verification of ESTEREL programs and applications to telecommunications software. In: Wolper P (ed) Proceedings of the 7th international conference on computer aided verification, Liège, Belgium, 3–5 July 1995. Lecture notes in computer science, vol 939. Springer, Berlin Heidelberg New York, pp 127–140
Kröning D, Strichman O (2003) Efficient computation of recurrence diameters. In: Zuck L, Attie P, Cortesi A, Mukhopadhyay S (eds) Proceedings of the 4th international conference on verification, model checking, and abstract interpretation (VMCAI 2003), New York, 9–11 January 2002. Lecture notes in computer science, vol 2575. Springer, Berlin Heidelberg New York, pp 298–309
Kupferman O, Vardi M (1999) Model checking of safety properties. In: Halbwachs and Peled [15], pp 172–183
Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143
McMillan K Cadence SMV. http://www-cad.eecs.berkeley.edu/ kenmcmil/smv.
McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer, Dordrecht
Niermann T, Patel J (1991) HITEC: A test generation package for sequential circuits. In: Proceedings of the European conference on design automation, Amsterdam, 25–28 February 1991, pp 214–218. IEEE Press, New York
Peled D (2001) Software reliability methods. Springer, Berlin Heidelberg New York
Schuppan V, Biere A (2003) Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. Formal Asp Comput 14(3):267–280
Seger C-J, Bryant R (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Meth Sys Des 6(2):147–189
Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt Jr W, Johnson S (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD 2000), Austin, TX, 1–3 November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 108–125
Somenzi F Wring 1.1.0. ftp://vlsi.colorado.edu/pub/Wring-1.1.0.tar.gz.
Somenzi F, Bloem R (2000) Efficient Buchi automata from ltl formulae. In: Emerson A, Sistla P (eds) Proceedings of the 12th international conference on computer aided verification (CAV 2000), Chicago, 15–19 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 248–263
The VIS Group (1996) VIS: a system for verification and synthesis. In: Alur R, Henzinger T (eds) Proceedings of the 8th international conference on computer aided verification (CAV ’96), New Brunswick, NJ, 31 July–3 August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 428–432
Yang B. SMV models. http://www.cs.cmu.edu/ bwolen/software/smv-models/.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Schuppan, V., Biere, A. Efficient reduction of finite state model checking to reachability analysis. STTT 5, 185–204 (2004). https://doi.org/10.1007/s10009-003-0121-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-003-0121-x