Selected Topics in the Theory of Concurrent Processes

The aim of the course material is to give a brief insight into the theory of reactive systems, both on the syntactic and on the semantic part. In the first chapter a labelled transition system describing structures composed of communicating and interacting, independent participants, namely, the Milner’s calculus of communicating systems (CCS), is introduced. In the next chapters syntactical properties of these systems is investigated, several kinds of process equivalences are discussed. It turns out that there is a semantical description of process equivalences, too, with the help of the so-called Hennessy–Milner logic. Then temporal properties of the systems are examined, we introduce the logics of linear temporal logic (LTL), computation tree logic (CTL) and its generalization CTL*. It is a crucial question whether a transition system satisfies a given property: problems of this nature are called model checking problems. Several solutions are offered for model checking in various temporal logics. Finally, we
close the course notes by a short discussion on processes defined by recursive equations or recursive equational systems, and on the fixpoint theorems lying in the background. In the last chapter, we introduce a logic explicitly formulating the properties of being the least or greatest fixpoints: this is the modal μ-calculus.