Possible and Guaranteed Concurrency in CSP

As part of an effort to give a "truly concurrent" semantics to process algebra, we propose a framework of refinements of the failures model for CSP with concurrency, conflict and causality relations on traces. These relations are defined by induction over syntax of CSP processes. We study in detail two new semantics: the possible concurrency (where two traces are said to be concurrent if they may be observations of the same concurrent run) and the possible conflict (two traces are said to be in conflict if they may be observations of two different runs). The guaranteed concurrency is obtained from the possible conflict semantics. Although the expansion law is necessarily weakened to an inequality, we show that most of the CSP laws are preserved, the exception being the idempotency of choice for the possible conflict refinement. Finally, we show that our semantics is well-founded by demonstrating a strong connection with the existing event structures semantics for CSP. The latter result..