TLA - The Temporal Logic of Actions

The  TLA+  tools  are  available  here.

What is TLA?

TLA (the Temporal Logic of Actions) is a logic for specifying and reasoning about concurrent and reactive systems.   It is the basis for TLA+, a complete specification language.

This Web page will be updated to reflect new work on TLA.   I hope that all work on TLA and TLA tools will be accessible from here.   If you want to be notified of changes to this page, or if you want your work to be represented here, please send e-mail to Leslie Lamport.

About TLA and TLA+

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.

A Summary of TLA+

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)

PODC 2000 Tutorial Handout

This is the handout from the TLA+ tutorial at PODC 2000.   It will be meaningful only to people who attended the tutorial. Postscript (300K) - Compressed Postscript (170K) - PDF (120K)

The Wildfire Verification Challenge Problem

This challenge poses the problem of finding a bug in a system formally specified with TLA+.   It is also a good example of a TLA+ specification of a realistic system.

TLA Papers

The current corpus--all relevant papers and notes by Leslie Lamport and friends that are about TLA or use TLA.

Related Issues

Proofs

About writing mathematical proofs.

Useful LaTeX Style Files

For writing in and about TLA.

Should Your Specification Language Be Typed?
Leslie Lamport and Lawrence C. Paulson
1 May 1997

A discussion of types in specification languages that should explain why TLA+ is untyped. (To appear in ACM TOPLAS.)

Logic Calculators

Check it out.

Work on TLA Outside Compaq and Microsoft

Papers

"A formulation of TLA in Isabelle"-- Sara Kalvala

"Reasoning About Programs by Exploiting the Environment"-- Limor Fix and Fred B. Schneider

Links to Other Groups and Projects

Case Study in TLA+ / TLC

Examples created by Michel Charpentier for a course he gave on program verification.

Stephan Merz

A page containing several papers on TLA by Stephan Merz, as well as a link to Isabelle/TLA, Merz's encoding of TLA in the higher-order logic of the generic interactive theorem prover Isabelle. (That page includes a machine-checked proof of The Dagstuhl RPC-Memory Example.)

Work With and On TLA .

Publications by the Networks and Distributed Systems group at the University of Bielefeld, headed by Peter Ladkin

The DisCo Home Page

Disco is a specification language developed by Reino Kurki-Suonio at the University of Tampere in Finland.

Tools for TLA based specifications

This page describes work done at the University of Dortmund, Department of Computer Science by the Computer Networks and Distributed Systems group headed by Dr. Heiko Krumm.

TLP

TLP is a system for mechanically checking TLA proofs. It was developed primarily by Urban Engberg (ue@ccieurope.com) when he was a doctoral student at Aarhus University, with help from Peter Grønning. The page has not been updated since 1995, but the program should still work. (It uses an obsolete version of the LP theorem prover, which is available from the site. It also has Emacs macros that were written for an old version of Emacs and may or may not work with newer versions.) Further development of TLP is a promising research project waiting for someone to undertake it.

In 2000, this page was visited about 33500 times from 8000 different hosts.
In 1999, this page was visited about 31100 times from 8000 different hosts.
In 1998, this page was visited about 18400 times from 5300 different hosts.
In 1997, this page was visited about 19000 times from 5600 different hosts.
In 1996, this page was visited about 18800 times from 5300 different hosts. _____________________________________________________________________________________________________

This page can be found by searching the Web for the 21-letter string uidlamporttlahomepage. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamporttlahomepage".