License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2021.28
URN: urn:nbn:de:0030-drops-136735
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13673/
Exibard, Léo ;
Filiot, Emmanuel ;
Khalimov, Ayrat
Church Synthesis on Register Automata over Linearly Ordered Data Domains
Abstract
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.
BibTeX - Entry
@InProceedings{exibard_et_al:LIPIcs.STACS.2021.28,
author = {Exibard, L\'{e}o and Filiot, Emmanuel and Khalimov, Ayrat},
title = {{Church Synthesis on Register Automata over Linearly Ordered Data Domains}},
booktitle = {38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
pages = {28:1--28:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-180-1},
ISSN = {1868-8969},
year = {2021},
volume = {187},
editor = {Bl\"{a}ser, Markus and Monmege, Benjamin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13673},
URN = {urn:nbn:de:0030-drops-136735},
doi = {10.4230/LIPIcs.STACS.2021.28},
annote = {Keywords: Synthesis, Church Game, Register Automata, Transducers, Ordered Data Words}
}
|
Keywords: |
|
Synthesis, Church Game, Register Automata, Transducers, Ordered Data Words |
|
Collection: |
|
38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
10.03.2021 |
