[isabelle] New AFP entry: A Definitional Encoding of TLA* in Isabelle/HOL

A Definitional Encoding of TLA* in Isabelle/HOL
Gudmund Grov and Stephan Merz

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.