About the Course

We present formal modeling languages and analysis tools for discrete-event dynamical systems, with special emphasis on applications from computer science and biology. The languages we discuss are based on mathematical logic, rewrite rules, automata, circuits, and programming constructs. The analysis methods include model checking, theorem proving, and abstract interpretation. We give brief introductions to advanced models incorporating time, probabilities, game-theoretic aspects, and continuous behavior.

  • Instructors: Thomas A. Henzinger, Krishnendu Chatterjee
  • Teaching Assistants: Pavol Cerny, Arjun Radhakrishna
  • Time:
    • Lectures: 2 weekly 75 min lectures Tuesdays and Thursdays, 1:45 - 3:00
      Starts Thursday, October 4th, 2012.
    • Recitations: Wednesdays, 12.45pm-1.35pm
  • Location: Seminar Room Mondi 3, IST Austria
  • Grading: The course will be graded based on
    • Examination on 22nd November, 2012 from 13:45 to 15:00 (50% of the grade)
    • Weekly homeworks (50% of the grade)
  • Credits: 3ECTS
  • Registration: We ask that those interested in taking the course register with the Graduate School at IST at least 1 week before the course starts. You can register here.
  • Shuttle: IST Austria operates a shuttle-bus, from Heiligenstadt (terminus of the U4) to our campus. Check here for the schedule. The course invitation can be used as a ticket for the shuttle.

Tentative Schedule

Date Lecturer Topic Slides/Notes
October 4th, 2012 Thomas A. Henzinger Formal Systems Notes
October 9th, 2012 Thomas A. Henzinger Automata Notes
October 11th, 2012 Thomas A. Henzinger Reactive Modules Notes
October 16th, 2012 Thomas A. Henzinger Reactive Modules. Functions. Notes
October 18th, 2012 Thomas A. Henzinger Operational and Axiomatic Semantics. Invariants. Notes
October 23rd, 2012 Krishnendu Chatterjee Graph Algorithms Notes
October 25th, 2012 Krishnendu Chatterjee Markov chains Notes
October 30th, 2012 Krishnendu Chatterjee Markov Decision Processes -- Qualitative Analysis Notes
November 6th, 2012 Krishnendu Chatterjee Markov Decision Processes -- Quantitative Analysis Notes
November 8th, 2012 Krishnendu Chatterjee Games Notes
November 13th, 2012 Thomas A. Henzinger Programming Languages Notes
November 20th, 2012 Krishnendu Chatterjee Timed and Hybrid Systems --
November 22nd, 2012 Krishnendu Chatterjee Examination -- 13:45 to 15:00 --


Recitations

Date TA Topic Slides/Notes
October 10th, 2012 Pavol Cerny Formal Systems, Automata Exercises
October 17th, 2012 Pavol Cerny Reactive Modules Exercises
October 24th, 2012 Pavol Cerny Operational and Axiomatic Semantics. Invariants. Exercises
October 31st, 2012 Arjun Radhakrishna Markov Chains, and Qualitative analysis of MDPs --
November 7th, 2012 Arjun Radhakrishna Quantitative analysis of MDPs --
November 14th, 2012 Arjun Radhakrishna Reachability and Buchi Games --
November 21st, 2012 Pavol Cerny Programming Languages Exercises


Homework

Date Topic
25th October, 2012 Graph algorithms and Markov Chains [pdf]
25th October, 2012 MDPs and Games [pdf]