Planche 1

Concurrency 4
Bisimulations
Jean-Jacques Lévy
jeanjacqueslevy.net/dea

Planche 2

Bibliography

Principles of Concurrent Programming
Mordechai Ben-Ari, Prentice Hall, 1982
Communication and Concurrency
Robin Milner, Prentice Hall, 1989
Algebraic Theory of Processes
Matthew Hennessy, MIT Press, 1988
Communicating and Mobile Systems: the Pi-Calculus
Robin Milner, Cmabridge University Press, 1999.
The Pi-Calculus : A Theory of Mobile Processes
Davide Sangiorgi, David Walker, Cambridge University Press, 2001
System Porgramming in Modula-3
Greg Nelson, Prentice Hall, 1991

Planche 3

CCS with values (1/4)

Language

::=

variables

::=

x₁,x₂,... x_n (n ³ 0)

::=

values

::=

v₁,v₂,... v_n (n ³ 0)

a, b, c

::=

(channel) names

::=

co-names

::=

a(x) |

v | t

actions

P,Q,R

::=

0 | a.P | P+Q | (P | Q) | (n a) P | K á v ñ

processes

K á x ñ

def

::=

constant definitions

Act = { a(x), b(x), c(x), ... } È { a v, b v, c v, ... } È { t }

Notation: a for a.0

Planche 4

CCS with values (2/4)

Memory register

Regá ñ

def

put(x).A á x ñ

A á x ñ

def

put(y).A á y ñ |

get

x.A á x ñ

... | P | put 1 | get(x). Q | put 2.get(y). R | ...

Exercice 1 What can be values of x and y in Q and R ?

Buffers

Buf₁^in,out á ñ =^def in(x).out x.Buf₁^in,out á ñ

in,out

Buf₂

á ñ

def

in(x).Aá x ñ

Aá x ñ

def

in(y).

out

x.Aá y ñ +

out

in,out

Buf₂

á ñ

Buf₁'á ñ =^def (n c) (Buf₁^in,cá ñ| Buf₁^c,out á ñ)

Exercice 2 Relate Buf₂ and Buf₁'.

Planche 5

CCS with values (3/4)

Semantics (SOS)

[Act] a.P

¾®

P [Sum1]

P ¾®^a P'

P+Q ¾®^a P'

[Sum2]

Q ¾®^a Q'

P+Q ¾®^a Q'

[Par1]

P ¾®^a P'

P | Q ¾®^a P' | Q

[Par2]

Q ¾®^a Q'

P | Q ¾®^a P | Q'

[Com1]

P ¾®^a(x) P' Q ¾®^{a v} Q'

P | Q ¾®^t P'{v/x} | Q'

[Com2]

P ¾®^{a v} P' Q ¾®^a(x) Q'

P | Q ¾®^t P' | Q' { v/x }

[Res]

P ¾®^a P' a Ï{a,a}

(n a) P ¾®^a (n a) P'

[Rec]

P{v/x} ¾®^a P' Ká x ñ =^def P

Ká v ñ ¾®^a P'

Planche 6

CCS with values (4/4)

One can emulate CCS with values by pure CCS (with infinite sum).

[[ P ]]

a(x).P

S_{v Î V} a_v.[[ P {v / x} ]] (V set of values)

v.P

a_v.[[ P ]]

t.P

t.[[ P ]]

S_{i Î I} P_i

S_{i Î I} [[ P_i ]]

P | Q

[[ P ]] | [[ Q ]]

...

Exercice 3 Terminate the translation

Exercice 4 Find the relation between P and [[ P ]].

Planche 7

CCS and weak bisimulation (1/4)

Write P (®^t)^* Q if P=P₀ ®^t P₁ ®^t P₂ ··· ®^t P_k=Q (k ³ 0).

Let µ = µ₁µ₂···µ_n (n > 0)

Write P ¾®^µ Q if P ¾®^µ₁¾®^µ₂ ··· ¾®^µ_n Q

Write P =Þ^µ Q if P (®^t)^* ¾®^µ₁ (®^t)^* ¾®^µ₂ (®^t)^* ··· ¾®^µ_n (®^t)^* Q

Write µ be µ where all occurences of t in µ have been erased.

Take µ = t a b tt a, then µ=aba. If µ = tⁿ, then µ = e (empty string).

Then

¾®^µ specifies exactly the t actions occuring in µ

=Þ^µ specifies at least the t actions

=Þ^µ specifies nothing about the t actions

Planche 8

CCS and weak bisimulation (2/4)

Definition 1 P weakly bisimilar to Q (we write P » Q) if, for any a Î Act, whenever

P ¾®^a P', there is Q' such that Q =Þ^a Q' and P' » Q'.
Q ¾®^a Q', there is P' such that P =Þ^a P' and P' » Q'.

(» is the largest weak bisimulation)

Examples

A =^def c.(k.A + t.A)

B =^def (n d) c.(k.d.B + t.d.B)

A » B

C =^def (a.b.t.C + b. a.t.C

D =^def ((a.b.D + b a.D)

C » D

Exercice 5 Find weak bisimulation when

A₀

def

a.A₀ + b.A₁ + t.A₁

A₁

def

a.A₁ + t.A₂

B₁

def

a.B₁ + t.B₂

A₂

def

b.A₀

B₂

def

b.B₁

Planche 9

CCS and weak bisimulation (3/4)

Proposition 2 Following equations hold.

t.P

P » Q

P | R » Q | R

P » Q

R | P » R | Q

P » Q

a.P » a.Q

P » Q

(n x) P » (n x) Q

def

P and P » Q

K » Q

Exercice 6 Prove it.

Fact 3 P » Q ¬ Þ P + R » Q + R

Take P = t.Q, Q = a, R = b.
Then t.a » a. But we have not t.a + b » a + b.

Hence weak bisimulation is not a congruence in CCS
(differs from strong bisimulation)

Planche 10

CCS and weak bisimulation (4/4)

Definition 4[observation-congruence] P weakly congruent to Q (we write P @ Q) if, for any a Î Act, whenever

P ¾®^a P', there is Q' such that Q =Þ^a Q' and P' » Q'.
Q ¾®^a Q', there is P' such that P =Þ^a P' and P' » Q'.

Exercice 7 Prove @ Í ».

Proposition 5 @ is a congruence.

Exercice 8 Prove it.

Proposition 6 The following t laws are true:

a.t.P	»	a.P
P + t.P	»	t.P
a.(P+t.Q)+a.Q	»	a.(P+t.Q)

Exercice 9 Prove them.

Planche 11

CCS and weak bisimulation (4/4)

Proposition 7

P ~ Q Þ P @ Q Þ P » Q

P » Q Þ a.P @ a.Q

P » Q iff P @ Q or P @ t.Q or t.P @ Q

Exercice 10 Prove it.

Proposition 8 @ is the largest congruence on CCS contained in ».

Exercice 11 Prove it.

This document was translated from L^AT_EX by H^EV^EA.