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