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