TLA (the temporal logic of actions) is a simple logic for describing and reasoning about concurrent systems. It provides a uniform way of specifying algorithms and their correctness properties, as well as rules for proving that one specification satisfies another. TLA+ is a formal specification language based on TLA, and TLC is a model checker for TLA+ specifications. TLA+ and TLC have been used to specify and check high-level descriptions of real, complex systems. Because TLA+ provides the full power of ordinary mathematics, it permits simple, straightforward specifications of the kinds of algorithms presented at PODC.
This tutorial will try to convince you to describe your algorithms in TLA+. You will then be able to check them with TLC and use TLA to prove their correctness as formally or informally as you want. (However, TLA proofs do have one disadvantage that is mentioned below.) The tutorial will describe TLA+ through examples and demonstrate how to use TLC. No knowledge of TLA is assumed.
TLA does have the following disadvantages:
Some researchers may find these drawbacks insurmountable.
Leslie Lamport was a member of the program committee for the first PODC conference. By 1990, he knew so little about the subject that he was unable to write the chapter on distributed computing in the Handbook of Theoretical Computer Science by himself. His knowledge eventually diminished enough to qualify him for membership in the National Academy of Engineering.
Last modified: July 24, 2000