Definition. Partial trace semantics for (non-recursive) CCS [pa-0003]
A simple denotational semantics for CCS is in terms of partial traces: finite sequences of actions.
\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {PT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {PT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \cup \{ \varepsilon \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {PT} & = & \{ \varepsilon \} \cup \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {PT} \\ \llbracket P|Q \rrbracket _\text {PT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {PT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {PT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {PT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {PT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {PT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \end {array}The trace merge operator \bowtie is defined as follows:
\begin {array}{lcl} \sigma \bowtie \varepsilon &=& \{\sigma \} \\ \varepsilon \bowtie \sigma &=& \{\sigma \} \\ a\sigma \bowtie b\rho &=& \{ a\varsigma \mid \varsigma \in \sigma \bowtie b\rho \} \\ &\cup & \{ b\varsigma \mid \varsigma \in a\sigma \bowtie \rho \} \\ &\cup & \{ \tau \varsigma \mid \varsigma \in \sigma \bowtie \rho \land a = \overline {b} \} \\ \end {array}