Properties of concurrent computation

• Non-termination: the program(s) may not terminate, and additionally the output of a program may not be the focus of the computation
• Parallelism: steps of computation can occur simultaneously
• Interference: the meaning of a program may depend on the behaviour of other programs that are being executed
• Non-determinism: the same computations do not always produce the same results

The calculus of communicating systems (CCS)

Milner’s general model:

• A concurrent system is a collection of processes
• A process is an independent agent that may perform internal activities in isolation, or may interact with the environment to perform shared activities

Example of CCS

A vending machine can be represented as follows: $\text{coke.coin.}\overline{\text{coke\_can}}\text{.0}+\text{chocolate.coin.}\overline{\text{chocolate\_bar}}\text{.0}$

With the following syntax:

1. Actions: $\text{coke}$, $\overline{\text{coke\_can}}$, $\dots$
2. Sequential composition: . (the dot)
3. Non-deterministic choice: +
4. Terminal process: $0$

Processes perform actions (${\to }^{\text{action}}$) and become a new process: \begin{aligned}\textsf{coke.coin.}\overline{\textsf{coke\_can}}.0 + \textsf{chocolate.coin.}\overline{\textsf{chocolate\_bar}}.0 &\rightarrow^\textsf{coke} \textsf{coin.}\overline{\textsf{coke\_can}}.0 \\ &\rightarrow^\textsf{coin} \overline{\textsf{coke\_can}}.0 \\ &\rightarrow^\overline{\textsf{coke\_can}} 0 \end{aligned}

Syntax

The simplest possible process is a terminal process, represented by $0$, which is a terminated, inactive, or deadlocked process.

A set of labels for actions: $\mathcal{A}=\mathcal{N}\cup \bar{\mathcal{N}}\cup \{\tau \}=\{a,b,c,\dots \}\cup \{\cup a,\cup b,\cup c,\dots \}\cup \{\tau \}$.

• Input actions: $i\in \mathcal{N}$ represents the receiving of an input
• Output actions: $o\in \bar{\mathcal{N}}$ represent the sending of an output
• Internal actions: $\tau$ represents an internal action

The simplest behaviour is sequential action. If $P$ is a process, we write $\alpha .P$ to denote the prefixing of $P$ with action $\alpha$.

$\alpha .P$ models a system that is ready to perform the action $\alpha$ and then it will behave as $P$. i.e. $\alpha .P{\to }^{\alpha }P$

Semantics

Labelled transition systems

Equivalence of concurrent processes