The course will cover a range of topics in Model Checking and its applications to distributed and multi-agent systems in a 10 day series of lectures and tutorials. For more information see the schedule below.
The course will be given by Prof. Alessio Lomuscio of Imperial College London.
The course will take place at Durand building, room 023 at Stanford Campus from 10:00am to 12:00pm between 12th - 16th and 20th - 23rd of August 2019.
This is a tentative Lectures and Tutorials breakdown. (Adjustments will be made during the course to maximise the learning objectives)
12 August:
Modal Specification Languages.
Linear Temporal Logic (LTL), Computation Tree Logic (CTL).
Tutorial: Satisfaction in LTL and CTL.
13 August:
Expressive power in LTL, CTL. The logic CTL*.
Temporal Specfications; Mutual Exclusion in LTL and CTL.
Tutorial: Specification Patterns; Mutual Exclusion.
14 August:
Mutual Exclusion Revised. The Bit Transmission Problem.
Explicit Model Checking Algorithms for LTL and CTL.
Tutorial: Explicit Model Checking.
15 August:
Binary Decision Trees, Binary Decision Diagrams.
Symbolic Model Checking.
Tutorial: Binary Decision Trees and Binary Decision Diagrams.
16 August:
Interpreted Systems. Epistemic Specifications in LTLK and CTLK.
The NuSMV Model Checker.
Tutorial: The NuSMV Model Checker.
19 August:
20 August:
Explicit and Symbolic Model Checking against Epistemic Specifications.
Epistemic analysis of the Bit Transmission Problem.
Tutorial: Satisfaction in CTLK.
21 August:
Bounded model checking.
Safety-Analysis via Fault Injection.
Tutorial: Explicit model checking for CTLK.
22 August:
Verification of strategic properties in multi-agent systems.
The MCMAS model checker.
Tutorial: The MCMAS model checker.
23 August:
Parameterized Verification for the analysis of robotic swarms. Verifiable Emergence.
Towards the verification of autonomous systems based on neural networks.
Tutorial: Cutoffs in Parameterized verification.