@inproceedings{50eea03c7dbd4e0da63f60a1466e9cba,
title = "SAT-Based explicit LTL reasoning",
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.",
author = "Jianwen Li and Shufang Zhu and Geguang Pu and Vardi, \{Moshe Y.\}",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 11th International Haifa Verification Conference, HVC 2015 ; Conference date: 17-11-2015 Through 19-11-2015",
year = "2015",
doi = "10.1007/978-3-319-26287-1\_13",
language = "英语",
isbn = "9783319262864",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "209--224",
editor = "Nir Piterman",
booktitle = "Hardware and Software",
address = "德国",
}