Title: LTL translation improvements in Spot 1.0

 

Author: Alexandre Duret-Lutz

 

Address: EPITA's Research and Development Laboratory (LRDE), 14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre, France

 

Journal: Int. J. of Critical Computer-Based Systems, 2014 Vol.5, No.1/2, pp.31 - 54

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2014.059594

 

Available online 02 Mar 2014

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article