Reactive Synthesis

References to Reading Material

• Linear time temporal logic
  • Chapter 5 of "Principles of model checking" / Christel Baier and Joost-Pieter Katoen (available in the library)
• Automata on infinite words
  • Chapter "Automata Theory and Model Checking" in "Handbook of Model Checking" (available at https://doi.org/10.1007/978-3-319-10575-8 from the university network)
  • Chapter 4 of "Principles of model checking" / Christel Baier and Joost-Pieter Katoen (available in the library)
• Reactive Synthesis
  • Chapter "Graph Games and Reactive Synthesis" in "Handbook of Model Checking" (available at https://doi.org/10.1007/978-3-319-10575-8 from the university network)
• Games on graphs
  • Lecture notes from the Infinite Games advanced lecture, available at this link
• Zielonka’s Algorithm in Quasi-Polynomial Time
  • A Recursive Approach to Solving Parity Games in Quasipolynomial Time - Karoliina Lehtinen ; Paweł Parys ; Sven Schewe ; Dominik Wojtczak (available at this link)
• GR(1) Synthesis
  • Synthesis of Reactive(1) Designs - Roderick Bloem; Barbara Jobstmann; Nir Piterman; Amir Pnueli YanivSaʼar (available at this link )
• Bounded Synthesis
  • Bounded Synthesis - Bernd Finkbeiner and Sven Schewe (available at this link)
• Distributed Synthesis
  • Distributed Systems are Hard to Synthesize - Amir Pnueli and Roni Rosner (available at this link) 
  • Uniform Distributed Synthesis - Bernd Finkbeiner and Sven Schewe (available at this link)