Verifying arbitrary temporal formulas in the temporal logic of actions.

Lucian Wischik. In tech note SRC-1999-003, 1999.

Note: The work described here was carried out as a summer intern at Digital's Systems Research Center. It, along with project reports from all the other interns, was published in a single technical note (available online).


"Engineers should be able to specify and verify their systems directly and conveniently in logic." This aphorism provides a pragmatic motivation for Lamport's Temporal Logic of Actions, and for the associated model-checker TLC. It also distinguishes TLC from other comparable model-checkers, where specifications must be translated into a special-purpose language.

Normally, to verify a temporal formula about a system, you would turn that formula into a finite-state-machine using the 'tableau' method of Clarke and Emmerson. Any execution-trace that passes through this machine thereby satisfies the formula. But in the Temporal Logic of Actions, the temporal logic language has been expanded to include 'actions' - i.e. transitions between states. (The standard tableau technique only deals with temporal formulas on states, not on actions).

I introduce an enhanced "action tableau" technique that can deal with actions. This new technique also unifies two aspects of temporal-verification that had previously been treated separately: the handling of fairness, and the verification of state-based temporal formulas.

  title  = "Verifying arbitrary temporal formulas in the temporal logic of actions",
  author = "Lucian Wischik",
  organization = "DEC SRC",
  number = "003",
  year   = "1999",
  note   = "In Selected 1999 SRC Summer Intern Reports, ed. James Mason",
  url    = "http:// lu/ research/ verify-tla-report.html",


  • Report in PDF format, 367k, 3 pages.
  • Slides from a talk, [paged HTML] or [continuous HTML].
  • See also

  • External link: The Temporal Logic of Actions