Weighted automata, timed automata, hybrid automata, probabilistic automata (to be elaborated)
Instructors: Madhavan Mukund, B Srivathsan
Weighted Automata,
Manfred Droste and Dietrich Kuske,
Preprint
Weighted Automata,
Benedikt Bollig and Marc Zeitoun,
Lecture notes, MPRI (2011)
Techniques for Automatic
Verification of Real-Time Systems
Rajeev Alur,
PhD Thesis, Stanford (1991)
A Theory of Timed Automata
Rajeev Alur and David Dill,
Theoretical Computer Science 126(2) (1994) 183-235.
Decision problems for timed automata: A
survey,
Rajeev Alur and P. Madhusudan,
4th Intl. School on Formal Methods for Computer,
Communication, and Software Systems: Real Time (2004).
On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap,
Joël Ouaknine and James Worrell,
Proc LICS 2004 (2004).
From Qualitative to Quantitative Analysis of Timed Systems,
Patricia Bouyer,
Habilitation Thesis (2009).
Timed automata: Semantics, algorithms and tools,
Johan Bengtsson and Wang Yi,
Lectures on Concurrency and Petri Nets, Springer (2004).
Alternating Timed Automata,
Slawomir Lasota and Igor Walukiewicz,
ACM Transactions on Computational Logic, 9(2) (2008).
An Introduction to Hybrid Automata,
Jean-Francois Raskin,
in Dimitros Hristu-Varsakelis, William S. Levine
(Eds.),
Handbook of Networked and Embedded Control
Systems Birkhauser (2005), 491-518.
What's Decidable about Hybrid Automata?,
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri and Pravin Varaiya,
Journal of Computer and Systems Sciences 57(1),
(1998) 94-124.
Lazy Rectangular Hybrid Automata,
Manindra Agrawal and P. S. Thiagarajan,
Proc HSCC 2004.
Principles of Model Checking (Chapter 10),
Christel Baier and Joost-Pieter Katoen,
MIT Press (2008).
Lectures on Probabilistic Model
Checking (slides),
Dave Parker.
Lecture 1, 5 Jan 2015 (Madhavan)
Introduction to weighted automata: examples, basic definitions
Lecture 2, 7 Jan 2015 (Madhavan)
Weighted systems: generalized Floyd-Warshall algorithm; Weighted automata: NFAs and probabilistic systems.
Lecture 3, 19 Jan 2015 (Madhavan)
Examples of semi-rings; Weighted automata: examples, typical decision problems; Probabilisitc automata: basic definitions, stochastic languages.
Lecture 4, 28 Jan 2015 (Madhavan)
Probabilistic automata: Stochastic languages are not r.e, threshold language for isolated cutpoint is regular .
Lecture 5, 30 Jan 2015 (Madhavan)
Probabilistic automata: Undecidability of threshold languages in general, undecidability of identifying cut points, value 1 problem (sketch), decidability of equality (sketch).
Lecture 6, 04 Feb 2015 (Madhavan)
Rational and recognizable formal power series: statement of Kleene-Schutzenberger theorem; Series over the integer semiring: encoding polynomials with integer coefficents, overview of negative and positive results; Transducers: overview of negative and positive results.
Lecture 7, 16 Feb 2015 (Srivathsan)
Introduction to timed languages and timed automata, closure properties of timed automata, non-closure under complement, effect of epsilon-transitions.
Lecture 8, 18 Feb 2015 (Srivathsan)
The region construction.
Lecture 9, 02 Mar 2015 (Srivathsan)
Undecidabiliy of language inclusion, universality (Section 5.2, Alur and Dill, TCS 1994).
Lecture 10, 04 Mar 2015 (Srivathsan)
Universality is decidable for one-clock timed automata (Ouaknine and Worrell, LICS 2004).
Lecture 11, 09 Mar 2015 (Srivathsan)
Reachability for timed automata using zones, Backward analysis and forward analysis (Section 3.1–3.5 of Bouyer's Habilitation thesis).
Lecture 12, 11 Mar 2015 (Srivathsan)
Graph representation for zones, algorithms for operations needed in forward analysis (Sections 4.1, 4.2 and the Appendix of Bengtsson and Yi, 2004).
Lecture 13, 16 Mar 2015 (Srivathsan)
Deterministic Timed Automata, a generic framework for determinization, some determinizable subclasses.
Lecture 14, 18 Mar 2015 (Srivathsan)
Alternating timed automata, closure properties, expressiveness of 1-clock ATA, decidability questions (Lasota and Walukiewicz, ACM TOCL 2008).
Lecture 15, 23 Mar 2015 (Srivathsan)
Non-Zeno infinite runs; using regions to find non-Zeno infinite runs that visit an accepting state infinitely often (Definitions 4.10 and 4.11, Lemma 4.13 of Alur and Dill, TCS 1994).
Lecture 16, 25 Mar 2015 (Srivathsan)
Extending timed automata with diagonal guards; expressiveness and succinctness.
Lecture 17, 30 Mar 2015 (Madhavan)
Hybrid automata: basic definitions, examples.
Lecture 18, 01 Apr 2015 (Madhavan)
Hybrid automata: rectangular initialized automata, decidability (Sections 2, 3.1, 3.2 of Henzinger et al, JCSS 1998).
Lecture 19, 06 Apr 2015 (Madhavan)
Hybrid automata: beyond rectangular initialized automata, undecidability (Section 4 of Henzinger et al, JCSS 1998).
Lecture 20, 08 Apr 2015 (Madhavan)
Hybrid automata: lazy rectangular hybrid automata (from Agrawal and Thiagarajan, HSCC 2004).
Lecture 21, 13 Apr 2015 (Madhavan)
Probabilistic systems: Discrete-time Markov chains, probability measure on paths, reachability properties (Chapters 10.1, 10.1.1, Baier and Katoen).
Lecture 22, 15 Apr 2015 (Madhavan)
Discrete-time Markov chains: transient probabilities, qualititative properties, repeated reachability (Chapter 10.2, Baier and Katoen).
Lecture 23, 20 Apr 2015 (Madhavan)
Markov Decision Processes: paths, probabilities and adversaries, end-components and long-run behaviour (Chapters 10.6 (part), 10.6.3 (part) Baier and Katoen).
Lecture 24, 22 Apr 2015 (Madhavan)
Markov Decision Processes: Qualitative reachability, Optimality equation (Bellman), Memoryless adversaries, Quantitative reachability—value iteration, linear programming, policy iteration (Chapter 10.1 (part), Baier and Katoen).