|
| Date |
Lecture |
Notes |
Handouts |
Homework |
| 1 | 1 June 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 |
| 2 | 2 June 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 |
| 3 | 9 June 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 3 |
| 4 | 15 June 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 4 |
| 5 | 16 June 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
| HW 5 |
| 6 | 22 June 2020 | Lecture 6 (1:59)
- Compositionality, or congruence
- Congruence closure of a semantic equivalence
- Equational logic
- Sound and complete axiomatisations
- Head normalisation
- Guarded recursion
- The recursive specification principle (RSP)
| Notes |
| HW 6 |
| 7 | 23 June 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 7 |
| 8 | 29 June 2020 | Lecture 8 (1:20)
- Syntax and semantics of CSP
- Structural operational semantics
- Congruence formats
| Notes |
Structural Operational Semantics.
| HW 8 |
| 9 | 30 June 2020 | Lecture 9 (1:15)
- The Hennessy-Milner logic
- Preorders
- Simulation
| Notes |
[
Wikipedia page on Modal_μ-calculus ]
| HW 9 |
| 10 | 13 July 2020 | Lecture 10 (1:23)
- Modal and temporal logic
(Seminar presentation by Vivian Dang)
- Temporal logic
- Translating labelled transition systems into Kripke structures
- Modal characterisation theorems for LTL and CTL
| Notes |
Vivian's slides
Wikipedia page on LTL.
Wikipedia page on CTL.
| HW 10 |
| 11 | 14 July 2020 | Lecture 11 (1:00)
- Hennessy–Milner Logics: Weak and Branching Bisimulation
(Seminar presentation by Vincent Jackson)
- Deciding bisimilarity
(Partition refinement algorithms for strong,
branching and weak bisimilarity)
| Notes |
Vincent's slides
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 11 |
| 12 | 20 July 2020 | Lecture 12 (1:12)
- Alternating bit protocol
- Equivalence checking versus model checking
- Tools (in notes only)
- The role of fairness assumptions in verification
| Notes |
Introduction to Process Algebra
(Pages 71-79 and 92-95)
| HW 12 |
| 13 | 21 July 2020 | Lecture 13 (1:44)
- Petri nets
(Zoom session with collective watching of
recorded seminar presentation by Tiankuang Zhang)
- Petri nets
- A denotational Petri net semantics of ACP and CCS
- Non-interleaving semantic equivalences
- Some reasons for choosing a semantic equivalence
- Pomsets
| Notes |
Presentation by Tiankuang Zhang keynote
and pdf
Youtube Playlist
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 13 |
| 14 | 27 July 2020 | Lecture 14 (1:44)
- Progress, Justness and Fairness
- Invariants for proving safety properties
- Reactive systems versus closed systems
| Notes |
| HW 14 |
| 15 | 28 July 2020 | Lecture 15 (1:38)
- Reasoning about knowledge in distributed systems
(Recorded seminar presentation by
Courtney Darville with live question time)
- Reactive CTL/LTL
- Progress, Justness and Fairness for reactive systems
- Bisimilarity does not preserve liveness under justness
| Notes | Courtney's
Youtube1,
2,
3 and
4.
Ensuring
liveness properties
(Sections 2–4, and especially 5)
| HW 15 |
| 16 | 3 August 2020 | Lecture 16 (1:23)
- Fair schedulers and mutual exclusion
| Notes |
CCS: It's not Fair!
(Sections 1–5, and 7)
| HW 16 |
| 17 | 4 August 2020 | Lecture 17 (1:39)
- Algorithmic verification
(Seminar presentation by Aidan Farrell)
- Value-passing process algebras
| Notes |
Aidan's slides
| HW 17 |
| 18 | 10 August 2020
15:00 (zoom) | Wrap up: probably
like the tutorials | | |