Synthesis and some of its challenges

Abstract

The advent of a methodology of automatic synthesis (of state-based systems) adds a number of interesting facets to the setting of model-checking. In this talk we focus on some conceptual aspects arising from the basic scenario of strategy synthesis in infinite-duration two-player games, as a natural extension of model-checking. The starting point is the simple observation that modelchecking asks about the (non-) emptiness of sets while synthesis asks for a certain kind of uniformization of relations by functions. This raises a large number of questions on the classification of (word-) functions (which serve as strategies in games). We discuss basic results and recent progress, emphasizing two aspects: the definability of strategies and their "complexity" in various dimensions. These results are as yet preliminary, and we end by listing unresolved problems, for example on the logic-representation of strategies. © 2012 Springer-Verlag.