2026-07-23T04:49:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13673 2024-03-06T10:52:37Z ddc:004 open_access

Church Synthesis on Register Automata over Linearly Ordered Data Domains Exibard, Léo Filiot, Emmanuel Khalimov, Ayrat Synthesis Church Game Register Automata Transducers Ordered Data Words Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data ω-words. We study the synthesis problem for specifications given as register automata over a linearly ordered data domain (e.g. (ℕ, ≤) or (ℚ, ≤)), which allow for comparison of data with regards to the linear order. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately play some data, and Eve wins whenever their interaction complies with the specification, which is a language of ω-words over ordered data. Such games are however undecidable, even when the specification is recognised by a deterministic register automaton. This is in contrast with the equality case, where the problem is only undecidable for nondeterministic and universal specifications. Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and 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. Lastly, we apply these results to the transducer synthesis problem for input-driven register automata, where each output data is restricted to be the content of some register, and show that if there exists an implementation, then there exists one which is a register transducer. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Léo Exibard and Emmanuel Filiot and Ayrat Khalimov 2021 Is Part Of LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2021.28 urn:nbn:de:0030-drops-136735 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.28 eng https://creativecommons.org/licenses/by/4.0/legalcode