We are happy to announce that the following paper has been accepted
for publication at the 20th International SPIN Symposium on Model
Checking of Software (SPIN'13) that will take place in Stony Brook,
NY, USA on 8-9 July 2013.
Compositional Approach to Suspension and
Other Improvements to LTL Translation
Tomáš Babiak (1), Thomas Badie (2), Alexandre Duret-Lutz (2),
Mojmír Křetínský (1), and Jan Strejček (1)
(1) Faculty of Informatics, Masaryk University, Brno, Czech Republic
(2) LRDE, EPITA, Kremlin-Bicêtre, France
http://publis.lrde.epita.fr/201307-Spin
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.
--
Alexandre Duret-Lutz