Course contents
- In this course, we will consider different abstract formalisms to model distribution, concurrency and communication. We also focus on systems that can exhibit infinite behaviours and how to reason about them. The course outline will be put up here.
Prerequisites
- Discrete Structures, e.g., CS105, CS207 or equivalent (hard requirement, mandatory) and Logic/Automata theory (soft requirement, recommended but not mandatory)
Reference Material
-
Lecture Notes on Petri Nets (PDF),
Javier Esparza, 2019.
-
Elementary Net Systems (PDF),
Grzegorz Rozenberg and Joost Engelfriet,
Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, Springer LNCS 1491 (1998) 12-121. -
Some Behavioural Aspects of Net Theory (PDF),
P.S. Thiagarajan,
Theoretical Computer Science, 71 (1990) 133-153. -
Place/Transition Nets (PDF),
Jörg Desel and Wolfgang Reisig,
Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, Springer LNCS 1491 (1998) 122-173. Well-Structured Transition Systems Everywhere! (PDF),
Alain Finkel and Philippe Schnoebelen,
Theoretical Computer Science 256(1-2), pages 63-92, 2001.Algorithmic Aspects of WQO Theory (PDF),
Sylvain Schmitz and Philippe Schnoebelen,
Lecture notes for MPRI Masters' course, France 2012.
Topics covered
| Date | Topics covered | |
|---|---|---|
| Lec 00: 28/07 | Introduction, course outline (PDF). | |
| Lec 01: 31/07 | Petri nets, basic definitions, examples, dynamics of a net, token game, elementary net systems, place/transition nets. Dynamics as a transition system: the reachability graph. ( reference A, B and D) - | |
| Lec 02: 04/08 | Fundamental situations: Concurrency, Conflict, Causality, Contact, Confusion. Confusion-free subclasses of nets: S-systems, T-systems ( reference A, B and C) | |
| Lec 03: 08/08 | Free-choice nets, Behavioral theory of net systems: firing sequences and Mazurkiewicz traces ( reference A and C) | |
| Lec 04: 11/08 | Behaviour of net systems: posets, extending traces, compatibility and poset on traces ( Reference C) | |
| Lec 05: 18/08 | Behavioural theory of net systems: processes, branching processes and event-structures ( Reference C) | |
| Lec 06: 21/08 | Algorithms for Petri nets: Boundedness, reachability, liveness, coverability problems. Dickson's Lemma. Algorithms for Non-termination, boundedness ( reference A) | |
| Lec 07: 25/08 | Algorithms for Petri nets: Omega-regular markings, Karp Miller Coverability trees and their finiteness, Decidability of coverability. ( reference A) | |
| Lec 08: 28/08 | Algorithms for Petri nets: Backward set-saturation algorithm for coverability, extensions, linear algebraic theory. ( reference A) | |
| Lec 09: 01/09 | Algorithms for Petri nets: Rackoff's algorithm for coverability, complexity bounds. ( reference A) | |
| 04/09 | Quiz 1 | |
| Lec 10: 08/09 | Quasi orders and well quasi orders, examples ( reference E and F) | |
| Lec 11: 11/09 | Well-structured Transition Systems: Backward set saturation and finite reachability tree algorithm, effectivity conditions ( reference E and F) | |
| Sep 13-21 | Midsem week | |
| Lec 12: 22/09 | Guest Lecture by Prof Soham Chakraborty on Event Structures in Concurrent Programs | |
| Lec 13: 25/09 | WSTS everywhere: applications to Reset Petri nets and more ( reference E and F) | |
| Lec 14: 29/09 | Applications of WSTS beyond Petri nets: Integral Programs and lossy channel systems ( reference E and F) |