Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Concurrency 4

CCS - Simulation and bisimulation. Coinduction.

Catuscia Palamidessi

INRIA Futurs and LIX - Ecole Polytechnique

The other lecturers for this course:

Jean-Jacques Lévy (INRIA Rocquencourt)

James Leifer (INRIA Rocquencourt) Eric Goubault (CEA)

http://pauillac.inria.fr/˜ leifer/teaching/mpri-concurrency-2005/

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Announcement

The class of Wednesday 26 October will follow the usual schedule (16h15 - 19h15).

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

The semaphore

Define in CCS a semaphore with initial value n First Solution

rec_{S_{n}} down.rec_{S_{n−1}} (up.S_{n} + down.rec_{S_{n−2}} (… (up.S_{2} + down.rec_{S_{0}} up.S_{1}) …))

Second solution

Let S = rec_{X}down.up.X Then S_{n} = S | S | … | S n times

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

The semaphore

Define in CCS a semaphore with initial value n First Solution

rec_{S_{n}} down.rec_{S_{n−1}} (up.S_{n} + down.rec_{S_{n−2}} (… (up.S_{2} + down.rec_{S_{0}} up.S_{1}) …))

Second solution

Let S = rec_{X}down.up.X Then S_{n} = S | S | … | S n times

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

The semaphore

Define in CCS a semaphore with initial value n First Solution

rec_{S_{n}} down.rec_{S_{n−1}} (up.S_{n} + down.rec_{S_{n−2}} (… (up.S_{2} + down.rec_{S_{0}} up.S_{1}) …))

Second solution

Let S = rec_{X}down.up.X Then S_{n} = S | S | … | S n times

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Maximal trace equivalence is not a congruence

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0
R = ā.b̄.d̄.0

P and Q have the same traces, but (νa)(νb)(νc)(P | R) and (νa)(νb)(νc)(Q | R) have different maximal traces.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Maximal trace equivalence is not a congruence

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0
R = ā.b̄.d̄.0

P and Q have the same traces, but (νa)(νb)(νc)(P | R) and (νa)(νb)(νc)(Q | R) have different maximal traces.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Syntax

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Syntax

Syntax of “modern” CCS

(channel, port) names: a, b, c, … co-names: ā, b̄, c̄, … Note: ¯ ā = a silent action: τ

actions, prefixes: μ ::= a | ā | τ

processes: P, Q ::= 0  inaction | μ.P  prefix | P | Q parallel | P + Q (external) choice | (νa)P restriction | K (a⃗) process name with parameters

Process definitions:

D ::= K (x⃗) =^{def} P where P may contain only the x⃗

as channel names

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Syntax

Syntax of “modern” CCS

(channel, port) names: a, b, c, … co-names: ā, b̄, c̄, … Note: ¯ ā = a silent action: τ

actions, prefixes: μ ::= a | ā | τ

processes: P, Q ::= 0  inaction | μ.P  prefix | P | Q parallel | P + Q (external) choice | (νa)P restriction | K (a⃗) process name with parameters

Process definitions:

D ::= K (x⃗) =^{def} P where P may contain only the x⃗

as channel names

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Labeled transition System

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Labeled transition System

Labeled transition system for “modern” CCS

We assume a given set of definitions D

[Act] _{\overline{μ.P →^{μ} P}}  [Res] \frac{P →^{μ} P′ μ≠a,\overline{a}}{(νa)P →^{μ} (νa)P′}
[Sum1] \frac{P →^{μ} P′}{P+Q →^{μ} P′}  [Sum2] \frac{Q →^{μ} Q′}{P+Q →^{μ} Q′}
[Par1] \frac{P →^{μ} P′}{P|Q →^{μ} P′|Q}  [Par2] \frac{Q →^{μ} Q′}{P|Q →^{μ} P|Q′}
[Com] \frac{P →^{a} P′ Q →^{\overline{a}} Q′}{P|Q →^{τ} P′|Q′}  [Rec] \frac{P[a⃗/x⃗] →^{μ} P′ K (x⃗)=^{def} P ∈ D}{K (a⃗) →^{μ} P′}

The reason for moving to “modern” CCS was to get static scope (thanks to the presence of the parameters). The old version had dynamic scope.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Simulation

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Simulation

Simulation

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Definition We say that a relation R on processes is a simulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′

Note that this property does not uniquely defines R. There may be several relations that satisfy it. Define ≲ = ⋃{R | R is a simulation} Theorem ≲ is a bisimulation (Proof: Exercise) P ≲ Q intuitively means that Q can do everything that P can do. Q simulates P.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Bisimulation

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Bisimulation

