Paper Info
Title
Evaluating LTL satisfiability solvers
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.
Year
DOI
Venue
2011
10.1007/978-3-642-24372-1_28
ATVA
Keywords
Field
DocType
fixed point,complementary strength,temporal resolution,previous study,off-the-shelf solvers,cpu time,benchmark family,portfolio solver,guides estimation,ltl satisfiability solvers,comprehensive experimental evaluation
Fixed point computation,Model checking,CPU time,Computer science,Satisfiability,Linear temporal logic,Theoretical computer science,Solver,Temporal resolution
Conference
Volume
ISSN
Citations 
6996
0302-9743
23
PageRank 
References 
Authors
0.86
38
2
Name
Order
Citations
PageRank
Viktor Schuppan140917.49
Luthfi Darmawan2271.94