TLA Papers
TLA Papers
Last modified 24 September 2012
This page lists approximately all the papers written by Leslie Lamport
that are relevant to TLA (the Temporal Logic of
Actions) and TLA+. The section on newer papers lists ones written
in this millenium, and contains pointers to the papers' entries on
Leslie Lamport's publication page. Earlier papers are
listed below in the
section on older papers.
Newer Papers
This is a list of pointers to papers on
Leslie Lamport's publication page
that are relevant to learning about
TLA (the Temporal Logic of Actions) and TLA+.

How to Write a 21st Century Proof

Written primarily for mathematicians, this provides an introduction
to the kind of hierarchical proofs supported by the TLA+ language
and checked by
TLAPS
(the TLA+ Proof System).

Euclid Writes an Algorithm: A Fairytale

This is a short, whimsical introduction to TLA, TLA+, and TLA proofs.

Byzantizing Paxos by Refinement

This contains an informal description of a significant proof that
was done with
TLAPS,
and a pointer to the complete proof.

Computer Science and State
Machines

This is a very brief note that explains the basic idea that inspired TLA.

Teaching Concurrency

Another short note that I don't think mentions TLA, but that should
be of interest to anyone who teaches basic computer science.

Computation and State Machines
 This is a 30page paper that explains in detail the ideas behind the
preceding paper, Teaching Concurrency.

Leslie
Lamport: The Specification Language TLA+

A brief note, mostly about the history behind TLA and TLA+.

TLA+

This is a book chapter I was asked to write containing a TLA+ solution to
an uninteresting specification problem. It contains some comments about
the specification process that may be of interest.

The PlusCal Algorithm Language

This is the best place to learn about
the PlusCal algorithm language.
It complements the language manual.

Checking a Multithreaded Algorithm with +CAL

A case study of using PlusCal and the TLC model checker.

RealTime Model Checking is Really
Simple

This is an abridged version of the following paper.

Real Time is Really Simple

This is a good place to find out about using TLA+ in practice for checking
realtime algorithms.

Implementing and Combining Specifications

A note that may be helpful in learning to write real specifications.
Formal Specification of a Web Services
Protocol
A paper about a simple realworld specification.
HighLevel Specifications: Lessons from
Industry
A note about the use of TLA+ in industry.
Checking CacheCoherence Protocols with TLA+
Another industrial research report.
Specifying Systems: The TLA+
Language and Tools for Hardware and Software Engineers
The TLA+ book.
Specifying and Verifying Systems with TLA+
A description of early experience using TLA+ and the TLC model checker.
The Wildfire Challenge Problem
A nice example of a simplified realworld verification problem.

The Temporal Logic of Actions
Leslie Lamport
30 April 1994
 This is the basic TLA reference, introducing the logic and
proof rules.
Abstract:
The temporal logic of actions (TLA) is a logic for specifying and
reasoning about concurrent systems. Systems and their properties are
represented in the same logic, so the assertion that a system meets its
specification and the assertion that one system implements another are
both expressed by logical implication. TLA is very simple; its syntax
and complete formal semantics are summarized in about a
page. Yet, TLA is not just a logician's toy; it is extremely powerful,
both in principle and in practice. This report introduces TLA and
describes how it is used to specify and verify concurrent algorithms.
The use of TLA to specify and reason about open systems will be
described elsewhere. (51 pages)
Appeared in ACM Toplas 16, 3 (May 1994) 872923
Postscript 
DVI

Introduction to TLA
Leslie Lamport 
16 December 1994
 A short (7page) introduction
to what TLA formulas mean.
It should allow you to understand TLA specifications.

Specifying Concurrent Systems with TLA+
Leslie Lamport
3 March 1999
 A complete introduction to writing
TLA+ specifications. It is intended for engineers with no background
in TLA or formal methods. It includes an explanation of almost all
the constructs of TLA+. (65 pages)
Appeared in Calculational System
Design. M. Broy and R. Steinbrüggen, editors.
Postscript 
DVI

A Summary of TLA+
Leslie Lamport
6 June 2000
 This is a 7page "cheat sheet" that briefly describes all the
