Communication and

Concurrency: CCS

R. Milner, “A Calculus of Communicating Systems”,

1980
 Why calculi?

• Prove properties on programs and languages

• Principle: tiny syntax, small semantics, to be
handled on paper or mechanically
• Prove properties on the principles of a language
or a programming paradigm

• Examples: lambda calculus, sigma calculus, …

 Static semantics : examples

• Checks non-syntactic constraints

• compiler front-end :
declaration and utilisation of variables,
typing, scoping, … static typing => no execution
errors ???
• or back-ends :
optimisers
• defines legal programs :
Java byte-code verifier
JavaCard: legal acces to shared variables through
What can we do/know about a
firewall
program without executing it?
Mastère RSD - TC4 oct-nov 2007 3
 Dynamic semantics

• Gives a meaning to the program (a semantic

value)
• Describes the behaviour of a (legal) program
• Defines a language interpreter
|- e -> e ’
let i=3 in 2*i -> 6

Objective = to prove properties on

Program execution
(determinacy, subject reduction, …)
Mastère RSD - TC4 oct-nov 2007 4
 The different semantic families

• Denotational semantics
mathematical model, high level, abstract
• Axiomatic semantics
provides the language with a theory for
proving properties / assertions of programs
• Operational semantics
computation of the successive states of an
abstract machine
used to build evaluators, simulators.

Mastère RSD - TC4 oct-nov 2007 5

What about concurrency and communication?

• Different timing (synchronous/asynchronous …)

• Different programming models (what is the unit
of concurrency? What is sufficient to
characterize an execution?...?)
• Interaction between communication/
concurrency/shared memory!

Through CCS, this course is a simple

study of synchronous communications
SEMANTICS
 Operational Semantics
• Describes the computation
• States and configuration of an abstract machine:
Stack, memory state, registers, heap...
• Abstract machine transformation steps
• Transitions: current state -> next state
• Several different operational semantics

9
 Natural Semantics : big steps (Kahn 1986)
• Defines the results of evaluation.
• Direct relation from programs to results
env |- prog => result
env: binds variables to values
result: value given by the execution of prog
Reduction Semantics : small steps
describes each elementary step of the evaluation
• rewriting relation : reduction of program terms
• stepwise reduction: <prog, s> -> <prog’, s ’>
– infinitely, or until reaching a normal form.

10
 Labelled Transition Systems (LTS)

• Basic model for representing reactive,

concurrent, parallel, communicating systems.
• Definition:
 < S, s0, L, T>
 S = set of states
 S0 ∈ S = initial state
 L = set of labels (events, communication actions,
etc)
 T ⊆ S x L x S = set of transitions
a
 Notation: s1  s2 = (s1, a, s2) ∈ T

Mastère RSD - TC4 oct-nov 2007 11

An example
Deduction Rules
CCS – SYNTAX AND
SEMANTICS
 CCS syntax
• Channel names: a, b, c , . . .
• Co-names:
• Silent action: τ
• Actions:
• Processes:
 A tiny example

recC1 (T ick.C1)

Labelled graph
• vertices: process expressions
• labelled edges: transitions
• Each derivable transition of a vertex is depicted
• Abstract from the derivations of transitions
 CCS : behavioural semantics (1)
Operators and rules
• Action prefix:

• Communication:

• Parallelism
 CCS : behavioural semantics (2)
Operators and rules
• Non-deterministic choice

• Scope restriction

• Recursive definition
 Derivations
(construction of each transition step)

Prefix
a
Par-L
Prefix
a P|Q a
Par-2
τ

Par-2(Par_L(Prefix), Prefix)

Another one : One amongst 3 possible derivations

Par-L(Par_L(Prefix))

19
EQUIVALENCES

20
 Behavioural Equivalences