Bisimulation

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Definition We say that a relation R on processes is a bisimulation if P R Q implies that ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Again, this property does not uniquely defines R. There may be several relations that satisfy it. Define ∼ = ⋃{R | R is a bisimulation} Theorem ∼ is a bisimulation (Proof: Exercise) P ∼ Q intuitively means that Q can do everything that P can do, and vice versa, at every step of the computation. Q is bisimilar to P.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Proof methods

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Proof methods

Proof methods

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence Simulation and bisimulation are coinductive definitions. In order to prove that P ≲ Q it is sufficient to find a simulation R such that P R Q Similarly, in order to prove that P ∼ Q it is sufficient to find a bisimulation R such that P R Q Simulation and bisimulation are coinductive definitions. In order to prove that P ≲ Q it is sufficient to find a simulation R such that P R Q Similarly, in order to prove that P ∼ Q it is sufficient to find a bisimulation R such that P R Q Simulation and bisimulation are coinductive definitions. In order to prove that P ≲ Q it is sufficient to find a simulation R such that P R Q Similarly, in order to prove that P ∼ Q it is sufficient to find a bisimulation R such that P R Q Simulation and bisimulation are coinductive definitions. In order to prove that P ≲ Q it is sufficient to find a simulation R such that P R Q Similarly, in order to prove that P ∼ Q it is sufficient to find a bisimulation R such that P R Q

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Examples and exercises

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Examples and exercises

Examples and exercises

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Consider the following processes P = a.(b.0 + c.0)

Q = a.b.0 + a.c.0

Prove that Q ≲ P but P ≴ Q and Q ≁ P Assume that Q ≲ P and P ≲ Q (for two generic P and Q). Does it follow that P ∼ Q? Consider the following processes

R = a.(b.0 + b.0)

S = a.b.0 + a.b.0

Prove that Q ∼ P Consider the two definitions of semaphore given at the beginning of this lecture. Prove that they are bisimilar. Consider the processes H(a) and K (a) defined by H(x) =^{def} x.H(x) and K (x) =^{def} x.K (x) | x.K (x). Are they bisimilar? What is the smallest bisimulation?

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Alternative characterization of bisimulation

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Alternative characterization of bisimulation

Bisimulation as greatest fixpoint

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Consider the set of relations on processes (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice. Definition Let F be a function on relation defined in the following way:

P F(R) Q iff ifP →^{μ} P′ then ∃Q′ s.t. Q →^{μ} Q′ and P′ R Q′ ifQ →^{μ} Q′ then ∃P′ s.t. P →^{μ} P′ and P′ R Q′

Lemma F is monotonic Theorem (Knaster-Tarski) F has (unique) least and greatest fixpoints, and

lfp(F) = ⋂{R | F(R) ⊆ R}

gfp(F) = ⋃{R | R ⊆ F(R)}

Corollary ∼ = gfp(F) A similar characterization, of course, holds for ≲ as well.

Solution to exercises from previous time  Modern definition of CCS (1999)  Simulation and bisimulation  Exercises

Bisimulation in CCS is a congruence

Outline

1 Solution to exercises from previous time
2 Modern definition of CCS (1999)

Syntax Labeled transition System

3 Simulation and bisimulation

Simulation Bisimulation Proof methods Examples and exercises Alternative characterization of bisimulation Bisimulation in CCS is a congruence

Bisimulation in CCS is a congruence

Bisimulation in CCS is a congruence

Definition A relation R on a language is called congruence if

R is an equivalence relation (i.e. it is reflexive, symmetric, and transitive), and R is preserved by all the operators of the language, namely if P R Q then op(P, R⃗) R op(P, R⃗)

Theorem ∼ is a congruence relation

Bisimulation in CCS is a congruence

Bisimulation in CCS is a congruence

Definition A relation R on a language is called congruence if

R is an equivalence relation (i.e. it is reflexive, symmetric, and transitive), and R is preserved by all the operators of the language, namely if P R Q then op(P, R⃗) R op(P, R⃗)

Theorem ∼ is a congruence relation

Exercises

Complete the proof that bisimulation in CCS is a congruence

Prove that if P ≲ Q then the traces of P are contained in the traces of Q

Prove that if P ∼ Q then P ≲ Q and Q ≲ P

Prove that

P + 0 ∼ P and P|0 ∼ P

P + P ∼ P but (in general) P|P ≁ P P + Q ∼ Q + P and P|Q ∼ Q|P (P + Q) + R ∼ P + (Q + R) and (P|Q)|R ∼ P|(Q|R)