Weighted automata, timed automata, hybrid automata, probabilistic automata (to be elaborated)
Instructors: Madhavan Mukund, B Srivathsan
Manfred Droste and Dietrich Kuske,
Benedikt Bollig and Marc Zeitoun,
Lecture notes, MPRI (2011)
Techniques for Automatic
Verification of Real-Time Systems
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
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,
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,
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
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.
Introduction to timed languages and timed automata, closure properties of timed automata, non-closure under complement, effect of epsilon-transitions.
The region construction.
Undecidabiliy of language inclusion, universality (Section 5.2, Alur and Dill, TCS 1994).
Universality is decidable for one-clock timed automata (Ouaknine and Worrell, LICS 2004).
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).
Deterministic Timed Automata, a generic framework for determinization, some determinizable subclasses.
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).
Extending timed automata with diagonal guards; expressiveness and succinctness.
Hybrid automata: basic definitions, examples.
Hybrid automata: rectangular initialized automata, decidability (Sections 2, 3.1, 3.2 of Henzinger et al, JCSS 1998).
Hybrid automata: beyond rectangular initialized automata, undecidability (Section 4 of Henzinger et al, JCSS 1998).
Hybrid automata: lazy rectangular hybrid automata (from Agrawal and Thiagarajan, HSCC 2004).
Probabilistic systems: Discrete-time Markov chains, probability measure on paths, reachability properties (Chapters 10.1, 10.1.1, Baier and Katoen).
Discrete-time Markov chains: transient probabilities, qualititative properties, repeated reachability (Chapter 10.2, Baier and Katoen).
Markov Decision Processes: paths, probabilities and adversaries, end-components and long-run behaviour (Chapters 10.6 (part), 10.6.3 (part) Baier and Katoen).
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).