A New Tableau-based Satisfiability Checker for Linear Temporal Logic

Tableaux-based methods were among the first techniques proposed for Linear Temporal Logic satisfiability checking. The earliest tableau for LTL by [21] worked by constructing a graph whose path represented possible models for the formula, and then searching for an actual model among those paths. Subsequent developments led to the tree-like tableau by [17], which works by building a structure similar to an actual search tree, which however still has back-edges and needs multiple passes to assess the existence of a model. This paper summarizes theworkdoneonanewtool for LTL satisfiability checking based on a novel tableau method. The new tableau construction, which is very simple and easy to explain, builds an actually tree-shaped structure and it only requires a single pass to decide whether to accept a given branch or not. The implementation has been compared in terms of speed and memory consumption with tools implementing both existing tableau methods and different satisfiability techniques, showing good results despite the simplicity of the underlying algorithm.