Definition. Operational semantics for (non-recursive) CCS [pa-0002]

We assign an operational semantics to CCS by describing a series of transition rules P \xrightarrow {a} Q inductively as follows:

\begin {gather*} \dfrac { }{a.P \xrightarrow {a} P} \quad \dfrac {P_k \xrightarrow {a} P'}{\sum _{i \in I} P_i \xrightarrow {a} P'} \\[2em] \dfrac { P \xrightarrow {a} P'}{P|Q \xrightarrow {a} P'|Q} \quad \dfrac { Q \xrightarrow {a} Q'}{P|Q \xrightarrow {a} P|Q'} \dfrac { P \xrightarrow {a} P' \quad Q \xrightarrow {\overline {a}} Q'}{P|Q \xrightarrow {\tau } P'|Q'} \\[2em] \dfrac { P \xrightarrow {a} P' \quad a \notin \{\alpha , \overline {\alpha }\}}{ P\setminus \alpha \xrightarrow {a} P' \setminus \alpha } \quad \dfrac { P \xrightarrow {a} P'}{ P [ f ] \xrightarrow {f(a)} P' [ f ]} \end {gather*}

Let the relation P \xrightarrow {\sigma }^\ast Q denote the reflexive, transitive closure of the above step relation, where \sigma denotes a finite trace (a finite sequence of actions):

\dfrac { }{P \xrightarrow {\varepsilon }^\ast P} \quad \dfrac {P \xrightarrow {a} P' \quad P' \xrightarrow {\sigma }^\ast Q}{P \xrightarrow {a\sigma }^\ast Q}