LTL Translation Improvements in Spot 1.0

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

• Paper

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}
}