Seminar: Process Algebras
- The deadline for the seminar report is March 12!
- the report has to be sent in .pdf format via email to georgiana.caltais at uni-konstanz dot de
- The first session, 27th of October, 13:30-15:00, is mandatory for every student who wants to give a talk!
- Aishik -- 12 January, 15:15-16:00
- Jan-Hendrik -- 19 January, 15:15-16:00
- Hargurbir -- 19 January, 16:00-16:45
One of the research areas of great importance in Computer Science is the study of the semantics of concurrent reactive systems. These are systems that compute by interacting with their environment, and typically consist of several parallel components, which execute simultaneously and potentially communicate with each other. Examples of such systems range from rather simple devices such as calculators and vending machines, to programs controlling mechanical devices such as cars, subways or spaceships. In light of their widespread deployment and complexity, the application of rigorous methods for the specification, design and reasoning on the behaviour of reactive systems has always been a great challenge.
Process algebras are prototype specification languages for reactive systems. They come equipped with a notion of ‘syntax’ for expressing reactive systems as (communicating) ‘process terms’ and an associated notion of behavioural equivalence. The latter can be verified in an automatic/algorithmic fashion via ‘equational reasoning’ or ‘bisimulation’, for instance. Equational reasoning has the advantage of not generating the state space of processes, when checking for behavioural compliance. Hence, it can potentially combat the state explosion problem. Reasoning on processes can also be performed via model-checking, where system specifications are expressed as formulae in Hennessy Milner Logic, for instance. The latter has the advantage of completely characterising bisimilarity for a large class of reactive systems.
The seminar will help the participants to gain more insight into the abstract world of algebraic process theory, its applications, tools and future / open research directions.
The seminar will be held in English.
Theoretically-minded Master students (Computer Science, Mathematics…)
Informatik der Systeme / Angewandte Informatik
Reactive systems: Modelling, Specification and Verification [L. Aceto & al.]
Further literature will be announced.
Algebraic Process Theories (with time)
- Syntax. Semantics. Behavioural equivalence.
Hennessy-Milner Logic (with time)
- The logic. Applications to system analysis.
Rule Formats for Behavioural Equivalence
- e.g., GSOS
- e.g., mCRL2, UPPAAL
30 min. presentation + 15 min. discussion
- written report (8-10 pages)
- presence and active participation during the presentations of the other students
- language for presentation and report will be English
The grading schemes can be found here: