Abstract
In the transition axiom method, safety properties of a concurrent system can
be specified by programs; liveness properties are specified by assertions
in a simple temporal logic. The method is described with some simple examples,
and its logical foundation is informally explored through a careful examination
of what it means to implement a specification. Language issues and other
practical details are largely ignored.
