Topics in Concurrency Lecture Notes
Glynn Winskel · 2009
Prerequisite courses: Semantics of Programming Languages Aims The aim of this course is to introduce fundamental concepts and techniquesin the theory of concurrent processes. It will provide languages, models, logics and methods to formalise and reason about concurrent systems. Lecture plan * Simple parallelism and nondeterminism. Dijkstra's guarded com-mands. Communication by shared variables: A language of parallel commands. [1 lecture] * Communicating processes. Milner's Calculus of Communicating Pro-cesses (CCS). Pure CCS. Labelled-transition-system semantics. Bisimulation and weak bisimulation equivalence. Equational consequences andexamples. [3 lectures] * Specification and model-checking. The modal u-calculus. Its math-ematical foundations in Tarski's fixed point theorem. Its relation with Temporal Logic. Introduction to model checking. Bisimulation checking.Examples. [3 lectures] * Introduction to Petri nets. Petri nets, basic definitions and concepts.Petri-net semantics of CCS. [1 lecture]