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.
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.
