Email Gateway (Aug 18 2022 at 18:46): Email Gateway (Aug 18 2022 at 18:46):From: Tobias Nipkow <nipkow@in.tum.de>
A Definitional Encoding of TLA* in Isabelle/HOL
Gudmund Grov and Stephan Merz
http://afp.sourceforge.net/entries/TLA.shtml
We mechanise the logic TLA*, an extension of Lamport's Temporal Logic of
Actions (TLA) for specifying
and reasoning about concurrent and reactive systems. Aiming at a
framework for mechanising the verification
of TLA (or TLA*) specifications, this contribution reuses some elements
from a
previous axiomatic encoding of TLA in Isabelle/HOL by the second author,
which has been part of the
Isabelle distribution. In contrast to that previous work, we give here a
shallow, definitional
embedding, with the following highlights:
a theory of infinite sequences, including a formalisation of the
concepts of stuttering invariance central to TLA and TLA*;
a definition of the semantics of TLA*, which extends TLA by a
mutually-recursive definition of formulas and pre-formulas, generalising
TLA action formulas;
a substantial set of derived proof rules, including the TLA* axioms
and Lamport's proof rules for system verification;
a set of examples illustrating the usage of Isabelle/TLA* for
reasoning about systems.
Note that this work is unrelated to the ongoing development of a proof
system for the specification language TLA+,
which includes an encoding of TLA+ as a new Isabelle object logic.
Enjoy!
Last updated: Apr 25 2024 at 20:15 UTC