| products/sources/formale sprachen/Isabelle/HOL/TLA/README.html |
 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML>
<HEAD>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<TITLE>HOL/TLA</TITLE>
</HEAD>
<BODY>
<H2>TLA: Lamport's Temporal Logic of Actions
<A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">TLA</A>
is a linear-time temporal logic introduced by Leslie Lamport in
<EM>The Temporal Logic of Actions</EM> (ACM TOPLAS 16(3), 1994,
872-923). Unlike other temporal logics, both systems and properties
are represented as logical formulas, and logical connectives such as
implication, conjunction, and existential quantification represent
structural relations such as refinement, parallel composition, and
hiding. TLA has been applied to numerous case studies.
<P>This directory formalizes TLA in Isabelle/HOL, as follows:
<UL>
<LI>Theory <A HREF="Intensional.html">Intensional</A> prepares the
ground by introducing basic syntax for "lifted", possibl-world based
logics.
<LI>Theories <A HREF="Stfun.html">Stfun</A> and
<A HREF="Action.html">Action</A> represent the state and transition
level formulas of TLA, evaluated over single states and pairs of
states.
<LI>Theory <A HREF="Init.html">Init</A> introduces temporal logic
and defines conversion functions from nontemporal to temporal
formulas.
<LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal
logic.
</UL>
Please consult the
<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
for further information regarding the setup and use of this encoding
of TLA.
<P>
The theories are accompanied by a small number of examples:
<UL>
<LI><A HREF="Inc/index.html">Inc</A>: Lamport's increment
example, a standard TLA benchmark, illustrates an elementary TLA
proof.
<LI><A HREF="Buffer/index.html">Buffer</A>: a proof that two buffers
in a row implement a single buffer, uses a simple refinement
mapping.
<LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
untimed part of) Broy and Lamport's RPC-Memory case study,
more fully explained in LNCS 1169 (the
<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
solution</A> is available separately).
</UL>
<HR>
<ADDRESS>
<A HREF="mailto:[email protected]">Stephan Merz</A>
</ADDRESS>
<!-- hhmts start -->
Last modified: Sat Mar 5 00:54:49 CET 2005
<!-- hhmts end -->
</BODY></HTML>
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
