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