Authors: Alexandre Duret-Lutz
Addresses: EPITA's Research and Development Laboratory (LRDE), 14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre, France
Abstract: Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. We detail the different algorithms involved in this translation: the core translation itself, which performs many simplifications thanks to its use of binary decision diagrams; the pre-processing of the LTL formulas with rewriting rules chosen to help their translation; and various post-processing algorithms whose use depends on the intent of the translation: do we favour deterministic automata, or small automata? Using different benchmarks, we show how Spot competes with other LTL translators, and how it has improved over the years.
Keywords: formal methods; model checking; Büchi automata; linear-time temporal logic; LTL translators; translation; simplifications; software verification; implementation; Spot.
International Journal of Critical Computer-Based Systems, 2014 Vol.5 No.1/2, pp.31 - 54
Published online: 21 Oct 2014 *Full-text access for editors Access for subscribers Purchase this article Comment on this article