Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2011: Automated Technology for Verification and Analysis pp 397–413Cite as

Evaluating LTL Satisfiability Solvers

  • Conference paper

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

Abstract

We perform a comprehensive experimental evaluation of off-the-shelf solvers for satisfiability of propositional LTL. We consider a wide range of solvers implementing three major classes of algorithms: reduction to model checking, tableau-based approaches, and temporal resolution. Our set of benchmark families is significantly more comprehensive than those in previous studies. It takes the benchmark families of previous studies, which only have a limited overlap, and adds benchmark families not used for that purpose before.

We find that no solver dominates or solves all instances. Solvers focused on finding models and solvers using temporal resolution or fixed point computation show complementary strengths and weaknesses. This motivates and guides estimation of the potential of a portfolio solver. It turns out that even combining two solvers in a simple fashion significantly increases the share of solved instances while reducing CPU time spent.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. http://www.antichains.be/alaska/

  2. http://www.lwb.unibe.ch/index.html

  3. http://nusmv.fbk.eu/

  4. http://users.cecs.anu.edu.au/~rpg/PLTLProvers/

  5. http://www.csc.liv.ac.uk/~konev/software/trp++/

  6. http://www.csc.liv.ac.uk/~michel/software/tspass/

  7. http://www.schuppan.de/viktor/atva11/

  8. http://www.kenmcmil.com/smv.html

  9. http://minisat.se/

  10. http://www.antichains.be/acacia/

  11. http://www.iaik.tugraz.at/content/research/design_verification/anzu/

  12. http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/benchmarking_scripts.html

  13. http://www.csc.liv.ac.uk/~ullrich/TRP/

  14. http://www.cril.univ-artois.fr/PB10/

  15. Abate, P., Goré, R.: The Tableau Workbench. In: M4M (2007)

    Google Scholar 

  16. Beer, I., et al.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD 18(2) (2001)

    Google Scholar 

  17. Behdenna, A., Dixon, C., Fisher, M.: Deductive Verification of Simple Foraging Robotic Behaviours. Int. J. of Intelligent Comput. and Cybernetics 2(4) (2009)

    Google Scholar 

  18. Le Berre, D., Simon, L.: The Essentials of the SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Le Berre, D., et al.: The SAT 2009 competition results: does theory meet practice (presentation). In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584. Springer, Heidelberg (2009)

    Google Scholar 

  20. Biere, A., Claessen, K.: Hardware Model Checking Competition (presentation). In: Hardware Verification Workshop 2010, Edinburgh, UK (2010)

    Google Scholar 

  21. Biere, A., Jussila, T.: Benchmark Tool Run, http://fmv.jku.at/run/

  22. Biere, A., et al.: Handbook of Satisfiability. IOS Press, Amsterdam (2009)

    MATH  Google Scholar 

  23. Bloem, R., et al.: Automatic hardware synthesis from specifications: a case study. In: DATE (2007)

    Google Scholar 

  24. Bloem, R., et al.: Specify, Compile, Run: Hardware from PSL. In: COCV. ENTCS, vol. 190(4). Elsevier, Amsterdam (2007)

    Google Scholar 

  25. Cimatti, A., et al.: Boolean Abstraction for Temporal Logic Satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 532–546. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Cimatti, A., et al.: 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 

  27. Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. FMSD 10(1) (1997)

    Google Scholar 

  28. Daniele, M., Giunchiglia, F., Vardi, M.: 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 

  29. Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics (B) (1990)

    Google Scholar 

  30. Emerson, E., Lei, C.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). In: LICS (1986)

    Google Scholar 

  31. Filiot, E., Jin, N., Raskin, J.: An Antichain Algorithm for LTL Realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  32. Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1) (2001)

    Google Scholar 

  33. Fisman, D., et al.: 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 

  34. Gomes, C., Selman, B.: Algorithm portfolios. Artif. Intell. 126(1-2) (2001)

    Google Scholar 

  35. Goranko, V., Kyrilov, A., Shkatov, D.: Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis. In: M4M (2009)

    Google Scholar 

  36. Goré, R.: Personal Communication (2010)

    Google Scholar 

  37. Goré, R., Widmann, F.: An Experimental Comparison of Theorem Provers for CTL. In: CLoDeM (2010)

    Google Scholar 

  38. Goré, R., Widmann, F.: An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 437–452. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  39. Heljanko, K., Junttila, T., Latvala, T.: Incremental and Complete Bounded Model Checking for Full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  40. Henzinger, T., Kupferman, O., Qadeer, S.: From Pre-Historic to Post-Modern Symbolic Model Checking. FMSD 23(3) (2003)

    Google Scholar 

  41. Heuerding, A., et al.: Propositional Logics on the Computer. In: Baumgartner, P., Posegga, J., Hähnle, R. (eds.) TABLEAUX 1995. LNCS, vol. 918, pp. 310–323. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  42. Hirsch, B., Hustadt, U.: Translating PLTL into WS1S: Application Description. In: M4M (2001)

    Google Scholar 

  43. Huberman, B., Lukose, R., Hogg, T.: An Economics Approach to Hard Computational Problems. Science 275(5296) (1997)

    Google Scholar 

  44. Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Collegium Logicum, vol. 8. Kurt Gödel Society (2004)

    Google Scholar 

  45. Hustadt, U., Schmidt, R.A.: Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Dipartimento, di Ingegneria dell’Informazione, Unversitá degli Studi di Siena (2001)

    Google Scholar 

  46. Hustadt, U., Schmidt, R.A.: Scientific Benchmarking with Temporal Logic Decision Procedures. In: KR. Morgan Kaufmann, San Francisco (2002)

    Google Scholar 

  47. Hustadt, U., et al.: TeMP: A Temporal Monodic Prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 326–330. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  48. Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis. Technische Universiteit Eindhoven (1999)

    Google Scholar 

  49. Leyton-Brown, K., et al.: A Portfolio Approach to Algorithm Selection. In: IJCAI. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  50. Ludwig, M., Hustadt, U.: Fair Derivations in Monodic Temporal Reasoning. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 261–276. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  51. Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal logic prover. AI Commun. 23(2-3) (2010)

    Google Scholar 

  52. Ludwig, M., Hustadt, U.: Resolution-Based Model Construction for PLTL. In: TIME (2009)

    Google Scholar 

  53. de Moura, L.: SAL: Tutorial (2004)

    Google Scholar 

  54. de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  55. Nikolić, M.: Statistical Methodology for Comparison of SAT Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 209–222. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  56. Pill, I., et al.: Formal analysis of hardware requirements. In: DAC (2006)

    Google Scholar 

  57. Prosyd, http://www.prosyd.org/

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

    Google Scholar 

  59. Rozier, K., Vardi, M.: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417–431. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  60. Rozier, K., Vardi, M.: LTL Satisfiability Checking. STTT 12(2) (2010)

    Google Scholar 

  61. Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program (2010) (in Press), doi:10.1016/j.scico.2010.11.004

    Google Scholar 

  62. Schuppan, V., Darmawan, L.: Evaluating LTL Satisfiability Solvers (full version) (2011), http://www.schuppan.de/viktor/VSchuppanLDarmawan-ATVA-2011-full.pdf

  63. Schwendimann, S.: A New One-Pass Tableau Calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277–292. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  64. Simon, L., Le Berre, D.: Some Results and Lessons from the SAT Competitions (invited talk, slides only). In: Second International Workshop on Constraint Propagation and Implementation, Sitges, Spain (October 1, 2005)

    Google Scholar 

  65. StatSoft, Inc. Electronic Statistics Textbook. StatSoft, Tulsa, OK, USA, http://www.statsoft.com/textbook/

  66. Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1-2) (2001)

    Google Scholar 

  67. The VIS Group: VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  68. Wolper, P.: The Tableau Method for Temporal Logic: An Overview. Logique et Analyse 28(110-111) (1985)

    Google Scholar 

  69. De Wulf, M., et al.: 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 

  70. Xu, L., et al.: SATzilla: Portfolio-based Algorithm Selection for SAT. JAIR 32 (2008)

    Google Scholar 

Download references

Authors
  1. Viktor Schuppan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luthfi Darmawan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of California, Santa Barbara, CA, USA

    Tevfik Bultan

  2. Department of Computer Science and Information Engineering, National Chung Cheng University, 168 University Road, Min-Hsiung, 62102, Chiayi, Taiwan, ROC

    Pao-Ann Hsiung

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schuppan, V., Darmawan, L. (2011). Evaluating LTL Satisfiability Solvers. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24372-1_28

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24371-4

  • Online ISBN: 978-3-642-24372-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation