Introduction  Syntax and Operational Semantics of CCS

Concurrency 1

CCS - Syntax and transitions, Equivalences

Catuscia Palamidessi

INRIA Futurs and LIX - Ecole Polytechnique

The other lecturers for this course:

Pierre-Louis Curien (PPS, Paris VII) Francesco Zappa Nardelli (INRIA Rocquencourt)

Roberto Amadio (PPS, Paris VII)

http://mpri.master.univ-paris7.fr/C-2-3.html

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Introduction  Syntax and Operational Semantics of CCS

Motivations

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Introduction  Syntax and Operational Semantics of CCS

Motivations

Why a Calculus for Concurrency?

The Calculus for Communicating Systems (CCS) was developed by R. Milner around the 80’s. Other Process Calculi were proposed at about the same time: the Theory of Communicating Sequential Processes by T. Hoare and the Algebra of Communicating Processes by J. Bergstra and J.W. Klop. Researchers were looking for a calculus with few, orthogonal mechanisms, able to represent all the relevant concepts of concurrent computations. More complex mechanisms should be built by using the basic ones.

To help understanding / reasoning about / developing formal tools for concurrency. To play a role, for concurrency, like that of the λ-calculus for sequential computation.

Introduction  Syntax and Operational Semantics of CCS

Motivations

Inadequacy of standard models of computations

The λ calculus, the Turing machines, etc. are computationally complete, yet do not capture the features of concurrent computations like

Interaction and communication Inadequacy of functional denotation Nondeterminism

Note: nondeterminism in concurrency is different from the nondeterminism used in Formal Languages, like for instance the Nondeterministic Turing Machines.

Introduction  Syntax and Operational Semantics of CCS

Motivations

A few words about nondeterminism

In standard computation theory, if we want to compute the partial function f s.t. f (0) = 1, a Turing Machine like this one is considered ok

However, we would not be happy with a coffee machine that behaves in the same way

Introduction  Syntax and Operational Semantics of CCS

Motivations

A few words about nondeterminism

In standard computation theory, if we want to compute the partial function f s.t. f (0) = 1, a Turing Machine like this one is considered ok

However, we would not be happy with a coffee machine that behaves in the same way

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in sequential models

Convenient tool for solving certain problems in an easy way or for characterizing complexity classes (examples: search for a path in a graph, search for a proof etc.)

Examples of nondeterministic formalisms:

The nondeterminismistic Turing machines Logic languages like Prolog and λ Prolog

The characteristics of nondeterminism in this setting:

It can be eliminated without loss of computational power by using backtracking. Failures don’t matter: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail.

Motivations

Nondeterminism in concurrent models

Nondeterminism may arise because of interaction between processes.

The characteristics of nondeterminism in this setting:

It cannot be avoided. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism. Failures do matter. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes.

Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.

Motivations

Nondeterminism in concurrent models

Nondeterminism may arise because of interaction between processes.

The characteristics of nondeterminism in this setting:

It cannot be avoided. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism. Failures do matter. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes.

Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.

Motivations

Nondeterminism in concurrent models

Nondeterminism may arise because of interaction between processes.

The characteristics of nondeterminism in this setting:

It cannot be avoided. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism. Failures do matter. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes.

Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.

Motivations

Nondeterminism in concurrent models

Nondeterminism may arise because of interaction between processes.

The characteristics of nondeterminism in this setting:

It cannot be avoided. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism. Failures do matter. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes.

Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.

Motivations

Nondeterminism in concurrent models

Nondeterminism may arise because of interaction between processes.

The characteristics of nondeterminism in this setting:

It cannot be avoided. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism. Failures do matter. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes.

Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.

Introduction  Syntax and Operational Semantics of CCS

Principles in CCS design

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (1/2)

A calculus should contain only the primary constructs. For instance, the primary form of interaction. But what is the primary form of interaction?

In general, concurrent languages can offer various kinds of communication. For instance:

Communications via shared memory. Communication via channels. Communication via broadcasting.

and we could make even more distinctions one-to-one / one-to-many Ordered / unordered (i.e. queues / bags) Bounded / unbounded.

Principles in CCS design

The basic kind of interaction (2/2)

In CCS, the fundamental model of interaction is synchronous and symmetric, i.e. the partners act at the same time performing complementary actions.

This kind of interaction is called handshaking: the partners agree simoultaneously on performing the two (complementary) actions.

In Java there is a separation between active objects (threads) and passive objects (resources). CCS avoids this separation: Every (non-elementary) entity is a process.

For instance, consider two proceesses P and Q communicating via a buffer B. in CCS also B is a process and the communication is between P and B, and between Q and B.

Principles in CCS design

The basic kind of interaction (2/2)

In CCS, the fundamental model of interaction is synchronous and symmetric, i.e. the partners act at the same time performing complementary actions.

This kind of interaction is called handshaking: the partners agree simoultaneously on performing the two (complementary) actions.

In Java there is a separation between active objects (threads) and passive objects (resources). CCS avoids this separation: Every (non-elementary) entity is a process.

For instance, consider two proceesses P and Q communicating via a buffer B. in CCS also B is a process and the communication is between P and B, and between Q and B.

