LTL Translation Improvements in Spot 1.0

From LRDE

Revision as of 09:00, 7 March 2014 by Bot (talk | contribs) (Created page with "{{Publication | published = true | date = 2014-03-06 | authors = Alexandre Duret-Lutz | title = LTL Translation Improvements in Spot 1.0 | journal = International Journal on C...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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