Skip to main content
SpringerLink
Log in

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking

  • Conference paper
FM 2011: Formal Methods (FM 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6664))

Included in the following conference series:

Abstract

Formal behavioral specifications written early in the system-design process and communicated across all design phases have been shown to increase the efficiency, consistency, and quality of the system under development. To prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. Our focus here is on specifications expressed in linear temporal logic (LTL).

We introduce a novel encoding of symbolic transition-based Büchi automata and a novel, “sloppy,” transition encoding, both of which result in improved scalability. We also define novel BDD variable orders based on tree decomposition of formula parse trees. We describe and extensively test a new multi-encoding approach utilizing these novel encoding techniques to create 30 encoding variations. We show that our novel encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking.

A full version of this paper with appendices is available at http://ti.arc.nasa.gov/m/profile/ kyrozier/papers/RozierVardiFM2011.pdf.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 254–268. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. FMSD 18(2), 141–162 (2001)

    MATH  Google Scholar 

  3. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS, vol. 66(2) (2002)

    Google Scholar 

  4. Bloem, R., Cimatti, A., Pill, I., Roveri, M.: Symbolic implementation of alternating automata. IJFCS 18(4), 727–743 (2007)

    MathSciNet  MATH  Google Scholar 

  5. Bryant, R.E.: Graph-based algorithms for Boolean-function manipulation. IEEE TC C-35(8), 677–691 (1986)

    MATH  Google Scholar 

  6. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inform. and Computation 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cichon, J., Czubak, A., Jasinski, A.: Minimal Büchi automata for certain classes of LTL formulas. In: DepCoS, pp. 17–24 (2009)

    Google Scholar 

  8. Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: A modular symbolic encoding. In: FMCAD (2006)

    Google Scholar 

  9. Cimatti, A., Roveri, M., Tonetta, S.: Syntactic optimizations for PSL verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 505–518. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design 10(1), 47–71 (1997)

    Article  Google Scholar 

  11. Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 233–242. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  12. Couvreur, J.-M.: On-the-fly verification of Linear Temporal Logic. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. De Wulf, M., Doyen, L., Maquet, N., Raskin, J.: Antichains: Alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63–77. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using Transition-Based Generalized Büchi Automata. In: MASCOTS, pp. 76–83 (2004)

    Google Scholar 

  16. Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 997–1072. Elsevier, MIT Press (1990)

    Google Scholar 

  17. Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: Local vs. Global. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 489–503. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Log. Comput. 7(4), 429–456 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  19. Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 7–22. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. 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 and Hall, Boca Raton (1995)

    Google Scholar 

  22. Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata. In: FORTE (November 2002)

    Google Scholar 

  23. Goranko, V., Kyrilov, A., Shkatov, D.: Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis. ENTCS 262, 113–125 (2010)

    MathSciNet  Google Scholar 

  24. Habibi, A., Tahar, S.: Design for verification of SystemC transaction level models. In: Design, Automation and Test in Europe, pp. 560–565. IEEE, Los Alamitos (2005)

    Chapter  Google Scholar 

  25. Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 97–109. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  26. Koster, A.M.C.A., Bodlaender, H.L., van Hoesel, S.P.M.: Treewidth: Computational experiments. ZIB-Report 01–38, ZIB (2001)

    Google Scholar 

  27. Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. STTT 4(2), 224–233 (2003)

    Article  MATH  Google Scholar 

  28. Merz, S., Sezgin, A.: Emptiness of Linear Weak Alternating Automata. Technical report, LORIA (December 2003)

    Google Scholar 

  29. Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 16–30. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC, pp. 821–826. ACM, New York (2006)

    Google Scholar 

  31. Pnueli, A.: The temporal logic of programs. In: IEEE FOCS, pp. 46–57 (1977)

    Google Scholar 

  32. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)

    Google Scholar 

  33. Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1), 80–116 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  34. Roveri, M.: Novel techniques for property assurance. Technical report, PROSYD deliverable 1.2/2 (2004)

    Google Scholar 

  35. Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  36. Ruah, S., Fedeli, A., Eisner, C., Moulin, M.: Property-driven specification of VLSI design. Technical report, PROSYD deliverable 1.1/1 (2005)

    Google Scholar 

  37. 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)

    Chapter  Google Scholar 

  38. 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)

    Chapter  Google Scholar 

  39. Sistla, A.P., Clarke, E.M.: The complexity of Propositional Linear Temporal Logic. J. ACM 32, 733–749 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  40. 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. 248–263. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  41. Thirioux, X.: Simple and efficient translation from LTL formulas to Büchi automata. ENTCS 66(2), 145–159 (2002)

    Google Scholar 

  42. Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  43. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, Cambridge, pp. 332–344 (June 1986)

    Google Scholar 

  44. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NASA Ames Research Center, Moffett Field, CA, 94035, USA

    Kristin Y. Rozier

  2. Rice University, Houston, Texas, 77005, USA

    Kristin Y. Rozier & Moshe Y. Vardi

Authors
  1. Kristin Y. Rozier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Southampton, UK

    Michael Butler

  2. Microsoft Research, Redmond, WA, USA

    Wolfram Schulte

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rozier, K.Y., Vardi, M.Y. (2011). A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_31

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21437-0_31

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21436-3

  • Online ISBN: 978-3-642-21437-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation