Course contents
- The course is concerned with modeling, specification and analysis of hardware, software and intelligent systems with a focus on quantitative aspects such as time, probability, cost, and their combinations. The course outline will be available here.
- Our focus is to ask and automatically answer questions on safety, dependability, predicability and performance, such as "Can the system crash within the next 30s?", "What is the probability of a system failure in the next 24 hours?"
- The course will be tentatively split into 4 modules:
- 1. Basic probabilistic models: Markov chains and Markov decision processes (MDP). We consider both state-based and distributional settings and introduce state of the art verification techniques and tools.
- 2. Quantitative Automata Models and Verification. This will include Timed Automata, Hybrid automata and Weighted Automata and basic decidability and complexity issues for these models.
- 3. Quantitative logics, richer specification and reasoning. In this module we consider probabilistic logics and quantitative specifications in general, as well as some specific algorithms to reason about them.
- 4. Applications to intelligent systems. This module will include quantitative modeling of decision tree ensembles and neural networks. For all these models, we will consider several properties of interest including robustness, fairness, sensitivity, explainability.
Prerequisites
- Discrete Structures, e.g., CS105 or CS207 or equivalent (hard requirement, mandatory), basic mathematics, linear algebra. Some background on logic and/or automata/ToC will be useful, but is not mandatory.
- UG (2nd yr or above) and PG students can take the course.
Assessment
- Quizzes (~25-30% wtg), exams (~35% wtg) and paper presentations (~25-30% wtg). Participation, via, e.g., pop quizzes (~10% wtg)
Reference Material
Probabilistic Models
-
Chapter 10 of the book "Principles of Model Checking", MIT Press, May 2008, by Christel Baier and Joost-Pieter Katoen (Reference A)
-
Various proofs of the Fundamental Theorem of Markov Chains, Lecture notes by Prof. Somenath Biswas (Reference B)
Quantitative Automata
-
A theory of timed automata, OG paper by Rajeev Alur and David Dill (Reference I)
-
An introduction to timed automata, by Patricia Bouyer (Reference II)
-
Decision Problems for Timed Automata: A Survey, by Rajeev Alur and P Madhusudan (Reference III)
-
Event-clock automata: A determinizable class of timed automata. R. Alur, L. Fix and T. A. Henzinger. Theor. Comp. Sci., 211(1-2): 253-273, 1999 (Reference IV)
-
Reachability Algorithm Using Zones. B. Srivathsan, Lecture Notes (Reference V)
Topics covered
| Date | Topics covered | Reference |
|---|---|---|
| Lec 00: 6 Jan | Introduction, course outline | Slides |
| Lec 01: 9 Jan | Discrete-time Markov chains (DTMCs), basic definitions and examples | Reference A |
| Lec 02: 13 Jan | DTMCs as stochastic processes, Transient and Path-based Properties, Probability spaces and cylinder sets, Probabilistic Reachability | Reference A |
| Lec 03: 16 Jan | Algorithms for path-based probabilistic reachability, linear equations, iterative algorithms | Reference A |
| Lec 04: 20 Jan | Qualitative properties, Bottom strongly connected components (BSCCs), Algorithm for almost sure reachability, steady-state distributions | Reference A |
| Lec 05: 23 Jan | Steady-state reachability, irreducible and aperiodic Markov chains, Fundamental theorem | Reference A |
| Lec 06: 27 Jan | Proof of Fundamental theorem of Markov chains | Reference B |
| Lec 07: 30 Jan | Markov decision processes (MDPs) | Reference A |
| Lec 08: 03 Feb | Algorithms for reachability in Markov decision processes: Value iteration, linear programming | Reference A |
| Lec 09: 06 Feb | More algorithms for reachability in Markov decision processes: Policy iteration; MDPs as distribution transformers | Reference A |
| Lec 10: 10 Feb | Tools for probabilistic verification: PRISM and Storm (Demo by Osim Abes) | Reference A |
| 12 Feb | Quiz 1 | |
| Lec 11: 13 Feb | Distributional safety and reachability in Markov chains and MDPs. Start of New Module on Quantitative Automata, timed words | Reference I |
| Lec 12: 17 Feb | Module 2 on Quantitative Automata: Timed automata, timed regular languages | Reference I and Reference II |
| Lec 13: 20 Feb | Boolean operations, Properties of Timed automata: emptiness, universality, region construction, deterministic timed automata | Reference I , Reference II, and Reference III |
| Lec 14: 03 Mar | Event recording, predicting and event clock automata | Reference IV |
| Lec 15: 06 Mar | Zones for reachability in timed automata, timed automata extensions | Reference V |
| Lec 16: 10 Mar | Timed automata extensions, GTA, Tools for timed automata: Uppaal, TChecker (Demo by Prerak Contractor) | Reference II++ |
| Lec 17: 13 Mar | A primer to Quantitative Logics: PCTL, PCTL*, MTL etc | Reference A++ |