LTL Translation Improvements in Spot 1.0
From LRDE
- Authors
- Alexandre Duret-Lutz
- Journal
- International Journal on Critical Computer-Based Systems
- Type
- article
- Projects
- Spot
- Date
- 2014-03-06
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.
Documents
Bibtex (lrde.bib)
@Article{ duret.14.ijccbs,
author = {Alexandre Duret-Lutz},
title = {{LTL} Translation Improvements in {S}pot 1.0},
journal = {International Journal on Critical Computer-Based Systems},
year = 2014,
volume = 5,
number = {1/2},
pages = {31--54},
month = mar,
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{\"u}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.},
doi = {10.1504/IJCCBS.2014.059594}
}