Abstract: |
We formalize linear-time temporal logic (LTL) and the algorithm by Gerth
et al. to convert LTL formulas to generalized Büchi automata.
We also formalize some syntactic rewrite rules that can be applied to
optimize the LTL formula before conversion.
Moreover, we integrate the Stuttering Equivalence AFP-Entry by Stefan
Merz, adapting the lemma that next-free LTL formula cannot distinguish
between stuttering equivalent runs to our setting.
We use the Isabelle Refinement and Collection framework, as well as the
Autoref tool, to obtain a refined version of our algorithm, from which
efficiently executable code can be extracted. |
BibTeX: |
@article{LTL_to_GBA-AFP,
author = {Alexander Schimpf and Peter Lammich},
title = {Converting Linear-Time Temporal Logic to Generalized Büchi Automata},
journal = {Archive of Formal Proofs},
month = may,
year = 2014,
note = {\url{http://isa-afp.org/entries/LTL_to_GBA.html},
Formal proof development},
ISSN = {2150-914x},
}
|