Stud.IP Uni Oldenburg
University of Oldenburg
29.11.2023 18:58:36
inf335 - Strategy Synthesis (Complete module description)
Original version English PDF download
Module label Strategy Synthesis
Module abbreviation inf335
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Master's Programme Computing Science (Master) > Technische Informatik
  • Master's Programme Engineering of Socio-Technical Systems (Master) > Embedded Brain Computer Interaction
Responsible persons
  • Lehrenden, Die im Modul (module responsibility)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
No participant requirements
Skills to be acquired in this module
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
The students:
  • Reflect their actions and respect the scope of methods for strategy synthesis
Module contents
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.
Recommended reading
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.
Language of instruction English
Duration (semesters) 1 Semester
Module frequency annual
Module capacity unlimited
Module level
Type of module
Teaching/Learning method 1VL + 1Ü
Previous knowledge keine
Type of course Comment SWS Frequency Workload of compulsory attendance
Lecture 2 SoSe oder WiSe 28
Exercises 2 SoSe oder WiSe 28
Total module attendance time 56 h
Examination Examination times Type of examination
Final exam of module
At the end of the lecture period
Wirtten or oral exam