[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

  • Conference paper
Automated Deduction – CADE-21 (CADE 2007)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4603))

Included in the following conference series:

Abstract

We present an encoding of LTL bounded model checking problems within the Bernays-Schönfinkel fragment of first-order logic. This fragment, which also corresponds to the category of effectively propositional problems (EPR) of the CASC system competitions, allows a natural and succinct representation of both a software/hardware system and the property that one wants to verify.

The encoding for the transition system produces a formula whose size is linear with respect to its original description in common component description languages used in the field (e.g. smv format) preserving its modularity and hierarchical structure. Likewise, the LTL property is encoded in a formula of linear size with respect to the input formula, plus an additional component, with a size of O(logk) where k is the bound, that represents the execution flow of the system.

The encoding of bounded model checking problems by effectively propositional formulae is the main contribution of this paper. As a side effect, we obtain a rich collection of benchmarks with close links to real-life applications for the automated reasoning community.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. 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) (2006)

    Google Scholar 

  3. Cimatti, A., Clarke, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)

    Google Scholar 

  5. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5, 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  6. Jehle, M., Johannsen, J., Lange, M., Rachinsky, N.: Bounded model checking for all regular properties. Electr. Notes Theor. Comput. Sci. 144(1), 3–18 (2006)

    Article  Google Scholar 

  7. Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 186–200. Springer, Heidelberg (2004)

    Google Scholar 

  8. Martin, A.J.: The design of a self-timed circuit for distributed mutual exclusion. In: Fuchs, H. (ed.) Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration (1985)

    Google Scholar 

  9. McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)

    Google Scholar 

  10. Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. International Journal on Software Tools for Technology Transfer (STTT) 7, 156–173 (2005)

    Article  Google Scholar 

  11. Strichman, O.: Accelerating bounded model checking for safety properties. Formal Methods in System Design 24(1), 5–24 (2004)

    Article  MATH  Google Scholar 

  12. Sutcliffe, G., Suttner, C.: The state of CASC. AI Communications 19(1), 35–48 (2006)

    MATH  MathSciNet  Google Scholar 

  13. Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Navarro-Pérez, J.A., Voronkov, A. (2007). Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73595-3_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73594-6

  • Online ISBN: 978-3-540-73595-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics