←

Back

High-Level View

News

ccc

→

My Papers About TLA and TLA+

Leslie Lamport

Last modified on 30 November 2018

You'll miss a lot on this web site unless you enable Javascript in your browser.

What's Here [hide]

This page lists approximately every paper I've published or perhaps should have published about TLA and TLA+. Newer papers are in reverse chronological order and have links to my publication page. Older papers are in chronological order with an index and self-contained descriptions. The boundary between older and newer is the turn of the millenium.

Newer Papers [show]

Auxiliary Variables in TLA+: Auxiliary variables are added to a spec to permit the definition of a refinement mapping under which a specification implements a higher-level specification. This paper explains how to add them to a TLA+ spec.
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 30-page 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.
Real-Time 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 real-time 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 real-world specification.

High-Level Specifications: Lessons from Industry

A note about the use of TLA+ in industry.

Checking Cache-Coherence 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 real-world verification problem.

Older Papers [show]

The Temporal Logic of Actions
Introduction to TLA
Specifying Concurrent Systems with TLA+
A Summary of TLA+
Model Checking TLA+ Specifications
TLA+ Verification of Cache-Coherence Protocols
The Module Structure of TLA+
The Operators of TLA+
Refinement in State-Based Formalisms
Processes are in the Eye of the Beholder
Proving Possibility Properties
Win32 Threads API Specification
A TLA Solution to the RPC-Memory Specification Problem
Lazy Caching: An Assertional View
An Old-Fashioned Recipe for Real Time
Conjoining Specifications
TLA in Pictures
Hybrid Systems in TLA+
Specifying and Verifying Fault-Tolerant Systems
Verification of a Multiplier: 64 Bits and Beyond
Mechanical Verification of Concurrent Systems with TLA
TLA Notes

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) 872-923
Postscript - DVI

Introduction to TLA
Leslie Lamport

16 December 1994

A short (7-page) 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 7-page "cheat sheet" that briefly describes all the constructs and built-in operators of TLA+ and the operators defined in the common standard modules, and that lists the user-definable 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 first-order logic and ZF set theory. TLC is a new model checker for debugging a TLA+ specification by checking invariance properties of a finite-state 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), 54-66.
Postscript - DVI

TLA+ Verification of Cache-Coherence 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 cache-coherence 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 State-Based 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 two-process algorithm is shown to be equivalent to an N-process 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), 333-351.
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 linear-time 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 real-world specification looks like. It also illustrates how one can write an "object oriented" specification in TLA+.

A TLA Solution to the RPC-Memory 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 RPC-Memory Specification Case Study. Manfred Broy, Stephan Merz, and Katharina Spies editors. LNCS 1169, (1996), 21-66.
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, 151-174.
Postscript - DVI

An Old-Fashioned Recipe for Real Time
Martin Abadi and Leslie Lamport
22 December 1993

Abstract: Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability.
Appeared in ACM Toplas 16, 5 (September, 1994) 1543-1571
Postscript - DVI - LaTeX

Conjoining Specifications
Martin Abadi and Leslie Lamport
3 November 1995

This paper describes how to write and reason about open system specifications--also 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) 507-534
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: Predicate-action diagrams, which are similar to conventional state-transition 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) 768-775
Postscript - DVI - LaTeX (requires IEEEtran.sty)

There is a minor error in this paper that no-one 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 built-in primitives for specifying real-time 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 lower-level specifications implementing the next higher-level one. Correctness proofs are sketched.
Appeared in Hybrid Systems, edited by Grossman, Nerode, Ravn, and Rischel, LNCS 736.
Postscript - DVI - LaTeX

Specifying and Verifying Fault-Tolerant 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 Real-Time and Fault-Tolerant Systems. H. Langmaack, W.-P. de Roever, and J. Vytopil, editors. LNCS 863, 41-76..
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 finite-state parts of a non-finite-state verification problem for verification by a model checker.

Abstract: Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the induction principle, and bdd fixed-point algorithms. Theorem proving, while not bound by the same computational constraints, may not be feasible for routinely coping with the complex, low-level details of a real multiplier. We show how to verify such a multiplier by applying COSPAN, a model-checking algorithm, to verify local properties of the complex low-level 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, 166-179. 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 translations--one 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, 44-55.
Postscript - DVI - LaTeX

TLA Notes

A collection of rough, half-baked notes that still seem relevant, including ones sent to an old TLA mailing list.

Back