inf335 - Strategy Synthesis (Complete module description)

No participant requirements

The students learn fundamental techniques in strategy synthesis as foundation for high-level control strategies in highly autonomous systems
Professional competences
The students:

• understand the concepts of open, reactive systems and can explain their relevance
• can provide formal model of open reactive systems and their relevance for system design
• understand the concept of world models as internal representation of a systems environment
• understand and can explain the concept of strategies, and relate this to system design
• understand the relevance of information flow in distributed system
• understand the relevance of choosing the periphery of world models
• can formalize system requirements in temporal logic
• understand the relevance of assumptions in system design

Methodological competences
The students:

• methods for synthesis of winning strategies in closed systems
• methods for synthesizing remorse-free strategies in open systems
• methods for determining the perimeter of world models
• methods for cooperative strategy synthesis

Social competences
The students:

• Work in teams
• Solve complex modelling, design, and synthesis tasks in teams

Self-competences
The students:

• Reflect their actions and respect the scope of methods for strategy synthesis

The module gives an introduction to the synthesis of control strategies for highly autonomous systems. We first introduce classical game theory and present algorithms for synthesizing strategies for reactive system. We extend this to open systems, and analyze conditions, under which synthesis for distributed systems is decidable. We introduce remorse-free strategies and present compositional approaches to synthesis of remorse-free strategies. We analyze under what conditions world models allow for optimal remorse free strategies. We provide algorithms for computing weakest assumptions on the system environments under which winning strategies exist. We extend this to cooperative strategy synthesis, where multiple players cooperate in achieving jointly the system objectives. We illustrate these concepts with examples from autonomous driving.

Suggested reading:

• Werner Damm and Bernd Finkbeiner. Automatic compositional synthesis of distributed systems. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 179-193. Springer International Publishing, 2014.
• Bernd Finkbeiner and Leander Tentrup. Detecting unrealizable specifications of distributed systems. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 78-92. Springer, 2014.
• Rayna Dimitrova and Bernd Finkbeiner. Counterexample-guided synthesis of observation predicates. In Marcin Jurdzinski and Dejan Nickovic, editors, Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings, volume 7595 of Lecture Notes in Computer Science, pages 107-122. Springer, 2012.
• Werner Damm and Bernd Finkbeiner. Does it pay to extend the perimeter of a world model?. In Michael Butler and Wolfram Schulte, editors, Proceedings of the 17th International Symposium on Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 12-26. Springer-Verlag, June 2011.
• Bernd Finkbeiner and Sven Schewe. Coordination logic. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the European Association for Computer Science Logic (EACSL), Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science (LNCS), pages 305-319. Springer-Verlag, 2010.

At the end of the lecture period

Wirtten or oral exam