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.
@TechReport{src_1999_interns,
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:// www.wischik.com/ lu/ research/ verify-tla-report.html",
}