Editing Communicating sequential processes (section)

=== Denotational semantics ===

The three major denotational models of CSP are the ''traces'' model, the ''stable failures'' model, and the ''failures/divergences'' model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.<ref name="roscoe" />

==== Traces model ====
The ''traces model'' defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,

* <math>\mathrm{traces}\left(\mathrm{STOP}\right) = \left\{ \langle\rangle \right\}</math> since <math>\mathrm{STOP}</math> performs no events
* <math>\mathrm{traces}\left(a\rightarrow b \rightarrow \mathrm{STOP}\right) = \left\{\langle\rangle ,\langle a \rangle, \langle a, b \rangle \right\}</math> since the process <math>(a\rightarrow b \rightarrow \mathrm{STOP})</math> can be observed to have performed no events, the event {{mvar|a}}, or the sequence of events {{mvar|a}} followed by {{mvar|b}}

More formally, the traces model <math>\mathcal T</math> is defined as the set of non-empty prefix-closed subsets of <math>\Sigma^{\ast}</math>. The meaning of a process {{mvar|P}} in the traces model is defined as <math>\mathrm{traces}\left(P\right) \subseteq \Sigma^{\ast}</math> such that:
# <math>\langle\rangle \in \mathrm{traces}\left(P\right)</math> (i.e. <math>\mathrm{traces}\left(P\right)</math> contains the empty sequence)
# <math>s_1 \smallfrown s_2 \in \mathrm{traces}\left(P\right) \implies s_1 \in \mathrm{traces}\left(P\right)</math> (i.e. <math>\mathrm{traces}\left(P\right)</math> is prefix-closed)
where <math>\Sigma^{\ast}</math> is the set of all possible finite sequences of events.

==== Stable failures model ====

The ''stable failures model'' extends the traces model with refusal sets, which are sets of events <math>X \subseteq \Sigma</math> that a process can refuse to perform. A ''failure'' is a pair <math>\left(s,X\right)</math>, consisting of a trace {{mvar|s}}, and a refusal set {{mvar|X}} which identifies the events that a process may refuse once it has executed the trace {{mvar|s}}. The observed behavior of a process in the stable failures model is described by the pair <math>\left(\mathrm{traces}\left(P\right), \mathrm{failures}\left(P\right)\right)</math>. For example,

<math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \Box \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{\left(\langle\rangle,\emptyset\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>
<math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \sqcap \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>

==== Failures/divergences model ====

The ''failures/divergence model'' further extends the failures model to handle [[divergence (computer science)|divergence]]. The semantics of a process in the failures/divergences model is a pair <math>\left(\mathrm{failures}_\perp\left(P\right), \mathrm{divergences}\left(P\right)\right)</math> where <math>\mathrm{divergences}\left(P\right)</math> is defined as the set of all traces that can lead to divergent behavior and <math>\mathrm{failures}_\perp\left(P\right) = \mathrm{failures}\left(P\right) \cup \left\{\left(s,X\right) \mid s \in \mathrm{divergences}\left(P\right)\right\}</math>.

==== Unique fixed points ====
One of the most important principles in CSP is the Unique Fixed Points (UFP) rule. A version for single recursions in the traces model states that if <math>F : \mathcal T \rightarrow \mathcal T</math> is a function on trace sets generated by the guarded recursive{{clarify|date=April 2025}} process <math>X</math>, and <math>Y</math> is a process where <math>\mathrm{traces}(Y)</math> is a [[fixed point (mathematics)|fixed point]] of <math>F</math>, then <math>X</math> is equivalent to <math>Y</math> in the traces model.<ref name="ucs"/> UFP can also be extended to mutual recursions and other models of CSP.