Modelling of Concurrent Systems (SS 2019)

Past lecture

This page is about a lecture from past years. Up-to-date lecture material and dates can be found here.

Lecturer and Tutor:
Dr. Harsh Beohar

Technical content

The following topics are expected to be covered during this course:

  • Transition system
  • Behavioral equivalences: trace equivalence, failure equivalence, bisimulation equivalence
  • Hennessy-Milner Logic
  • Process algebra - TCP, (CCS and CSP)
  • Formal specification of hybrid systems (aka cyber physical systems).

See also the website from SS 2017 (with the slides from year 2017).

Who is this course for?

  • Master of Applied Computer Science (MAI): Computer Science for the field of application - Distributed, Reliable Systems

Literature

  • JCM Baeten, T. Basten, MA Reniers: Process Algebra : Equational Theories of Communicating Processes . Cambridge University Press, 2010.
  • Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba : Reactive Systems: Modeling, Specification and Verification . Cambridge University Press, 2007.
  • R. Milner : Communication and Concurrency . Prentice Hall, 1989.
  • CAR Hoare : Communicating sequential processes . 2004. http://www.usingcsp.com/cspbook.pdf
  • Davide Sangiorgi : On the Origins of Bisimulation, Coinduction, and Fixed Points . Technical Report 2007-24, Department of Computer Science, University of Bologna, 2007. http://www.cs.unibo.it/~sangio/DOC_public/history_to_coind.pdf
  • Pieter Cuijpers and Michel Reniers, Hybrid Process Algebra, The Journal of Logic and Algebraic Programming,  Volume 62, Issue 2,  2005,  Pages 191-245. Journal article Source. For an open source, see Chapter 2 and 3 of Cuijper's  PhD thesis available from here. 
  • ​André Platzer. Logical foundations of Cyber-Physical Systems. https://www.springer.com/de/book/9783319635873 Note: Reference for Differential dynamic logic; essentially we will focus on Chapters 4 and 5.

Tools

The following tool demo will be given in the lecture (not part of the syllabus):

Schedule

Lecture

  • Tuesday, 14-16, LF 035
  • Friday, 12-14, LF 035

Exercises

  1. Sheet 1 to be solved on 30.04.2019. Click here.
  2. Sheet 2 to be solved on 14.05.2019. 
  3. Sheet 3 to be solved on 28.05.2019.
  4. Sheet 4 to be solved on 18.06.2019.
  5. Sheet 5 to be solved on .

Examination

Yet to be decided.

Downloads

Slides

  • Introductory slides. Lecture held on 9th April 2019.
  • Slides on transition systems. Lecture held on 12th April 2019.

Lecture notes

  • Chapter on closure properties of bisimilarity and Hennessy-Milner logic.