Seminar: Process Algebras

Schedule

  • Seminar (Prof. Dr. Stefan Leue, Dr. Georgiana Caltais)
    Thursday 15:15 - 16:45  Room: PZ 901
  • 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!

Presentations

  • Aishik -- 12 January, 15:15-16:00
  • Jan-Hendrik -- 19 January, 15:15-16:00
  • Hargurbir -- 19 January, 16:00-16:45

Description

Contents

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.

Participants

Theoretically-minded Master students (Computer Science, Mathematics…)

Subject Area

Informatik der Systeme / Angewandte Informatik 

Literature

Reactive systems: Modelling, Specification and Verification [L. Aceto & al.]

Further literature will be announced.

Topics

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

Tools

  • e.g., mCRL2, UPPAAL

Credits

Credit Requirements

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:

Credits

SWS: 2
ECTS-points: 4