Modelling of Concurrent Systems (SS 2019)
Past lectureThis 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
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
- 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.
The following tool demo will be given in the lecture (not part of the syllabus):
- Tuesday, 14-16, LF 035
- Friday, 12-14, LF 035
- Sheet 1 to be solved on 30.04.2019. Click here.
- Sheet 2 to be solved on 14.05.2019.
- Sheet 3 to be solved on 28.05.2019.
- Sheet 4 to be solved on 18.06.2019.
- Sheet 5 to be solved on .
Yet to be decided.
- Introductory slides. Lecture held on 9th April 2019.
- Slides on transition systems. Lecture held on 12th April 2019.