Definition. Finite completed trace semantics for CCS with \textbf {1} [pa-0007]
We offer a denotational semantics for CCS augmented with a \textbf {1} constant, denoting successful termination. Unlike our partial trace semantics, this semantics only includes finite completed traces — traces where the process has terminated.
\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {CT} & = & \emptyset \\ \llbracket \textbf {1} \rrbracket _\text {CT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {CT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {CT} \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {CT} & = & \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {CT} \\ \llbracket P|Q \rrbracket _\text {CT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {CT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {CT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {CT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {CT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {CT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {CT} \} \end {array}The trace merge operator \bowtie is defined exactly as in the partial trace semantics.