ML Anthology

Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau

Matteo Bertello, Nicola Gigante, Angelo Montanari, Mark Reynolds
IJCAI 2016 pp. 950-956
/ijcai/2016/bertello2016ijcai-leviathan/

Abstract

The paper presents Leviathan, an LTL satisfiability checking tool based on a novel one-pass, tree-like tableau system, which is way simpler than existing solutions. Despite the simplicity of the algorithm, the tool has performance comparable in speed and memory consumption with other tools on a number of standard benchmark sets, and, in various cases, it outperforms the other tableau-based tools. PDF

PDF IJCAI Semantic Scholar

Cite

Text

Bertello et al. "Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau." International Joint Conference on Artificial Intelligence, 2016.

Markdown

[Bertello et al. "Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau." International Joint Conference on Artificial Intelligence, 2016.](https://mlanthology.org/ijcai/2016/bertello2016ijcai-leviathan/)

BibTeX

@inproceedings{bertello2016ijcai-leviathan,
  title     = {{Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau}},
  author    = {Bertello, Matteo and Gigante, Nicola and Montanari, Angelo and Reynolds, Mark},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2016},
  pages     = {950-956},
  url       = {https://mlanthology.org/ijcai/2016/bertello2016ijcai-leviathan/}
}