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}