finite alphabet, for an infinite number of rounds. The game is won by Eve if the ω-word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for ω-regular specifications, it is decidable whether Eve has a strategy to enforce the specification no matter what Adam does. We study the extension of Church synthesis games to the linearly ordered data domains (Q,≤) and (N,≤). In this setting, the …
Abstract
In a Church synthesis game, two players, Adam and Eve, alternately pick some element in a finite alphabet, for an infinite number of rounds. The game is won by Eve if the -word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for -regular specifications, it is decidable whether Eve has a strategy to enforce the specification no matter what Adam does. We study the extension of Church synthesis games to the linearly ordered data domains and . In this setting, the infinite interaction between Adam and Eve results in an -data word, i.e., an infinite sequence of elements in the domain. We study this problem when specifications are given as register automata. Those automata consist in finite automata equipped with a finite set of registers in which they can store data values, that they can then compare with incoming data values with respect to the linear order. Church games over are however undecidable, even for deterministic register automata. Thus, we introduce one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show that they are determined, and that deciding the existence of a winning strategy is in ExpTime, both for and . This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to -regular games. We present an application of one-sided Church games to a transducer synthesis problem. In this application, a transducer models a reactive system (Eve) which outputs data stored in its registers, depending on its interaction with an environment (Adam) which inputs data to the system.