Process Theory and Reactive Systems

Purpose. These notes are my write-up of Process Theory and Reactive Systems, extended with material from Aceto, Ingólfsdóttir, Larsen, and Srba’s Reactive Systems: Modelling, Specification and Verification. I adapted tutorial and exam material into a blog-friendly format, keeping the TU/e proof style: SOS derivation trees, modal logic denotational calculations, and attacker–defender bisimulation games. Examples are numbered per section (2.1, 2.2, …).

1. Reactive Systems as Labelled Transition Systems (LTS)

Definition. A reactive system is an LTS $(S, Act, \to)$ with states $S$, actions $Act$ (may include $\tau$), and transitions $\to \subseteq S \times Act \times S$. We write $s \xrightarrow{\alpha} s’$ if $(s,\alpha,s’)\in\to$.

Motivation.

Actions capture interaction with the environment.
Nondeterminism arises from multiple outgoing edges.
Silent steps ($\tau$) model internal computation.

Example 1.1

Let $S={s,s_1,s_2}$, $Act={a,b}$, with transitions $s \xrightarrow{a} s_1$, $s \xrightarrow{a} s_2$, and $s_1 \xrightarrow{b} s_2$.
Here, $s$ is nondeterministic on $a$; both successors exist.

2. CCS: Syntax and Structural Operational Semantics

2.1 Syntax

Processes $P,Q ::= 0 \mid \alpha.P \mid P+Q \mid P\mid Q \mid P\setminus L \mid P[f]$
where $\alpha\in Act\cup{\tau}$, $L\subseteq Act$, and $f:Act\to Act$ with $f(\tau)=\tau$.

2.2 SOS Rules

Act: $a.P \xrightarrow{a} P$
Sum: $\cfrac{P\xrightarrow{a}P’}{P+Q\xrightarrow{a}P’}$ and $\cfrac{Q\xrightarrow{a}Q’}{P+Q\xrightarrow{a}Q’}$
Par: $\cfrac{P\xrightarrow{a}P’}{P\mid Q \xrightarrow{a} P’\mid Q}$ and $\cfrac{Q\xrightarrow{a}Q’}{P\mid Q \xrightarrow{a} P\mid Q’}$
Com: $\cfrac{P\xrightarrow{a}P’ \quad Q\xrightarrow{\bar a}Q’}{P\mid Q \xrightarrow{\tau} P’\mid Q’}$
Res: $\cfrac{P\xrightarrow{a}P’}{P\setminus L \xrightarrow{a} P’\setminus L}\quad (a,\bar a\notin L)$
Rel: $\cfrac{P\xrightarrow{a}P’}{P[f]\xrightarrow{f(a)} P’[f]}$

Example 2.1: Communication and Restriction

Show $(a.B \mid \bar a.0)\setminus{a} \xrightarrow{\tau} (B\mid 0)\setminus{a}$.

$ \cfrac{ \cfrac{ \cfrac{a.B \xrightarrow{a} B}{a.B \mid \bar a.0 \xrightarrow{a} B \mid \bar a.0} \quad \cfrac{\bar a.0 \xrightarrow{\bar a} 0}{a.B \mid \bar a.0 \xrightarrow{\bar a} a.B \mid 0} }{ a.B \mid \bar a.0 \xrightarrow{\tau} B \mid 0 } }{ (a.B \mid \bar a.0)\setminus{a} \xrightarrow{\tau} (B\mid 0)\setminus{a} } $

Example 2.2: Choice vs. Sequencing

$P = b.a.0 + b.0$
$Q = b.(a.0 + b.0)$

$P$ allows $b$ then either deadlock or continue with $a$.
$Q$ forces $b$ first, then offers both $a$ and $b$.
We will distinguish them in HML (Example 4.4).

3. Hennessy–Milner Logic (HML)

3.1 Syntax

$ \varphi ::= \top \mid \bot \mid \varphi\land\varphi \mid \varphi\lor\varphi \mid \neg\varphi \mid \langle a\rangle \varphi \mid [a]\varphi $

3.2 Semantics

$[[\top]]=Proc,\ [[\bot]]=\emptyset$
$[[\varphi\land\psi]] = [[\varphi]] \cap [[\psi]]$
$[[\langle a\rangle \varphi]] = {P\mid \exists P’.\ P\xrightarrow{a}P’ \land P’\in [[\varphi]]}$
$[[[a]\varphi]] = {P\mid \forall P’.\ P\xrightarrow{a}P’ \Rightarrow P’\in [[\varphi]]}$

Example 3.1: Basic Satisfaction

If $s \xrightarrow{a} s’$, then $s \in [[\langle a\rangle \top]]$.
If $s$ has no $b$-successor, then $s \in [[[b]\bot]]$.

Example 3.2: Nested Box

$[[[a][b]\bot]] = {P\mid \forall P’.\ P\xrightarrow{a}P’ \Rightarrow (\forall P’’.\ P’\xrightarrow{b}P’’ \Rightarrow P’‘\in\emptyset)}$.

So $P$ satisfies $[a][b]\bot$ iff all $a$-successors of $P$ have no $b$-successor.

Example 3.3: Diamond Then Conjunction

$[[\langle a\rangle (\langle a\rangle \top \land \langle b\rangle \top)]] = {P\mid \exists P’.\ P\xrightarrow{a}P’ \land P’\text{ has both $a$- and $b$-successors}}$.

Example 3.4: Distinguishing CCS Terms

Formula $\varphi \equiv [b]\langle b\rangle \top$ distinguishes $P=b.a.0+b.0$ from $Q=b.(a.0+b.0)$:

