+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +**********************************************************************

Zeit: Donnerstag, 20. Dezember 2018, 16:15 Uhr Ort: Raum 9222, Gebäude E3, Ahornstr. 55

Referent: Dipl.-Inform. Benedikt Brütsch Lehrstuhl Informatik 7

Thema: Strategies in Infinite Games: Structured Reactive Programs and Transducers over Infinite Alphabets

Abstract:

In this talk, we study the construction of winning strategies in games of the following kind: Two players take turns in choosing symbols from some fixed alphabet. They play forever, thus constructing an infinite sequence of symbols. The winning condition is a set L of such sequences: Player II wins if the constructed sequence is in the set L, otherwise Player I wins. These games can be viewed as a model of reactive systems, which maintain an ongoing interaction with their environment.

We consider the so-called synthesis problem: Given a winning condition, determine whether Player II has a winning strategy, and construct such a strategy.

First, we study the synthesis of winning strategies in the form of structured reactive programs (for omega-regular winning conditions). In particular, we show an exponential lower bound for the number of (Boolean) program variables that are required in the case of winning conditions specified in linear temporal logic (LTL), roughly matching the known upper bound.

Second, we consider a more general form of the synthesis problem, where the alphabet is infinite. Specifically, we focus on the case where the symbols chosen by the players are natural numbers. To represent winning conditions, we define a model of automata over infinite alphabets such as the set N of natural numbers, namely N-memory automata. Analogously, we introduce N-memory transducers to represent strategies. We show that the synthesis problem is solvable in this setting: Given a winning condition defined by a deterministic N-memory automaton with a parity acceptance condition, we can determine which player has a winning strategy and construct such a strategy in the form of a deterministic N-memory transducer.

Es laden ein: Die Dozenten der Informatik