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