Alexander Schimpf – Publications
(Show all abstracts)
(Hide all abstracts)
2009
-
Alexander Schimpf, Stephan Merz and Jan-Georg Smaus.
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.
In
Stefan Berghofer and Tobias Nipkow and Christian
Urban and Makarius Wenzel (ed.),
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics
(TPHOLs 2009), pp. 424-439.
Springer-Verlag 2009.
(Show abstract)
(Hide abstract)
(BIB)
We present the implementation of a translation of LTL formulae into
automata in Isabelle/HOL, which is an essential component of LTL
model checking algorithms. In automaton-based model checking, we
have a system modelled as a transition system and a correctness
property stated as a temporal (in our case: LTL) formula.
Such a formula can be translated into a (generalised) Büchi
automaton that accepts precisely those behaviours allowed by the
formula. Checking correctness of the system thus amounts to a
language inclusion property between the two automata. We implemented
a standard translation algorithm due to Gerth et al. The
correctness and termination of our implementation is shown in
Isabelle/HOL, and executable code is generated using the
Isabelle/HOL code generator.
