Lecture Notes
This lecture is a newly revised lecture. There is material from other courses that overlap thematically. However, this lecture is based on the handwritten notes taken during the semester.
- Overview, while programs, safety properties
- Abstract Interpretation
- Well-quasi orders & Upward-closed sets
- Well-structured domains, Abdulla's Backwards Search
- Predicate Abstraction 1, Predicate Abstraction 2, CEGAR
- IC3 Slides, Lattice Theoretic PDR
- Transition Invariants, Liveness, Transition Predicate Abstraction
- LTL 1, LTL 2
- Mu Calculus 1, Mu Calculus 2
- Algorithmic Aspects of WQO Theory, Applications of LFT, Proof of LFT 1, Proof LFT 2
- Ordinals, Ordinals
Literature
The lectures will be based upon the following books and articles. Most of them are available online.
- Naoki Kobayashi, C.-H. Luke Ong: A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS 2009: 179-188.
- C.-H. Luke Ong: On Model-Checking Trees Generated by Higher-Order Recursion Schemes. LICS 2006: 81-90.
- B. Khoussainov, A. Nerode. Automata Theory and its Applications. Birkhäuser, 2001.
- M. Hofmann and M. Lange. Automatentheorie und Logik. Springer-Verlag, 2011.
- Th. Cachat. Symbolic Strategy Synthesis for Games on Pushdown Graphs. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP, pages 704-715, Springer, 2002.
- I. Walukiewicz. Pushdown Processes: Games and Model Checking. In Journal Information and Computation - Special issue on FLOC '96, pages 234-263. Academic Press, 2001. Pages 234-263
- L. Holik, R. Meyer, S. Muskalla. Summaries for Context-Free Games. In Proc.of 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages 41:1-41:16. LIPIcs, 2016.
- O. Serre. Note on winning positions on pushdown games with omega-regular winning conditions. In Information Processing Letters, Vol 85 Issue 6, pages 285-291. Elsevier, 2003.
- D. A. Martin. A purely inductive proof of Borel determinacy. In Proc. Sympos. Pure Math., Vol 42, page 303-30. AMS, 1985.
- U. Zwick, M. Paterson. The complexity of mean payoff games on graphs. In Theoretical Computer Science, Vol. 158, Issues 1-2, pages 343-359. Elsevier, 1996.
