Abstract
The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In our reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique “Counterexample-Preserving Reduction” (CePRe, for short), and the proposed technique is experimentally evaluated by adapting NuSMV.
This work is supported by NSFC under Grant No. 61103012, 91118007; the 863 Program under Grant No. 2011AA010106, 2012AA011201; the Program for New Century Excellent Talents in University.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science 2(5:5), 1–64 (2006)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R.: Improving the encoding of LTL model checking into SAT. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 196–207. Springer, Heidelberg (2002)
Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85–96. Springer, Heidelberg (2004)
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)
Frisch, A., Sheridan, D., Walsh, T.: A fixpoint encoding for bounded model checking. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 238–255. Springer, Heidelberg (2002)
Gabbay, D.: The declarative past and imperative future: Executable temporal logic for interactive systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 431–448. Springer, Heidelberg (1989)
Latvala, T., Biere, A., Heljanko, K., Junttila, T.A.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 186–200. Springer, Heidelberg (2004)
Latvala, T., Biere, A., Heljanko, K., Junttila, T.A.: Simple is better: Efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380–395. Springer, Heidelberg (2005)
McMillan, K.L.: Symbolic Model Checking, An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, Kluwer Academic Publishers (1993)
Pnueli, A.: The temporal logic of programs. In: Proc. of 18th IEEE Symposium on Foundation of Computer Science (FOCS 1977), pp. 46–57. IEEE Computer Society (1977)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–65. Springer, Heidelberg (2000)
Taurainen, H., Heljanko, K.: Testing LTL formula translation into Büchi automata. STTT 4, 57–70 (2002)
Vardi, M.Y.: Branching vs. Linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)
Zbrzezny, A.: A new translation from ETCL* to SAT. In: Szczuka, M., et al. (eds.) Proceedings of the International Workshop CS&P 2011, pp. 589–600 (September 2011)
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
Liu, W., Wang, R., Fu, X., Wang, J., Dong, W., Mao, X. (2013). Counterexample-Preserving Reduction for Symbolic Model Checking. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)