src/HOL/TLA/README.html
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 17747 1ce1f62768bd
child 51404 90a598019aeb
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<!-- $Id$ -->

<HTML>

<HEAD>
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <TITLE>HOL/TLA</TITLE>
</HEAD>

<BODY>

<H2>TLA: Lamport's Temporal Logic of Actions</H2>

<A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">TLA</A>
is a linear-time temporal logic introduced by Leslie Lamport in
<EM>The Temporal Logic of Actions</EM> (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.

<P>This directory formalizes TLA in Isabelle/HOL, as follows:
<UL>
<LI>Theory <A HREF="Intensional.html">Intensional</A> prepares the
  ground by introducing basic syntax for "lifted", possibl-world based 
  logics.
<LI>Theories <A HREF="Stfun.html">Stfun</A> and
  <A HREF="Action.html">Action</A> represent the state and transition
  level formulas of TLA, evaluated over single states and pairs of
  states.
<LI>Theory <A HREF="Init.html">Init</A> introduces temporal logic
  and defines conversion functions from nontemporal to temporal
  formulas.
<LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal
  logic.
</UL>

Please consult the
<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
for further information regarding the setup and use of this encoding
of TLA.

<P>
The theories are accompanied by a small number of examples:
<UL>
<LI><A HREF="Inc/index.html">Inc</A>: Lamport's <EM>increment</EM>
  example, a standard TLA benchmark, illustrates an elementary TLA
  proof.
<LI><A HREF="Buffer/index.html">Buffer</A>: a proof that two buffers
  in a row implement a single buffer, uses a simple refinement
  mapping.
<LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
  untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study,
  more fully explained in LNCS 1169 (the 
  <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
  solution</A> is available separately).
</UL>

<HR>

<ADDRESS>
<A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>
</ADDRESS>
<!-- hhmts start -->
Last modified: Sat Mar  5 00:54:49 CET 2005
<!-- hhmts end -->
</BODY></HTML>