In: Theoretical Computer Science, Vol. 80, No. 2, pages 263-288. March 1991.
Abstract: A new notion of correctness for concurrent processes is introduced. It is a relationship between process terms built up from operators of CCS, CSP and COSY and logical formulas specifying sets of finite communication sequences. The definitions are based on a Petri net semantics for process terms. The main point is that a simple liveness property of the involved nets is required. Process correctness determines a new semantic model for process terms and logical formulas. It is a modification of the readiness semantics. The modified readiness equivalence is closely related to failure equivalence and strong testing equivalence.
Keywords: correctness (of) concurrent process(es); process term; CCS; CSP; COSY; logic; communication sequence; net semantics; liveness; readiness semantics; readiness equivalence; strong testing equivalence; failure equivalence.