Compositional Approach to Suspension and Other Improvements to LTL Translation

Authors

Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček

Where

Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN'13)

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2013-04-28

Abstract

Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  babiak.13.spin,
  author	= {Tom{\'a}{\v{s}} Babiak and Thomas Badie and Alexandre
		  Duret-Lutz and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Jan
		  Strej{\v{c}}ek},
  title		= {Compositional Approach to Suspension and Other
		  Improvements to {LTL} Translation},
  booktitle	= {Proceedings of the 20th International SPIN Symposium on
		  Model Checking of Software (SPIN'13)},
  year		= 2013,
  volume	= 7976,
  series	= {Lecture Notes in Computer Science},
  pages		= {81--98},
  month		= jul,
  publisher	= {Springer},
  doi		= {10.1007/978-3-642-39176-7_6},
  abstract	= {Recently, there was defined a fragment of LTL (containing
		  fairness properties among other interesting formulae) whose
		  validity over a given infinite word depends only on an
		  arbitrary suffix of the word. Building upon an existing
		  translation from LTL to B{\"u}chi automata, we introduce a
		  compositional approach where subformulae of this fragment
		  are translated separately from the rest of an input formula
		  and the produced automata are composed in a way that the
		  subformulae are checked only in relevant accepting strongly
		  connected components of the final automaton. Further, we
		  suggest improvements over some procedures commonly applied
		  to generalized B{\"u}chi automata, namely over generalized
		  acceptance simplification and over degeneralization.
		  Finally we show how existing simulation-based reductions
		  can be implemented in a signature-based framework in a way
		  that improves the determinism of the automaton.}
}