constructs and builtin operators of TLA+ and the operators defined in
the common standard modules, and that lists the userdefinable
operator symbols and the ascii representations of symbols.
Postscript (300K) 
Compressed Postscript (170K) 
PDF (120K)
Model Checking TLA+ Specifications
Yuan Yu, Panagiotis Manolios, and Leslie Lamport
5 March 1999
Describes TLC, the model checker for TLA+ specifications
written mostly by Yuan Yu.
Abstract: TLA+ is a specification language for concurrent and
reactive
systems that combines the temporal logic TLA with full firstorder
logic and ZF set theory. TLC is a new model checker for debugging a
TLA+ specification by checking invariance properties of a
finitestate model of the specification. It accepts a subclass of
TLA+ specifications that should include most descriptions of real
system designs. It has been used by engineers to find errors in the
cache coherence protocol for a new Compaq multiprocessor. We
describe TLA+ specifications and their TLC models, how TLC works,
and our experience using it. In Charme '99.
(12 pages)
Appeared in Correct Hardware Design and Verification Methods
(CHARME'99), Laurence Pierre and Thomas Kropf editors.
Lecture Notes in Computer Science number 1703 (1999), 5466.
Postscript 
DVI
TLA+ Verification of CacheCoherence Protocols
Homayoon Akhiani, Damien Doligez, Paul Harter,
Leslie Lamport, Mark Tuttle, and Yuan Yu
10 February 1999
Describes two projects to use TLA+ to formally specify and verify
cachecoherence protocols for multiprocessor computers being
built at Compaq. (20 pages)
Postscript 
DVI
The Module Structure of TLA+
12 September 1996
An html document that informally describes the revised syntax and
semantics for the module structure of TLA+. This is a preliminary
draft; there have been a few minor changes to TLA+ since this was written.
(About 15 pages)
The
Operators of TLA+
12 April 1997
This document is an introduction to the syntax and semantics of
the operators of TLA+. It assumes that you are familiar with ordinary
mathematics (sets and functions) and are at least acquainted with TLA.
It should enable you to understand the expressions that appear in TLA+
specifications. Most of this information appears in
Specifying Concurrent Systems with TLA+,
with a couple of very minor changes. (20 pages)
Refinement in StateBased Formalisms
18 December 1996
A note explaining what refinement and dummy variables
are all about. It also sneaks in an introduction to
TLA. (7 pages)
Processes are in the Eye of the Beholder
Leslie Lamport
16 January 1996
An illustration of the power of TLA for transforming
algorithms.
A twoprocess algorithm is shown to be equivalent to an Nprocess
one, illustrating the insubstantiality of processes. A completely
formal equivalence proof in TLA (the Temporal Logic of Actions) is
sketched.
Appeared in Theoretical Computer Science, 179
(1997), 333351.
Postscript 
DVI 
LaTeX
Proving Possibility Properties
Leslie Lamport
4 July 1995
Abstract: A method is described for proving
"always possibly" properties of specifications in formalisms with
lineartime trace semantics. It is shown to be relatively complete for
TLA (Temporal Logic of Actions) specifications.
To appear in Theoretical Computer Science
Postscript 
DVI 
LaTeX
Win32 Threads API
Specification
14 May 1996
A preliminary, unfinished TLA+ specification of the kernel
threads procedures from the Windows Win32 Application Programming
Interface (API). Win32 is the API for the Windows 95 and Windows NT
operating systems. This document shows what a realworld
specification looks like. It also illustrates how one can
write an "object oriented" specification in TLA+.
A TLA Solution to the RPCMemory Specification Problem
Martín Abadi, Leslie Lamport, and Stephan Merz
16 January 1996
Presents a TLA solution to a specification and verification problem
proposed at a Dagstuhl workshop. (45 pages, with
index)
Appeared in Formal Systems Specification: The RPCMemory
Specification Case Study. Manfred Broy,
Stephan Merz, and Katharina Spies editors.
LNCS 1169, (1996), 2166.
LaTeX 
Postscript 
DVI
Click here for more information.
Lazy Caching in TLA
Peter Ladkin, Leslie Lamport, Bryan Olivier, and Denis Roegel
8 February 1999
We address the problem, proposed by Gerth, of verifying that the
simplified version of the lazy caching algorithm of Afek, Brown, and
Merritt, described
informally in

Verifying Sequential Consistent Memory Problem Definition
Rob Gerth
April 1993
Postscript
is sequentially consistent. We specify the algorithm and
sequential consistency in TLA+, a formal specification language based
on TLA (the Temporal Logic of Actions). We then describe a formal
correctness proof in TLA. (50 pages)
Appeared in Distributed Computing 12, 2/3, 1999, 151174.
Postscript 
DVI
An OldFashioned Recipe for Real Time
Martin Abadi and Leslie Lamport
22 December 1993
Abstract:
Traditional methods for specifying and reasoning about concurrent
systems work for realtime systems. Using TLA (the temporal logic of
actions), we illustrate how they work with the examples of a queue and
of a mutualexclusion protocol. In general, two problems must be
addressed: avoiding the realtime programming version of Zeno's
paradox, and coping with circularities when composing realtime
assumption/guarantee specifications. Their solutions rest on
properties of machine closure and realizability.
Appeared in ACM Toplas 16, 5 (September, 1994) 15431571
Postscript 
DVI 
LaTeX
Conjoining Specifications
Martin Abadi and Leslie Lamport
3 November 1995
This paper describes how to write and reason about open system
specificationsalso known as
rely/guarantee specifications. It is rather hard going,
but Section 2 gives a simple introduction to the issues.
Abstract:
We show how to specify components of concurrent systems. The
specification of a system is the conjunction of its components'
specifications. Properties of the system are proved by reasoning
about its components. We consider both the decomposition of a given
system into parts, and the composition of given parts to form a
system.
Appeared in ACM Toplas 17, 3 (May, 1995) 507534
Postscript 
DVI 
LaTeX
(requires acmtrans.sty)
TLA in Pictures
Leslie Lamport
31 August 1994
Other formalisms and informalisms no longer have all the
fun. Now, you can draw pictures of TLA specifications.
Abstract:
Predicateaction diagrams, which are similar to conventional
statetransition diagrams, are defined as representations of formulas
in the temporal logic of actions (TLA). These diagrams can be used to
express formal properties of specifications and to illustrate
correctness proofs. (8 large pages)
Appeared in IEEE Transactions on Software Engineering 21,
9, (September 1995) 768775
Postscript 
DVI 
LaTeX (requires
IEEEtran.sty)
There is a minor error in this paper that noone else seems
to have noticed.
Hybrid Systems in TLA+
Leslie Lamport
6 April 1993
Here is the famous gas burner of Ravn, Rischel, and Hansen
done in TLA+. This paper shows how to formally specification and
reason about solutions to integral (as in integral calculus)
equations.
Abstract:
\TLA+ is a general purpose, formal specification language based on the
Temporal Logic of Actions, with no builtin primitives for specifying
realtime properties. Here, we use \TLA+ to define operators for
specifying the temporal behavior of physical components obeying
integral equations of evolution. These operators, together with
previously defined operators for describing timing constraints, are
used to specify a toy gas burner introduced by Ravn, Rischel, and
Hansen. The burner is specified at three levels of abstraction, each
of the two lowerlevel specifications implementing the next
higherlevel one. Correctness proofs are sketched.
Appeared in Hybrid Systems, edited by
Grossman, Nerode, Ravn, and Rischel, LNCS 736.
Postscript 
DVI 
LaTeX
Specifying and Verifying FaultTolerant Systems
Leslie Lamport and Stephan Merz
14 October 1994
Abstract: We formally specify a well known solution to the
Byzantine generals problem and give a rigorous, hierarchically
structured proof of its correctness. We demonstrate that this is
an engineering exercise, requiring no new scientific ideas.
Appeared in Formal Techniques in RealTime and FaultTolerant
Systems. H. Langmaack, W.P. de Roever, and J. Vytopil,
editors. LNCS 863, 4176..
Postscript 
DVI 
LaTeX
Verification of a Multiplier: 64 Bits and Beyond
R. P. Kurshan and Leslie Lamport
14 April 1993
This is the first application of a general method, described in
"Conjoining Specifications", for
splitting off finitestate parts of a nonfinitestate verification
problem for verification by a model checker.
Abstract:
Verifying a 64bit multiplier has a computational complexity that puts
it beyond the grasp of current finitestate algorithms, including
those based upon homomorphic reduction, the induction principle, and
bdd fixedpoint algorithms. Theorem proving, while not bound by the
same computational constraints, may not be feasible for routinely
coping with the complex, lowlevel details of a real multiplier. We
show how to verify such a multiplier by applying COSPAN, a
modelchecking algorithm, to verify local properties of the complex
lowlevel circuit, and using TLP, a theorem prover based on the
Temporal Logic of Actions, to prove that these properties imply the
correctness of the multiplier. Both verification steps are automated,
and we plan to mechanize the translation between the languages of TLP
and COSPAN.
Appeared in Proceedings of the Fifth International Conference,
CAV'93. LNCS 697, 166179.
Postscript 
DVI 
LaTeX
Mechanical Verification of Concurrent Systems with TLA
Urban Engberg, Peter Groenning, and Leslie Lamport
14 September 1992
This describes a now obsolete version of TLP, the mechanical
verification system based primarily on LP.
Abstract:
We describe an initial version of a system for mechanically checking
the correctness proof of a concurrent system. Input to the system
consists of the correctness properties, expressed in TLA (the temporal
logic of actions), and their proofs, written in a humanly readable,
hierarchically structured form. The system uses a mechanical verifier
to check each step of the proof, translating the step's assertion into
a theorem in the verifier's logic and its proof into instructions for
the verifier. Checking is now done by LP (the Larch Prover),
using two different translationsone for action reasoning and one
for temporal reasoning. The use of additional mechanical verifiers is
planned. Our immediate goal is a practical system for mechanically
checking proofs of behavioral properties of a concurrent system; we
assume ordinary properties of the data structures used by the system.
Appeared in Proceedings of the Fourth International Conference,
CAV'92. LNCS 663, 4455.
Postscript 
DVI 
LaTeX
TLA Notes
A collection of rough, halfbaked notes, including
the ones sent to the TLA mailing list that still
seem relevant.