SRC Research Report 137

Proving Possibility Properties

Leslie Lamport

Report #137. July 4, 1995, Revised December 1, 1997

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.

Back to the SRC Research Reports main page.

Download report as:

PostScript compressed with UNIX compress -- 115 Kbytes
PostScript compressed with GNU compress (gzip) -- 88 Kbytes
PostScript compressed with ZIP -- 88 Kbytes
PostScript -- 440 Kbytes
Portable Document Format (PDF) -- 208 Kbytes