In $Q$: after $b$, the subterm $(a.0+b.0)$ still has a $b$. So $Q\models\varphi$.
In $P$: one $b$-successor is $a.0$, which has no $b$. So $P\not\models\varphi$.

4. Trace Equivalence vs. Bisimulation

Trace equivalence. Two processes are trace-equivalent if they generate the same sets of finite traces (observable action sequences).

Bisimulation. Requires step-by-step matching, preserving branching structure.

Example 4.1

$P = a.b.0 + a.c.0$
$Q = a.(b.0 + c.0)$

Both have trace set ${ab, ac}$.
So $P$ and $Q$ are trace-equivalent.

But they are not bisimilar: after $a$, $P$ commits to $b$ or $c$, while $Q$ still allows both.
Attacker can exploit this difference.

5. Weak Bisimulation

Strong bisimulation is too strict in practice; we often abstract from $\tau$-steps.

5.1 Weak Transitions

$P \xRightarrow{\alpha} Q$ means $P$ can reach $Q$ via any number of $\tau$, then $\alpha$, then any number of $\tau$.
For $\alpha=\tau$, $P \xRightarrow{\tau} Q$ means “$P$ can reach $Q$ via only $\tau$-steps.”

5.2 Weak Bisimulation

$R$ is a weak bisimulation if $(P,Q)\in R$ and whenever $P \xrightarrow{\alpha} P’$, there exists $Q’$ with $Q \xRightarrow{\alpha} Q’$ and $(P’,Q’)\in R$ (and vice versa).

Example 5.1

$P = \tau.a.0$
$Q = a.0$

Not strongly bisimilar (first $\tau$ visible in strong sense).
But weakly bisimilar: $P \xRightarrow{a} 0$ matches $Q \xrightarrow{a} 0$.

6. Recursive Processes and HML with Recursion

6.1 Recursive Definitions

Processes can be defined recursively: $X = a.X + b.0$.
This process can perform arbitrarily many $a$’s and eventually a $b$.

6.2 Characteristic Formulas

For each finite-state process $P$, there exists an HML formula $\chi(P)$ such that $Q\models\chi(P)$ iff $Q$ is bisimilar to $P$.

Example 6.1.
For $P = a.b.0$, $\chi(P) = \langle a\rangle \langle b\rangle [a]\bot \land [a]\langle b\rangle \top$.
Such formulas capture the exact branching structure.

7. Attacker–Defender Games

7.1 Game Definition

Attacker chooses a transition.
Defender must match with same observable label (weak case allows $\tau$-closure).
If defender fails, attacker wins; otherwise infinite play → defender wins.

Example 7.1

$s_0\xrightarrow{a}s_1$ but $t_0$ has no $a$.
Attacker plays $a$, defender stuck.
So $s_0 \not\sim t_0$.
Witness formula: $\langle a\rangle \top$.

Example 7.2

Let $P=a.(b.0+c.0)$ and $Q=a.b.0+a.c.0$.
Attacker: from $Q$, choose $a$ then commit to $b$.
Defender: from $P$, $a$ leads to $(b.0+c.0)$, which still has $c$.
Attacker now switches to $c$, defender cannot match.
So $P\not\sim Q$.
Witness formula: $a$.

8. Case Study: Mutual Exclusion

8.1 Modelling

We want two processes $P_1,P_2$ that share a critical section.
Model:

$P_i = req_i.enter_i.exit_i.P_i$
System = $P_1 \mid P_2$

8.2 Correctness Properties

Safety: never both in critical section.
In HML: $[[\neg(\langle enter_1\rangle \langle enter_2\rangle \top)]]$.
Liveness: if $req_i$ occurs infinitely often, eventually $enter_i$.
In HML recursion: $\nu X.\ ([req_i]\langle enter_i\rangle \top \land [Act]X)$.

8.3 Verification

An incorrect version without synchronization allows both $enter_1$ and $enter_2$ simultaneously → violates safety formula.
A correct mutex (with a shared lock) satisfies safety but may or may not satisfy liveness depending on fairness assumptions.

9. More CCS Equivalences

Example 9.1: τ-Absorption

Show $P \mid (\tau.Q+Q) \approx P \mid Q$ (weak bisimulation).

$ \cfrac{ \cfrac{\cfrac{\tau.Q\xrightarrow{\tau} Q}{\tau.Q+Q\xrightarrow{\tau}Q}}{P\mid (\tau.Q+Q)\xrightarrow{\tau} P\mid Q} }{} $

So both sides behave equivalently modulo $\tau$.

Example 9.2: Parallel vs. Choice

$a.0\mid b.0 \sim a.b.0 + b.a.0$.

$a.0\mid b.0$ can do $a$ or $b$, reducing to the other.
$a.b.0+b.a.0$ offers the same traces.

Bisimulation relates $(a.0\mid b.0,\ a.b.0+b.a.0)$ and continuations.

10. Conclusion

Reactive systems are modelled by LTS.

CCS gives a precise operational account.
HML specifies modal properties.
Trace equivalence vs. bisimulation highlights structural vs. behavioural matching.
Weak bisimulation abstracts internal actions.
Recursive definitions and characteristic formulas enrich expressiveness.
Attacker–defender games give an intuitive strategy-based interpretation.
Case studies like mutual exclusion illustrate practical application.

Together, these tools form a rigorous framework for reasoning about concurrency and reactivity.

References

L. Aceto, A. Ingólfsdóttir, K. Larsen, J. Srba, Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
R. Milner, Communication and Concurrency, Prentice Hall, 1989.
C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008.
TU/e course Process Theory and Reactive Systems tutorial and exam materials.

CCS operational semantics, HML derivations, and behavioural equivalences