I am happy to announce that the following paper has just been published in Vol. 5 of the International Journal on Critical Computer-based Systems:

LTL Translation Improvements in Spot 1.0 Alexandre Duret-Lutz (LRDE/EPITA)

This is an extended version of my VECOS'11 paper, that was submitted to IJCCBS in October 2012, accepted in April 2013, and published in March 2014.

https://www.lrde.epita.fr/wiki/Publications/duret.14.ijccbs

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 favor 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.