Modelling of Concurrent Systems (SS 2017)

Lecturer and Tutor:
Dr. Harsh Beohar

Technical content

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

  • Transitions system
  • Behavioural equivalences: Trace equivalence, Failure equivalence, Bisimulation equivalence
  • Closure properties of bisimulation relations and Hennessy-Milner Logic
  • Process algebra - TCP, (CCS and CSP)
  • Probabilistic process algebra
  • Event structures

Who is this course for?

  • Master Angewandte Informatik (MAI): Informatik für den Anwendungsbereich - Verteilte, Verlässliche Systeme

Literature

  • J.C.M. Baeten, T. Basten, M.A. Reniers: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, 2010.
  • Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
  • R. Milner: Communication and Concurrency. Prentice Hall, 1989.
  • C.A.R. 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_bis_coind.pdf
  • Winskel G. (1989) An introduction to event structures. In: de Bakker J.W., de Roever W.P., Rozenberg G. (eds) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. REX 1988. Lecture Notes in Computer Science, vol 354. Springer, Berlin, Heidelberg
  • Winskel G. (1986) Event structures. Invited lectures for the Advanced Course on Petri Nets, Sept. 1986. Appears as a report of the Computer Laboratory, University of Cambridge, 1986. https://www.cl.cam.ac.uk/~gw104/EvStr.pdf

Tools

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

Schedule

Lecture

  • Monday, 12-14, LK 053
  • Thursday, 10-12, LB 117

Downloads

Slides

  • Organisation and Introduction [24.04.2017]. Click here.
  • Bisimulation algorithm [08.05.2017]. Click here.
  • Confluence [17.07.2017] and Probabilistic BSP [20-24.07.2017]. Click here.

Exercise sheets

  • Sheet 1 (to be solved on 11.05.2017)
  • Sheet 2 (to be solved on 29.05.2017)
  • Sheet 3 (to be solved on 30.06.2017)
  • Sheet 4 (to be solved on 14.07.2017)
  • Sheet 5 (to be solved on 27.07.2017)