Electrical Engineering and Computer Science

**ECS 402: Concurrency Theory** (4)

*Learning Objectives*:

A reactive system comprises networks of computing components, achieving their goals through interaction among themselves and their environment. This course aims to develop a general-purpose theory that can be used to describe, and reason about, reactive systems. We introduce Milner's Calculus of Communicating Systems (CCS) for modelling reactive systems, its structural operational semantics, together with the notions of behavioural equivalences and recursive extensions of Hennessy-Milner logic (HML). We also study CCS with time delays, timed automata, timed behavioural equivalences and HML with time.

*Course Contents*:

- Calculus of Communicating systems, labelled transition systems and structural operational semantics
- Behavioural equivalences
- Theory of fixed points, Tarski's fixed point theorem
- Hennessy-Milner Logic (HML) and HML with recursion
- Theory of real-time systems
- CCS with time delays
- Timed automata and timed behavioural equivalences
- HML with time
- Modeling examples and other process algebras

**Selected Readings:**

- Reactive Systems, Modelling, Specification and Verification, Cambridge Press, 2007 (First Edition), Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen and Jiri Srba.
- Introduction to Concurrency Theory - Transition Systems and CCS, Springer International Publishing, 2015 (First Edition), Roberto Gorrieri and Cristian Versari.
- Process Algebra: Equational Theories of Communicating Processes, Cambridge University Press, 2010, J.C.M. Baeten, T. Basten and M. A. Reniers.

Previous | Back to Course List | Next |