| Week |
Date |
Lecture |
Notes |
Handouts |
Homework |
| 1a | 19 Sept. 2023 | 2020 Lecture 1 (1:05)
- Specification vs Implementation
- Labelled transition systems and process graphs
- Relay Race
- Synchronisation and Parallel Composition
- Syntax and Semantics of ACP
| Notes |
Specification, Analysis and Verification
(Also used in lecture 12)
| HW 1 |
| 1b | 21 Sept. 2023 | 2020 Lecture 2 (1:02)
- Spectrum of semantic equivalences
- Partial and completed trace semantics
- Abstraction from internal actions
- Language equivalence
| Notes |
[
The Linear Time - Branching Time Spectrum I ]
| HW 2 |
| 2a | 26 Sept. 2023 | 2020 Lecture 3 (1:36)
- Bisimulation
- Weak bisimilarity
- Branching bisimilarity
- Consistent colourings
(postponed to Nov 9 and 14)
| Notes |
Bisimulation
(Also used in lectures 4 and 9)
(The section "Non-well-founded sets" is not covered.)
| HW 3 |
| 2b | 28 Sept. 2023 | 2020 Lecture 4 (1:57)
- Recursion
- Syntax and Semantics of CCS
(postponed to Oct 3)
- Denotational versus operational semantics
(continued on Oct 5)
| Notes |
The process algebras CCS and CSP
(Also used in lecture 8)
| HW 4 |
| 3a | 3 Oct. 2023 | In response to questions (lecture 5):
- Process graphs versus LTSs (in Recordings 1 and and 4)
- Syntax and Semantics of CCS (in Recording 4)
- Absolute and relative expressiveness
- RDP & RSP: unique solutions of guarded recursive specs. (in Rec. 6)
| Notes |
| HW 5 |
| skipped | 2020 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
| |
3b
4a | 5 & 10 Oct. 2023 | 2020 Lecture 6 (1:59)
- Compositionality, or congruence
- Congruence closure of a semantic equivalence
- Equational logic
- Sound and complete axiomatisations
- Head normalisation
- Guarded recursion (treated on Oct 3)
- The recursive specification principle (RSP) (treated on Oct 3)
| Notes |
[Introduction to Process Algebra]
| HW 6
HW 7 |
| 4b | 12 Oct. 2023 | 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
| Notes |
| HW 8 |
| 5a | 17 Oct. 2023 | 2020 Lecture 8 (1:20)
- Syntax and semantics of CSP
- Structural operational semantics
- Congruence formats
| Notes |
Structural Operational Semantics.
| HW 9 |
5b
6a | 19 Oct. 2023
24 Oct. 2023 | 2020 Lecture 9 (1:15)
- The Hennessy-Milner logic
- Preorders
- Simulation
| Notes |
| HW 10
HW 11 |
| 6b | 26 Oct. 2023 | No 2020 lecture
- Game theoretic characterisation of strong bisimilarity
(in Rec. 3)
- HML and games for simulation equivalence.
- Equational axiomatisations for strong and weak partial trace equivalence.
| Notes |
wikipedia page on
bisimulation game |
HW 12 |
7a
7b
8a | 31 Oct 2023
2 Nov 2023
7 Nov 2023 | 2020 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 13
HW 14
HW 15 |
8b
9a | 9 Nov 2023
14 Nov 2023 | 2020 Lecture 11 (1:00)
- Consistent colourings
(see Lecture 3, 26 Sept.)
(an alternative for bisimulation as a witness for bisimilarity)
- Deciding bisimilarity
(Partition refinement algorithms for strong,
branching and weak bisimilarity)
- Some remarks on the GSOS format (with negative premises)
(see Lecture 8, 17 Oct.)
| 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 16
HW 17 |
| 9b | 16 Nov 2023 | 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
(treated on Nov 21)
| Notes |
Introduction to Process Algebra
(Pages 71-79 and 92-95)
| HW 18 |
10a
10b | 21 & 23 Nov 2023 | 2020 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 |
|
| 11a | 28 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
| |
| 11b | 30 Nov 2023 | 2020 Lecture 14 (1:44)
- Progress, Justness and Fairness
- Invariants for proving safety properties
- Reactive systems versus closed systems
| Notes |
| |
|
| 15 | Non-treated material from 2020 | 2020 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 |
| |