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