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: Thorsten Tarrach, Andreas Pavlogiannis
  • Time:
    • Lectures: 2 weekly 75 min lectures Tuesdays and Thursdays, 13:00 - 14:15
      Starts Tuesday, November 26th, 2012.
    • Recitations: Thursdays, 14:30pm-15:20pm
  • Location: Seminar Room Mondi 3, IST Austria
  • Grading: The course will be graded based on
    • Examination (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 Notes, HW
Tuesday, 26th Nov, 2013 Thomas A. Henzinger Formal Systems Notes
Thursday, 28th Nov, 2013 Thomas A. Henzinger Automata Notes, HW
Thursday, 5th Dec, 2013 Thomas A. Henzinger Automata, Reactive Modules Notes, HW
Tuesday, 10th Dec, 2013 Thomas A. Henzinger Reactive Modules. Functions. Notes
Thursday, 12th Dec, 2013 Thomas A. Henzinger Operational and Axiomatic Semantics. Invariants. Notes, HW
Tuesday, 17th Dec, 2013 Thomas A. Henzinger Axiomatic Semantics. Invariants. Notes, HW
Tuesday, 7th Jan, 2014 Krishnendu Chatterjee Graph Algorithms Notes
Thursday, 9th Jan, 2014 Krishnendu Chatterjee Markov chains Notes, HW
Tuesday, 14 Jan, 2014 Krishnendu Chatterjee Markov Decision Processes Notes , HW
Thursday, 16 Jan, 2014 Krishnendu Chatterjee Markov Decision Processes - Quantitative Analysis, Games Notes , HW
Tuesday, 21 Jan, 2014 Krishnendu Chatterjee Games Notes
Thursday, 23 Jan, 2014 Krishnendu Chatterjee Games -
Tuesday, 28 Jan, 2014 Exam -


Recitations

Date TA Topic Notes
Thursday, 28th Nov, 2013 Thorsten Tarrach Formal Systems, Automata Notes
Thursday, 5th Dec, 2013 Thorsten Tarrach Reactive Modules Notes
Thursday, 12th Dec, 2013 Thorsten Tarrach Reactive Modules, Operational Semantics Notes
Thursday, 19th Dec, 2013 Andreas Pavlogiannis Axiomatic Semantics, Invariants Notes
Thursday, 9th Jan, 2014 Andreas Pavlogiannis Graphs, Markov Chains Notes
Thursday, 16th Jan, 2014 Andreas Pavlogiannis Quantitative analysis of MDPs Notes


Past Notes

Lecturer Topic Slides/Notes
Thomas A. Henzinger Formal Systems Notes
Thomas A. Henzinger Automata Notes
Thomas A. Henzinger Reactive Modules Notes
Thomas A. Henzinger Reactive Modules. Functions. Notes
Thomas A. Henzinger Operational and Axiomatic Semantics. Invariants. Notes
Krishnendu Chatterjee Graph Algorithms Notes
Krishnendu Chatterjee Markov chains Notes
Krishnendu Chatterjee Markov Decision Processes -- Qualitative Analysis Notes
Krishnendu Chatterjee Markov Decision Processes -- Quantitative Analysis Notes
Krishnendu Chatterjee Games Notes
Thomas A. Henzinger Programming Languages Notes