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