Stud.IP Uni Oldenburg
University of Oldenburg
12.07.2020 13:00:41
inf335 - Strategy Synthesis (Complete module description)
Original version English Download as PDF
Module label Strategy Synthesis
Module code inf335
Credit points 6.0 KP
Workload 180 h
Faculty/Institute Department of Computing Science
Used in course of study
  • Master's Programme Computing Science (Master) >
  • Master's Programme Engineering of Socio-Technical Systems (Master) >
Contact person
Module responsibility
Authorized examiners
Entry 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.
Reader's advisory
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 once a year
Module capacity unlimited
Modullevel AS (Akzentsetzung / Accentuation)
Modulart Pflicht o. Wahlpflicht / compulsory or optioal
Lern-/Lehrform / Type of program V+Ü
Vorkenntnisse / Previous knowledge
Course type Comment SWS Frequency Workload attendance
Lecture 2.00 SuSe and WiSe 28 h
Exercises 2.00 SuSe and WiSe 28 h
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
At the end of the lecture period
Wirtten or oral exam