README.html
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>
15is a linear-time temporal logic introduced by Leslie Lamport in
16<EM>The Temporal Logic of Actions</EM> (ACM TOPLAS 16(3), 1994,
17872-923). Unlike other temporal logics, both systems and properties
18are represented as logical formulas, and logical connectives such as
19implication, conjunction, and existential quantification represent
20structural relations such as refinement, parallel composition, and
21hiding. 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
39Please consult the
40<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
41for further information regarding the setup and use of this encoding
42of TLA.
43
44<P>
45The 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 -->
66Last modified: Sat Mar 5 00:54:49 CET 2005
67<!-- hhmts end -->
68</BODY></HTML>
69