TLA: Lamport's Temporal Logic of Actions

TLA is a linear-time temporal logic introduced by Leslie Lamport in The Temporal Logic of Actions (ACM TOPLAS 16(3), 1994, 872-923). Unlike other temporal logics, both systems and properties are represented as logical formulas, and logical connectives such as implication, conjunction, and existential quantification represent structural relations such as refinement, parallel composition, and hiding. TLA has been applied to numerous case studies.

This directory formalizes TLA in Isabelle/HOL, as follows:

Please consult the design notes for further information regarding the setup and use of this encoding of TLA.

The theories are accompanied by a small number of examples:

Stephan Merz
Last modified: Sat Mar 5 00:54:49 CET 2005