|
15283
|
1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
|
2 |
|
|
15582
|
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>
|
|
3807
|
13 |
|
|
6255
|
14 |
<H2>TLA: Lamport's Temporal Logic of Actions</H2>
|
|
3807
|
15 |
|
|
6255
|
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.
|
|
3807
|
24 |
|
|
6255
|
25 |
<P>This directory formalizes TLA in Isabelle/HOL, as follows:
|
|
3807
|
26 |
<UL>
|
|
6255
|
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.
|
|
3807
|
39 |
</UL>
|
|
|
40 |
|
|
6255
|
41 |
Please consult the
|
|
7881
|
42 |
<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
|
|
6255
|
43 |
for further information regarding the setup and use of this encoding
|
|
|
44 |
of TLA.
|
|
3807
|
45 |
|
|
6255
|
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
|
|
7881
|
58 |
<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
|
|
6255
|
59 |
solution</A> is available separately).
|
|
|
60 |
</UL>
|
|
|
61 |
|
|
|
62 |
<HR>
|
|
|
63 |
|
|
|
64 |
<ADDRESS>
|
|
17747
|
65 |
<A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>
|
|
6255
|
66 |
</ADDRESS>
|
|
|
67 |
<!-- hhmts start -->
|
|
15582
|
68 |
Last modified: Sat Mar 5 00:54:49 CET 2005
|
|
6255
|
69 |
<!-- hhmts end -->
|
|
15283
|
70 |
</BODY></HTML>
|