Church Synthesis on Register Automata over Linearly Ordered Data Domains

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 omega-word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for omega-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 infinite interaction between Adam and Eve results in an omega-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 (N, <) 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 Q and N. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to omega-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.