INFR10089/INFR11248 — 2024

 Main page Lectures and handouts Homework
Piazza Notes HW Submissions

Modelling Concurrent Systems: Syllabus

The below ordering of the treated material is w.r.t. the recorded lectures from 2020 (below linked to YouTube).
Deviations in this order made in this year's presentation are indicated in brown.
Material in grey has not yet been treated, either because it is scheduled for a future lecture, or because it didn't fit in the allotted time and was postponed.
Handouts listed [ in brackets ] are not exam material.
Week Date Lecture Notes Handouts Homework
1a17 Sept. 20242020 Lecture 1 (1:05)
  • Specification vs Implementation
  • Labelled transition systems and process graphs
  • Relay Race
  • Synchronisation and Parallel Composition
  • Syntax and Semantics of ACP (postponed to Sept. 19)
Notes Specification, Analysis and Verification
(Also used in lecture 12) 		HW 1
1b
2a		19 & 24 Sept. 2024 2020 Lecture 2 (1:02)
  • Spectrum of semantic equivalences
  • Partial and completed trace semantics
  • Abstraction from internal actions
  • Language equivalence (postponed to Oct. 1)
Notes [ The Linear Time - Branching Time Spectrum I ] HW 2
HW 3
2b
3a		26 Sept. & 1 Oct. 2024 2020 Lecture 3 (1:36)
  • Bisimulation
  • Weak bisimilarity
  • Branching bisimilarity
  • Consistent colourings
    		Notes Bisimulation
    (Also used in lectures 4 and 9)
    (The section "Non-well-founded sets" is not covered.)         		HW 4
    HW 5
    3b3 Oct. 2024 2020 Lecture 4 (1:57)
    • Recursion
    • Syntax and Semantics of CCS
    • Denotational versus operational semantics
    		Notes The process algebras CCS and CSP
    (Also used in lecture 8)     		HW 6
    4a
    4b    		8 & 10 Oct. 2024 2020 Lecture 6 (1:59)
    • Compositionality, or congruence
    • Congruence closure of a semantic equivalence
    • Equational logic
    • Sound and complete axiomatisations
    • Head normalisation
    • Guarded recursion (postponed to Oct. 17)
    • The recursive specification principle (RSP) (postponed to Oct. 17)
    		Notes [Introduction to Process Algebra] HW 7
    HW 8
    5a
    5b    		15 & 17 Oct. 2024 2020 Lecture 7 (1:35)
    • Congruence properties of weak equivalences
    • Rooted weak and branching bisimilarity
    • Complete axiomatisations for weak equivalences
    • Strongly versus weakly unguarded recursion
    • Equational axiomatisations for strong and weak partial trace equivalence.
    		Notes HW 9
    HW 10
    6a22 Oct. 2024 2020 Lecture 8 (1:20)
    • Syntax and semantics of CSP
    • Structural operational semantics
    • Congruence formats
    		Notes Structural Operational Semantics. HW 11
    6b
    7a    		24 & 29 Oct. 20242020 Lecture 9 (1:15)
    • The Hennessy-Milner logic
    • Game theoretic characterisation of strong bisimilarity (in Rec. 3)
    • Modal μ-calculus (not exam material)
    • Preorders
    • Simulation
    • HML and games for simulation equivalence.
    		Notes wikipedia page on bisimulation game

    [ Wikipedia page on Modal_μ-calculus ]     		HW 12
    HW 13
    7b31 Oct 20242020 Lecture 11 (1:00)
    • Deciding bisimilarity
      (Partition refinement algorithms for strong, branching and weak bisimilarity)
    		Notes Partition refinement algorithm
    An O(m log n) Algorithm for Branching Bisimulation.
    (Sect. 1 until "Another important insight",
    Sects. 2, 3 (until "In order to see") and 7)         		HW 14
    8a5 Nov. 20242020 Lecture 5 (1:06)
    • Safety and liveness properties
    • Progress assumption
    • Fairness assumptions
    • Deadlock, livelock and divergence
    • Divergence-preserving branching bisimilarity
    		Notes Deadlock, livelock and divergence HW 15
    8b7 Nov 2024 2020 Lecture 12 (1:12)
    • Alternating bit protocol
    • Equivalence checking versus model checking (read notes!)
    • Tools (in notes only)
    • The role of fairness assumptions in verification
    		Notes Introduction to Process Algebra
    (Pages 71-79 and 92-95)     		HW 16
    9a
    9b    		12 & 14 Nov 20242020 Lecture 10 (1:23)
    • Temporal logic
    • Translating labelled transition systems into Kripke structures
    • Modal characterisation theorems for LTL and CTL
    		Notes [Wikipedia page on LTL].
    [Wikipedia page on CTL].     		HW 17
    HW 18
    10a
    10b    		19 & 21 Nov 20242020 Lecture 13 (1:44)
    • Petri nets
    • A denotational Petri net semantics of ACP and CCS
    • Non-interleaving semantic equivalences
    • Some reasons for choosing a semantic equivalence
    • Pomsets
    		Notes Map of equivalences, and selection criteria.
    (Also used in lecture 14)
    (Page 3, minus text above figure;
    Section 1.2 on Pages 4-5; Page 7;
    Examples 1 (on Page 9-10) and 2 (on Page 12-13))
    Petri net semantics of ACP
    (Page 1 of the introduction, Sect 1,
    Sect. 2 until 2.5, and Sect. 3 without 3.4.1)         		HW 19
    HW 20
    11a28 Nov 2023 Non-examinable material:
    • Synchronous and asynchronous message passing concurrency
      versus shared memory concurrency
    • Sequential consistency and weak memory models
    • Total Store Ordering (TSO) memory model
    		Notes see also this website
    11b30 Nov 2023 2020 Lecture 14 (1:44)
    • Progress, Justness and Fairness
    • Invariants for proving safety properties
    • Reactive systems versus closed systems
    		Notes
    15Non-treated material from 20202020 Lecture 15 (1:38)
    • Reactive CTL/LTL
    • Progress, Justness and Fairness for reactive systems
    • Bisimilarity does not preserve liveness under justness
    		Notes Ensuring liveness properties
    (Sections 2–4, and especially 5)
    16 2020 Lecture 16 (1:23)
    • Fair schedulers and mutual exclusion
    		Notes CCS: It's not Fair!
    (Sections 1–5, and 7)
    17 2020 Lecture 17 (1:39)
    • Value-passing process algebras
    		Notes