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