Explicit termination for (non-recursive) CCS [pa-0005]
We add to syntax of CCS an additional process constant, \textbf {1}, which, like \mathbf {0}, has no rules in the operational semantics, and whose finite partial traces are just \llbracket \textbf {1} \rrbracket _\text {PT} = \{\varepsilon \}.
The difference between \textbf {0} and \textbf {1} only comes in once we introduce a notion of possible successful termination. Intuitively, we want the ability to denote when it is OK for a process to stop.
DefinitionPossible termination predicate for CCS with \textbf {1} [pa-0006]
We define an inductive judgement P \checkmark , where P is a process in CCS augmented with an additional process constant \textbf {1}:
\begin {gather*} \dfrac { }{ \textbf {1} \checkmark } \quad \dfrac {P_k \checkmark }{\sum _{i \in I} P_i \checkmark } \\[2em] \dfrac { P \checkmark \quad Q \checkmark }{P|Q \checkmark } \dfrac { P \checkmark }{ P\setminus \alpha \checkmark } \quad \dfrac { P \checkmark }{ P [ f ] \checkmark } \end {gather*}DefinitionFinite 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.
TheoremSoundness and adequacy of finite completed trace semantics for CCS [pa-0008]
The finite completed trace semantics of CCS gives exactly those finite partial traces reachable via the operational semantics that end in a terminating state.
\llbracket P \rrbracket _\text {CT} = \{ \sigma \mid \exists Q.\ P \xrightarrow {\sigma }^\ast Q \land Q \checkmark \}Proof.
Proved by induction on P.
DefinitionA translation to turn partial traces into completed traces [pa-0009]
Define a syntactic transformation on CCS terms (augmented with \textbf {1}) \Upsilon as follows:
\begin {array}{lcl} \Upsilon (\textbf {0}) &=& \textbf {1} \\ \Upsilon (\textbf {1}) &=& \textbf {1} \\ \Upsilon (a.P) &=& \textbf {1} + a.\Upsilon (P) \\ \Upsilon (\sum _{i \in I} P_i) &=& \textbf {1} + \sum _{i \in I} \Upsilon (P_i) \\ \Upsilon (P | Q) &=& \Upsilon (P) | \Upsilon (Q)\\ \Upsilon (P \setminus \alpha ) &=& \Upsilon (P) \setminus \alpha \\ \Upsilon (P [ f ]) &=& \Upsilon (P) [ f ] \end {array}TheoremCorrectness of the \Upsilon translation [pa-000A]
Our syntactic transformation \Upsilon gives a process whose completed traces are the same as the partial traces of the original process.
\llbracket P \rrbracket _\text {PT} = \llbracket \Upsilon (P) \rrbracket _\text {CT}Proof.
A very straightforward structural induction on P, where each case follows from the definitions.