English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In a Church synthesis game, two players, Adam and Eve, alternately pick someelement in a finite alphabet, for an infinite number of rounds. The game is wonby Eve if the omega-word formed by this infinite interaction belongs to a givenlanguage S, called the specification. It is well-known that for omega-regularspecifications, it is decidable whether Eve has a strategy to enforce thespecification no matter what Adam does. We study the extension of Churchsynthesis games to the linearly ordered data domains (Q, <) and (N, <). In thissetting, the infinite interaction between Adam and Eve results in an omega-dataword, 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 ofregisters in which they can store data values, that they can then compare withincoming data values with respect to the linear order. Church games over (N, <)are however undecidable, even for deterministic register automata. Thus, weintroduce one-sided Church games, where Eve instead operates over a finitealphabet, 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 Qand N. This follows from a study of constraint sequences, which abstract thebehaviour of register automata, and allow us to reduce Church games toomega-regular games. We present an application of one-sided Church games to atransducer synthesis problem. In this application, a transducer models areactive system (Eve) which outputs data stored in its registers, depending onits interaction with an environment (Adam) which inputs data to the system.

Church Synthesis on Register Automata over Linearly Ordered Data Domains