Jump to: navigation, search

Modeling and Analysis of Concurrent Systems

Tutorial Description

This is half-a-day tutorial held at the PSI 2015 conference at Innapolis, Russia. .

It gives an overview on the book Modeling and analysis of communicating systems that appeared in the summer of 2014. The theory in the book is developed with as major guideline how to model and verify system behaviour. It rests on two pillars, namely process algebras for behavioural description and modal logic to characterise requirements. As data is indispensable when describing realistic systems, both formalisms are endowed with a whole range of data types, including functions, sets and reals. Timed behaviour can also be expressed in both the algebra and the logic. An important purpose of the book is to mathematically verify the correctness of communicating systems.

The theory is implemented in the mCRL2 toolset, which is freely available under the Boost license.


Mohammad Mousavi

  • Office: E 305
  • Telephone 035 16 71 22
  • Email: []
Lecture Handouts / Slides Other Material
Lecture 1: Introduction Introduction - Slides

Introduction - Video

Lecture 2: Actions, Behavior, Abstraction Behavioral Modeling - Slides

Behavioral Modeling - Video

Lecture 3: Behavioral Equivalences Equivalences - Slides Part I

Equivalences - Slides Part II

Equivalences - Slides Part III

Trace Equiv. - Video Part I

Bisimulation - Video Part II

Weak Equiv. - Video Part III

Lecture 3: Hennessy Milner Logic HML - Slides Part I

HML - Slides Part II

HML - Slides Part III

HML - Slides Part IV

HML - Video Part I

HML - Video Part II

Modal mu-Calc. - Video Part III

Modal mu-Calc. - Video Part IV

Lecture 4: Sequential Processes Sequential Processes - Slides Part I

Sequential Processes - Slides Part II

Sequential Processes - Video Part I

Sequential Processes - Video Part II

Lecture 5: Parallel Processes Parallel Processes - Slides

Parallel Processes - Video]

System Validation at Delft Opencourseware