• Intuition:
Same possible sequences of observable actions
Finite / infinite sequences
Various refinements of the concept of observation
• Definition: Trace Equivalence
For a LTS (S, s0, L, T) its Trace language T is the set of finite
sequences {(t = t1, …, tn such that ∃s0,…,sn ∈ Sn+1,
and (sn-1,tn,sn) ∈ T}

Two LTSs are Trace equivalent iff their Trace languages are equal.

Corresponding Ordering: Trace inclusion

21
 Trace Languages, Examples

• Those 2 systems are trace equivalent:

a a a
b c ≡ b c
T = {(), (a), (a,b), (a,c)}

• A trace language can be an infinite set:

a T = {(), (a), (a,a), (a,…,a),…

(a,b), (a,a,b), (a,a,…,a,b),
b
…}

22
 Bisimulation
• Behavioural Equivalence
non distinguishable states by observation:
two states are equivalent if for all possible transitions labelled
by the same action, there exist equivalent resulting states.

• Bisimulations
R ⊆ SxS is a simulation iff
It is a equivalence relation
~
act act
∀(p,q) ∈ R,
(p,l,p’) ∈ T => ∃ q’/ (q,l,q’) ∈ T and (p’,q’) ∈ R
R is a bisimulation if the same condition hold with q too:
∀(p,q) ∈ R,
~
(q,l,q’) ∈ T => ∃ q’/ (q,l,q’) ∈ T and (p’,q’) ∈ R

• ~ is the coarsest bisimulation

2 LTS are bisimilar iff their initial states are in ~
quotients = canonical normal forms

23
 Transitivity

• If R, S are bisimulations, then so is their composition

RS = {(P, P’) | Q. P R Q and Q S P’}
• In particular, ∼∼ ∼, i.e., bisimilarity is transitive.
 Bisimulation
• More precise than trace equivalence :
A0 B0

a a a
~b
A1 B1 B2 No state in B is equivalent to
b c c A1
A2 A3 B3 B4

• Preserves deadlock properties.

• Can be built by adding elements in the
equivalence relation
• Coinductive definition (biggest set verifying …)
25
 Bisimulation

• Congruence laws:
P1~P2 => a.P1 ~ a:.2 (∀ P1,P2,a)
P1~P2, Q1~Q2 => P1+Q1 ~ P2+Q2
P1~P2, Q1~Q2 => P1|Q1 ~ P2|Q2
Etc…
• ~ is a congruence for all CCS operators :

for any CCS context C[.], C[P] ~ C[Q] <=> P~Q

Basis for compositional proof methods
• Maximal trace is not an equivalence

26
 Observational Equivalences
• Weak bisimulation
Abstraction: hidden actions
µ
allows for arbitrary many internal actions
τ act
τ* τ* act τ*

27
 Weak bisimulation

• The following def is a tractable version of weak

bisimulation:
A weak bisimulation is a relation R such that
µ µ
PRQ µ, P, P’ (P →P’ Q’. Q Q’ and P’ R Q’)
and conversely
• Note the dissymetry between the use of →on the left and
of on the right
• Two processes are weakly bisimilar if (notation P ≈ Q) if
there exists a weak bisimulation R such that P R Q.
 Branching bisimulation

• only staying in equivalent states

Still existence of a canonical minimal automata
Computation is polynomial

a a

τ
ADDITIONAL NOTATIONS AND
CONSTRUCTS
 Alternative Notations

recC1 (T ick.C1)
a little more complex for several definitions
-> exercise?
• Input/output: a=?a ; a = !a
• | or ||

31
 Extension: Parameterized actions

• input of data at port a, a(x ).E

• a(x ) binds free occurrences of x in E .
• Port a represents {a(v ) : v D } where D is a family of
data values
• Output of data at port a, a(e ).E where e is a data
expression.
• Transition Rules: depend on extra machinery for
expression evaluation. Let Val(e ) be data value in D (if
there is one) to which e evaluates
a(v )
• R (in) a(x ).E → E {v /x } if v D where {v /x } is
substitution
a (v )
• R (out) a(e ).E → E if Val(e ) = v
32
 Example: a register

Regi = read(i ).Regi + write(x ).Reg x

EXAMPLES
 philosopher
Example: dining philosophers
chopstick
Drop_right! Drop_left!

Drop?
Eat
Take_left Take_right
Take_right
Take_left Take?

Idle

Drop_left Drop_right

(recidling,eating. (idle.idling + take_left.take_right.eating +

take_right.take_left.eating,
eat.eating + drop_left.drop_right.idling +
drop_right.drop_left.idling)
Deadlock or not ?
Mutual exclusion ?
 (trivial) example: Milner’s
Scheduler
• Processes iteratively start and finish executing
tasks (one task per process)
• Task starts are cyclically ordered
cycler = α.start.( β.0 || end.cycler)
scheduler_3 = local α1, α2, α3 in
( [α1/ α, α2/β, start1/start, end1/end] cycler
|| [α2/ α, α3/β, start2/start, end2/end] cycler
|| [α3/ α, α1/β, start3/start, end3/end] cycler
vérification des
|| α1.0) propriétés ?
 Scheduler_2
expanded
tau
start1
end2
end1

end2 tau

end2 start1
end1 start2
end2
end1

tau end1

end1 end2

start2
tau
 Scheduler_2 reduced
tau
start1
end2
end1

end2 tau

end2 start1
end1 start2
end2
end1

tau end1

end1 end2

start2
tau
 Scheduler_2 reduced

end1 start1

end2
end2 start1
end1 start2
end2
end1
end1

start2
end2
 CONCLUSION

• A synchronous communication language

• A (complex but) efficient notion of equivalence on
processes
• What is missing?
Channel communication (like in pi-calculus) -> much
more complex
No computational construct by nature
EXERCISES
 Example: Alternated Bit Protocol
?imss !
omss
Fwd_channel
!in0 ?out0
? ? !ack1 ?out0
ack1 imss
? !
? !
ack0 omss
ack1 omss
? ?out1
!in1 imss ? Bwd_channel ?out1 !ack0
ack0
emitter receiver
Hypotheses: channels can loose
messages
Requirement:
Write in CCS ?
the protocol ensures no loss of
messages
42
 Example: Alternated Bit Protocol
(2)
• emitter =
let rec {em0 = ?ack1 :em0 + ?imss:em1
and em1 = !in0 :em1 + ?ack0 :em2
and em2 = ?ack0 :em2 + ?imss :em3
and em3 = !in1 :em3 + ?ack1 :em0
}
in em0
• ABP = local {in0, in1, out0, out1, ack0, ack1, …}
in emitter || Fwd_channel || Bwd_channel ||
receiver

Mastère RSD - TC4 oct-nov 2007 43

 Example: Alternated Bit Protocol
(3)
Channels that loose and
duplicate messages (in0
and in1) but preserve their
order ?
• Exercise :
1) Draw an LTS describing the loosy channel
behaviour
2) Write the same description in CCS