Principles in CCS design

The basic kind of interaction (2/2)

In CCS, the fundamental model of interaction is synchronous and symmetric, i.e. the partners act at the same time performing complementary actions.

This kind of interaction is called handshaking: the partners agree simoultaneously on performing the two (complementary) actions.

In Java there is a separation between active objects (threads) and passive objects (resources). CCS avoids this separation: Every (non-elementary) entity is a process.

For instance, consider two proceesses P and Q communicating via a buffer B. in CCS also B is a process and the communication is between P and B, and between Q and B.

Principles in CCS design

The basic kind of interaction (2/2)

In CCS, the fundamental model of interaction is synchronous and symmetric, i.e. the partners act at the same time performing complementary actions.

This kind of interaction is called handshaking: the partners agree simoultaneously on performing the two (complementary) actions.

In Java there is a separation between active objects (threads) and passive objects (resources). CCS avoids this separation: Every (non-elementary) entity is a process.

For instance, consider two proceesses P and Q communicating via a buffer B. in CCS also B is a process and the communication is between P and B, and between Q and B.

Introduction  Syntax and Operational Semantics of CCS

Principles in CCS design

Example: P and Q communicating via a buffer B

Introduction  Syntax and Operational Semantics of CCS

Syntax

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Introduction  Syntax and Operational Semantics of CCS

Syntax

Syntax of 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 | rec_{K}P process P with definition K = P | K  (defined) process name

(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 | rec_{K}P process P with definition K = P | K  (defined) process name

(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 | rec_{K}P process P with definition K = P | K  (defined) process name

(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 | rec_{K}P process P with definition K = P | K  (defined) process name

(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 | rec_{K}P process P with definition K = P | K  (defined) process name

(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 | rec_{K}P process P with definition K = P | K  (defined) process name

Introduction  Syntax and Operational Semantics of CCS

Labeled transition System

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Introduction  Syntax and Operational Semantics of CCS

Labeled transition System

Labeled transition system

The semantics of CCS is defined by in terms of a labeled transition system, which is a set of triples of the form

P →^{μ} Q

Meaning: P evolves into Q by making the action μ.

The presence of the label μ allows us to keep track of the interaction capabilities with the environment.

Introduction  Syntax and Operational Semantics of CCS

Labeled transition System

Structural operational semantics

The transitions of CCS are defined by a set of inductive rules. The system is also called structural semantics because the evolution of a process is defined in terms of the evolution of its components.

[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′}

Introduction  Syntax and Operational Semantics of CCS

Labeled transition System

Structural operational semantics

The transitions of CCS are defined by a set of inductive rules. The system is also called structural semantics because the evolution of a process is defined in terms of the evolution of its components.

[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′}

Introduction  Syntax and Operational Semantics of CCS

Labeled transition System

Some examples

The restriction can be used to enforce synchronization

The parallel operator may cause infinitely many different states

The fragment of the calculus without parallel operator generates only finite automata / regular trees The restriction can be used to enforce synchronization

The parallel operator may cause infinitely many different states

The fragment of the calculus without parallel operator generates only finite automata / regular trees The restriction can be used to enforce synchronization

The parallel operator may cause infinitely many different states

The fragment of the calculus without parallel operator generates only finite automata / regular trees The restriction can be used to enforce synchronization

The parallel operator may cause infinitely many different states

The fragment of the calculus without parallel operator generates only finite automata / regular trees

Introduction  Syntax and Operational Semantics of CCS

What equivalence for CCS?

Outline

1 Introduction

Motivations Principles in CCS design

2 Syntax and Operational Semantics of CCS

Syntax Labeled transition System What equivalence for CCS?

Introduction  Syntax and Operational Semantics of CCS

What equivalence for CCS?

Motivation

It is important to define formally when two system can be considered equivalent

There may be various "interesting" notion of equivalence, it depends on what we want (which observables we want to preserve)

It is important to define formally when two system can be considered equivalent

There may be various "interesting" notion of equivalence, it depends on what we want (which observables we want to preserve)

It is important to define formally when two system can be considered equivalent

There may be various "interesting" notion of equivalence, it depends on what we want (which observables we want to preserve)

It is important to define formally when two system can be considered equivalent

There may be various "interesting" notion of equivalence, it depends on what we want (which observables we want to preserve)

Introduction  Syntax and Operational Semantics of CCS

What equivalence for CCS?

Examples: possible definitions of a coffee machine

rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces. rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces. rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces. rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces. rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces. rec_{K}coin.(coffee .\overline{ccup}.K + tea.\overline{tcup}.K ) coin.rec_{K}(coffee .\overline{ccup}.coin.K + tea.\overline{tcup}.coin.K ) rec_{K}(coin.coffee .\overline{ccup}.K + coin.tea.\overline{tcup}.K ) Question: which of these machines can we safely consider equivalent? Note that these machines have all the same traces.

Introduction  Syntax and Operational Semantics of CCS

What equivalence for CCS?

Exercises

Define in CCS a semaphore with initial value n Show that maximal trace equivalence is not a congruence in CCS. By maximal traces here we mean the traces of all possible (finite or infinite) maximal runs.