The author discusses the use of temporal logic for specifying concurrent systems. In particular, he addresses the problems that are being encountered in the search for sufficiently abstract semantics for these systems.

The temporal formulae are interpreted in models based on state sequences and moments in time; this is an example of discrete linear-time semantics. This approach is worked out for a simple program notation in which all parallel parts are independent. The author shows how the method could be extended to accommodate communicating processes or shared variables.

The section ‘Some trouble with abstraction’ is interesting. A semantics is called fully abstract when two programs have the same semantic meaning if and only if no environment can distinguish them. The author’s linear discrete temporal logic cannot provide fully abstract semantics with respect to all desired levels of abstraction; for example, it has problems with stuttering (equal states at successive moments in time). Three approaches are mentioned that may remedy this. Two of these have been proposed by others, and one--the introduction of dense time--is the author’s.

Judging by the contents of the introductory section, which discusses the importance of formalism, the author addresses an audience that is not very familiar with temporal logic. It is questionable, however, whether the paper succeeds in this respect. Many readers may find the paper too technical and terse to convey its message. Initiated readers will appreciate the different efforts to find fully abstract semantics.