src/HOL/TLA/README.html
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 7881 1b1db39a110b
child 15283 f21466450330
permissions -rw-r--r--
improved theory reference in comment
     1 <HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY>
     2 
     3 <H2>TLA: Lamport's Temporal Logic of Actions</H2>
     4 
     5 <A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">TLA</A>
     6 is a linear-time temporal logic introduced by Leslie Lamport in
     7 <EM>The Temporal Logic of Actions</EM> (ACM TOPLAS 16(3), 1994,
     8 872-923). Unlike other temporal logics, both systems and properties
     9 are represented as logical formulas, and logical connectives such as
    10 implication, conjunction, and existential quantification represent
    11 structural relations such as refinement, parallel composition, and
    12 hiding. TLA has been applied to numerous case studies.
    13 
    14 <P>This directory formalizes TLA in Isabelle/HOL, as follows:
    15 <UL>
    16 <LI>Theory <A HREF="Intensional.html">Intensional</A> prepares the
    17   ground by introducing basic syntax for "lifted", possibl-world based 
    18   logics.
    19 <LI>Theories <A HREF="Stfun.html">Stfun</A> and
    20   <A HREF="Action.html">Action</A> represent the state and transition
    21   level formulas of TLA, evaluated over single states and pairs of
    22   states.
    23 <LI>Theory <A HREF="Init.html">Init</A> introduces temporal logic
    24   and defines conversion functions from nontemporal to temporal
    25   formulas.
    26 <LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal
    27   logic.
    28 </UL>
    29 
    30 Please consult the
    31 <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
    32 for further information regarding the setup and use of this encoding
    33 of TLA.
    34 
    35 <P>
    36 The theories are accompanied by a small number of examples:
    37 <UL>
    38 <LI><A HREF="Inc/index.html">Inc</A>: Lamport's <EM>increment</EM>
    39   example, a standard TLA benchmark, illustrates an elementary TLA
    40   proof.
    41 <LI><A HREF="Buffer/index.html">Buffer</A>: a proof that two buffers
    42   in a row implement a single buffer, uses a simple refinement
    43   mapping.
    44 <LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
    45   untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study,
    46   more fully explained in LNCS 1169 (the 
    47   <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
    48   solution</A> is available separately).
    49 </UL>
    50 
    51 <HR>
    52 
    53 <ADDRESS>
    54 <A HREF="merz@informatik.uni-muenchen.de">Stephan Merz</A>
    55 </ADDRESS>
    56 <!-- hhmts start -->
    57 Last modified: Mon Jan 25 14:06:43 MET 1999
    58 <!-- hhmts end -->
    59 </BODY></HTML>