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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
http://www.iaik.tugraz.at/content/research/design_verification/anzu/
http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/benchmarking_scripts.html
Abate, P., Goré, R.: The Tableau Workbench. In: M4M (2007)
Beer, I., et al.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD 18(2) (2001)
Behdenna, A., Dixon, C., Fisher, M.: Deductive Verification of Simple Foraging Robotic Behaviours. Int. J. of Intelligent Comput. and Cybernetics 2(4) (2009)
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)
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)
Biere, A., Claessen, K.: Hardware Model Checking Competition (presentation). In: Hardware Verification Workshop 2010, Edinburgh, UK (2010)
Biere, A., Jussila, T.: Benchmark Tool Run, http://fmv.jku.at/run/
Biere, A., et al.: Handbook of Satisfiability. IOS Press, Amsterdam (2009)
Bloem, R., et al.: Automatic hardware synthesis from specifications: a case study. In: DATE (2007)
Bloem, R., et al.: Specify, Compile, Run: Hardware from PSL. In: COCV. ENTCS, vol. 190(4). Elsevier, Amsterdam (2007)
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)
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)
Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. FMSD 10(1) (1997)
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)
Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics (B) (1990)
Emerson, E., Lei, C.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). In: LICS (1986)
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)
Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1) (2001)
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)
Gomes, C., Selman, B.: Algorithm portfolios. Artif. Intell. 126(1-2) (2001)
Goranko, V., Kyrilov, A., Shkatov, D.: Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis. In: M4M (2009)
Goré, R.: Personal Communication (2010)
Goré, R., Widmann, F.: An Experimental Comparison of Theorem Provers for CTL. In: CLoDeM (2010)
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)
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)
Henzinger, T., Kupferman, O., Qadeer, S.: From Pre-Historic to Post-Modern Symbolic Model Checking. FMSD 23(3) (2003)
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)
Hirsch, B., Hustadt, U.: Translating PLTL into WS1S: Application Description. In: M4M (2001)
Huberman, B., Lukose, R., Hogg, T.: An Economics Approach to Hard Computational Problems. Science 275(5296) (1997)
Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Collegium Logicum, vol. 8. Kurt Gödel Society (2004)
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)
Hustadt, U., Schmidt, R.A.: Scientific Benchmarking with Temporal Logic Decision Procedures. In: KR. Morgan Kaufmann, San Francisco (2002)
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)
Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis. Technische Universiteit Eindhoven (1999)
Leyton-Brown, K., et al.: A Portfolio Approach to Algorithm Selection. In: IJCAI. Morgan Kaufmann, San Francisco (2003)
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)
Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal logic prover. AI Commun. 23(2-3) (2010)
Ludwig, M., Hustadt, U.: Resolution-Based Model Construction for PLTL. In: TIME (2009)
de Moura, L.: SAL: Tutorial (2004)
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)
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)
Pill, I., et al.: Formal analysis of hardware requirements. In: DAC (2006)
Prosyd, http://www.prosyd.org/
Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1) (2009)
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)
Rozier, K., Vardi, M.: LTL Satisfiability Checking. STTT 12(2) (2010)
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
Schuppan, V., Darmawan, L.: Evaluating LTL Satisfiability Solvers (full version) (2011), http://www.schuppan.de/viktor/VSchuppanLDarmawan-ATVA-2011-full.pdf
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)
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)
StatSoft, Inc. Electronic Statistics Textbook. StatSoft, Tulsa, OK, USA, http://www.statsoft.com/textbook/
Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1-2) (2001)
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)
Wolper, P.: The Tableau Method for Temporal Logic: An Overview. Logique et Analyse 28(110-111) (1985)
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)
Xu, L., et al.: SATzilla: Portfolio-based Algorithm Selection for SAT. JAIR 32 (2008)
Editor information
Editors and Affiliations
Rights 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)