Introduction  Syntax and Operational Semantics of CCS

Concurrency 3

CCS - Syntax and transitions, Equivalences

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/

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.