TLA NOTES

Last modified 5 January 2019
This is a collection of material about TLA (Temporal Logic of Actions) and specification in general that may be of interest, but has not appeared in a real paper. These notes are rough and half-baked; they probably contain many errors. But, they provide the only available information on several important topics.

The notes marked "LaTeX/ASCII" can be read in ASCII or run through LaTeX to get a somewhat more readable version. To run them through LaTeX, you need the style file spec92.sty. You can click here for an explanation of the ASCII conventions that are used.

A Completeness Theorem for TLA
17 November 1993, LaTeX formatting corrected 5 January 2019
A relative completeness theorem for TLA, with its proof. The first part was distributed to the TLA mailing list. For intrepid souls only.
LaTeX/ASCII     pdf version

Types Considered Harmful
Leslie Lamport
23 December 1992
A brief explanation of how to do mathematics without types. (10 pages)
Postscript - DVI - LaTeX

Using Tense Logic in Specification and Verification
Peter Ladkin
5 August 1993
These are Peter Ladkin's comments on the question of using first-order logic rather than TLA. (Sent to TLA mailing list.)
LaTeX/ASCII

Miscellany
21 June 1993
Contains "Some Thoughts on Specification" (a short, not-too-hot flame), "Thinking About Actions Instead of States" (of interest to people who want to write TLA specs), "Encoding TLA in Ordinary Math" (required reading for anyone involved in mechanizing TLA), and "A New TLA+ Construct" (for aficionados of TLA+). (Sent to TLA mailing list.)
LaTeX/ASCII

Some Thoughts on Specification
5 May 1992
Some philosophical musings about specification. (Sent to TLA mailing list.)
ASCII

The Reduction Theorem
12 April 1992
The Reduction Theorem allows one to prove things about a fine-grained specification by reasoning about a coarser-grained one. This may be a crucial result for carrying verification down to the level of executable code. (Sent to TLA mailing list.)
LaTeX/ASCII

The Existence of Refinement Mappings
19 March 1992
An attempt to redo the paper of the same name in TLA. It contains mistakes, and there should soon be a paper that does this. (Sent to TLA mailing list.)
LaTeX/ASCII

Miscellany
4 April 1991
Contains a discussion of why breaking closed systems into open components makes for more work, and a representation of the closure and realizable-part operators in TLA. (Sent to TLA mailing list.)
ASCII

Philosophical Hogwash
15 November 1990
Some musings sent to the concurrency mailing list in response to a message from Vaughan Pratt. (Sent to TLA mailing list.)
ASCII