Instructors: Madhavan Mukund, C. Aiswarya
TAs: Ashwani Anand, Sricharan
Lectures will take place from 9:10-10:25 on Wednesdays, and 10:30 - 11:45 on Fridays LH 801.
References: (will be added on the fly)
Mukund| Date | Descr | Topics covered | Resources/materials |
|---|---|---|---|
| 13/9/2019 | Lecture 10 |
Distributed alphabets, direct product automata, characterization in terms of shuffle closure |
Sections 1.1 - 1.3 of Mukund |
| 18/9/2019 | Lecture 11 |
Synchronized product automata, Boolean closure, a language that is not a synchronized product langauge |
Sections 1.4 of Mukund |
| 20/9/2019 | Lecture 12 |
Asynchronous automata, independence relation, trace closure of a word language |
Sections 1.5 of Mukund |
| 4/10/2019 | Lecture 13 |
The gossip problem, primary, primary graph .. |
Sections 1.7 ( 1.7.1, 1.7.2 ) of Mukund |
| 9/10/2019 | Lecture 14 |
The gossip problem, primary, primary graph, secondary, gossip automaton, Zielonka's theorem |
Sections 1.7, 1.6 of Mukund |
| 11/10/2019 | Lecture 15 |
Zielonka's theorem - residues - process residues - primary residues |
Sections 1.8 of Mukund |
| 18/10/2019 | Lecture 17 |
Zielonka's theorem - locally updating the primary residues - the asynchronous automaton - on determinising aynchronous automata |
Sections 1.8 , 1.9 of Mukund |
| 23/10/2019 | Lecture 18 |
On determinising aynchronous automata Finer notions of equivalence between transition systems - language equivalence, failure equivalence |
|
| 25/10/2019 | Lecture 19 |
Finer notions of equivalence between transition systems - language equivalence, failure equivalence, two way simulations, bisimulation
|
|
| 29/10/2019 | Lecture 20 |
Finer notions of equivalence between transition systems - language equivalence, failure equivalence, two way simulations, bisimulation in the presence of concurrency - \tau actions, concurrency preserving bisimulations, hereditory history preserving bisimulations |
|
| 30/10/2019 | Lecture 21 | Message sequence charts, communicating finite state machines (a.k.a. message passing automata) over an architecture/topology. Language of an MPA as set of MSCs. Membership problem decidable | Chapter 2 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 1/11/2019 | Lecture 22 | Message sequence charts, communicating finite state machines (a.k.a. message passing automata) over an architecture/topology. Reachability problem (differnt variants). Architectures yielding decidability/undecidability for local control state reachability problem. | Chapter 2 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 6/11/2019 | Lecture 23 | Decidable architectures of reachability. Under-approximate verification. Bounding the channel size. | Chapter 4 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 8/11/2019 | Lecture 24 | Tree width - path width - operations on colored graphs. finite set of operations. interpreting a graph on a sequence of operations | Chapter 4 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 13/11/2019 | Lecture 25 | path width - operations on colored graphs. finite set of operations. interpreting a graph on a sequence of operations | Chapter 4 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 15/11/2019 | Lecture 26 | finite set of operations = new finite alphabet. Finite state word automata over the sequence of operations to 1) recognize MSCs among bounded path width graphs, 2) recognize Language of a message passing automaton among the bounded path width graphs, 3) channel bounded MSCs | Chapter 4 of Lecture notes of the MPRI course Non-Sequential Theory of Distributed Systems |
| 20/11/2019 | Lecture 27 | Lossy channel systems. LCS as an over approximation of reliable channel systems. Algorithm to compute pre*. Termination proof (to be continued) -- well quasi orders. | paper by Abdulla and Jonsson |
| 22/11/2019 | Lecture 28 | well quasi orders- different definitions, Dickson's lemma, Higman's lemma - proof of termination of the algortihm from last class thanks to Higman's lemma | Chapter 1 of Lecture notes by Sylvain Schmitz and Philip Schnoebelen for WQO and its applications in the analysis of infinite state systems. |