Mastère RSD - TC4 oct-nov 2007 44

Exercise 2
 Exercice 3 : Bisimulations

?in0 Are those 3 LTSs equivalent by:

τ
- Strong bisimulation?
!out0 !out0
- Weak bisimulation ?
In each case, give a proof.
?in0
τ
!out0

τ
τ !out0
?in1 ?in0
 Exercice 3 : Bisimulation
A1
?in0
τ
τ

!out0 !out0

• Exercice :
1) Compute the strong minimal automaton for A1.
2) Compute the weak minimal automaton for A1.
 Exercise 5
def
• Compare the construct = and recK :
1. Let us start by a simple pair of processes
def
A = ā.A + b.B
def
B = a.A
2. Suppose rec can accept several variables:
rec (K=P,L=Q) express the same term
3. Is it possible to express the same thing with a single variable K?
Here are some possible hints:
 Define a recursive process All that contains A and B and can
trigger each of them by the reception of a message on channel cA
or cB
 (we suppose cA and cB cannot be used elsewhere)
 What kind of equivalence between the two expressions do you
have?
CORRECTION
 Exercice: Alternated Bit Protocol
Correction (1):
Channels that loose and
duplicate messages (in0 ?in1 ?in0
τ τ
and in1) but preserve their τ τ
order ? !out0
!out1 !out1 !out0
1) Draw an automaton
describing the loosy
channel behaviour
• It is a symmetric system, receiving ?in0 and ?in1 messages, then delivering 0 ,
1 or more times the corresponding !out0 or !out1 message.
• On each side (bit 0 or 1), the initial state has a single transition for the
reception.
• In the next state, it can either : return silently to the initial state (= lose the
message), deliver the message and return to the initial state (exactly one
delivery), or deliver the message and stay in the same state (thus enabling
duplication).
 Exercice: Alternated Bit Protocol
Correction (2):
Channels that loose and
duplicate messages (in0 ?in1 ?in0
τ τ
and in1) but preserve their τ τ
order ? !out0
!out1 !out1 !out0
2) Write it in CCS

• Lousy channel =
let rec {ch0 = ?in0 :ch1 + ?in1:ch2
and ch1 = τ :ch1 + τ :ch0 + !out0 :ch1 + !out0 :ch0
and ch2 = τ :ch2 + τ :ch0 + !out0 :ch2 + !out0 :ch0
}
in ch0
 Exercice: Alternated Bit Protocol
Correction (3):
?in0
Channels that loose and
duplicate messages (in0 τ
and in1) but preserve their !out0
!out0
order ?

?in0
Other Solutions: τ
!out0

More generally,
parameterized model :
?in(x)
τ !out(x)
x
 Exercice 2 : Bisimulations

?in0 Are those 3 LTSs equivalent by:

τ 1.1
- Strong bisimulation?
1.0
!out0 !out0 NO ! Need find non equivalent states. E.g. counter
example for 1 ≠ 2:
States 1.0 and 1.1 are different because 1.0 can do ?
?in0 in0 and 1.1 cannot.

τ 2.1 Then 1.1 and 2.1 are different because 1.1 can do !
out0 -> 1.0, while no 2.1 !out0 transitions can go to a
2.0
!out0 state equivalent to 1.0.

- Weak bisimulation ?
YES. Exhibit a partition of equivalent states:
τ
1={1.0,2.0}, 2={1.1, 2.1}
τ !out0
Check all possible (τ*aτ*) transitions:
?in1 ?in0 1 - !in0 -> 2, … , 2 - !out0.τ* -> 1
Remark: this transition set defines the minimal
representant modulo weak bisimulation…
Exercice 4 : Produit synchronisé
Compute the synchronized
product of the LTS
representing the ABP
emitter with the (forward)
Channel:
?imss
local {in0, in1} in
(Emitter || Channel)
!in0
?ack1 ?imss
0 1

?ack0 ?in1 ?in0

?ack1 τ τ
3 2 τ τ 1
2
?imss 0
!out1 !out1 !out0 !out0
!in1 ?ack0
Exercice 4 : Produit synchronisé
Correction ? partially…
local {in0, in1} in
(Emitter || Channel)

!out0
τ
?ack1 ?imss τ
0,0 1,0 τ 1,1 !out0
?ack0 ?ack0
?ack1 τ 2,1
2,0 τ
!out0
τ !in1 3,0 ?ack0 3,1 !out0
?imss
τ ?imss

!out1
 Exercice 4 : Produit synchronisé
Correction ? Tool generated LTS…