Abstract
We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We implemented the algorithm in a tool, Aalta_v2.0, which is built on top of the Minisat SAT solver. We tested the effectiveness of this approach by demonstrating that Aalta_v2.0 significantly outperforms all existing LTL satisfiability solvers.
Cite
CITATION STYLE
Li, J., Zhu, S., Pu, G., & Vardi, M. Y. (2015). SAT-Based explicit LTL reasoning. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9434, pp. 209–224). Springer Verlag. https://doi.org/10.1007/978-3-319-26287-1_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
