Leviathan: a new LTL satisfiability checking tool based on a one-pass tree-shaped tableau
Matteo Bertello, Nicola Gigante, Angelo Montanari, Mark A Reynolds · Institutional Research Information System (University of Udine) · 2016
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.