Petri nets can be used as a basis for defining the semantics of concurrent processes a` la CCS or CSP. This paper addresses the notion of the correctness of such processes with respect to trace logic specifications. The issues discussed here are safety (communication traces of processes must satisfy the specifications), liveness (communication traces that satisfy the specifications will eventually be completed), and stability (all internal activities have ceased). Olderog asserts that trace logic–based specifications can describe only deterministic and divergence-free processes, thus limiting the scope of such techniques. He then gives a different formulation of the liveness condition, using a more abstract semantics than nets, namely the readiness semantics. Readiness semantics is based on keeping the set of communications in which a process is willing to engage after a given communication trace. Finally, this readiness semantics is shown to be fully abstract with respect to specification satisfaction equivalence.

Although well-written, this paper is not self-contained and requires a fair amount of knowledge in the area. For instance, the semantic definition of processes in terms of Petri nets is not given. Addressing many of the issues related to correctness, it should, however, be of use to theoreticians working in the area of concurrent program semantics.