Abstract
The translation of temporal logic specifications constitutes an essential step in model checking and a major influence on the efficiency of formal verification via model checking. We devise a new explicit-state translation of Linear Temporal Logic to automata for the class of LTL specifications that describe safety properties, arguably the most used formal specifications in real-world systems. By exploiting the inherent determinism in safety specifications, we can build deterministic Promela never claims that accept only the bad prefixes of the safety specification. In contrast to previous works, we focus on compilation to never claims rather than simply automata and measure Spin model-checking time separately from compilation time and automata size. An extensive experimental evaluation over a space of configurations demonstrates that our new translation consistently results in better model-checking performance, for a large array of benchmarks, over the best current translation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Dist. Comp. 2, 117–126 (1987)
Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.Y.: Efficient LTL compilation for SAT-based model checking. In: ICCAD, pp. 877–884. IEEE (2005)
Bryant, R.E.: Symbolic Boolean manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
d’Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)
Dong, Y., Du, X., Holzmann, G.J., Smolka, S.A.: Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking. STTT 4(4), 505–528 (2003)
Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized Büchi automata. In: MASCOTS, pp. 76–83. IEEE (2004)
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 997–1072. Elsevier, MIT Press (1990)
Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53–70. Springer, Heidelberg (2006)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of Linear Temporal Logic. In: PSTV, pp. 3–18. Chapman & Hall (1995)
Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Holzmann, G.J.: The model checker Spin. IEEE TSE 23(5), 279–295 (1997)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2003)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (1979)
Jategaonkar Jagadeesan, L., Puchol, C., Von Olnhausen, J.E.: Safety property verification of Esterel programs and applications to telecommunications software. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 127–140. Springer, Heidelberg (1995)
Kaivola, R.: Using compositional preorders in the verification of sliding window protocol. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 48–59. Springer, Heidelberg (1997)
Kamel, M., Leue, S.: Validation of a remote object invocation and object migration in CORBA GIOP using Promela/Spin. In: SPIN (1998)
Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 110–124. Springer, Heidelberg (2006)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. FMSD 19(3), 291–314 (2001)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL 2(2), 408–429 (2001)
Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 74–88. Springer, Heidelberg (2003)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc. (1996)
Møller, A.: dk.brics.automaton (2004), http://www.brics.dk/automaton/
Pelánek, R.: BEEM: Benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)
Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 368–382. Springer, Heidelberg (2009)
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. International Journal on Software Tools for Technology Transfer (STTT) 12(2), 123–137 (2010)
Safra, S.: On the complexity of ω-automata. In: FOCS, pp. 319–327 (1988)
Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 39–54. Springer, Heidelberg (2001)
Sebastiani, R., Tonetta, S.: “More deterministic” vs. “Smaller” Büchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)
Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods in System Design 41(3), 236–268 (2012)
Vardi, M.Y.: From monadic logic to PSL. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 656–681. Springer, Heidelberg (2008)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Comp. Sci., Cambridge, pp. 332–344 (June 1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rozier, K.Y., Vardi, M.Y. (2013). Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking. In: Biere, A., Nahir, A., Vos, T. (eds) Hardware and Software: Verification and Testing. HVC 2012. Lecture Notes in Computer Science, vol 7857. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39611-3_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-39611-3_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39610-6
Online ISBN: 978-3-642-39611-3
eBook Packages: Computer ScienceComputer Science (R0)