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.ICALP.2022.122
URN: urn:nbn:de:0030-drops-164634
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16463/
Go to the corresponding LIPIcs Volume Portal

Exibard, Léo ; Filiot, Emmanuel ; Khalimov, Ayrat

A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders

pdf-format:
LIPIcs-ICALP-2022-122.pdf (0.8 MB)

Abstract

We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain (ℕ, =). This paper extends the decidability border to the domain (ℕ, <) of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. The condition is satisfied by natural data domains like (ℕ, <). It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain (ℕ^d, <^d) of tuples of numbers equipped with the component-wise partial order and in the domain (Σ^*,≺) of finite strings with the prefix relation.

BibTeX - Entry

@InProceedings{exibard_et_al:LIPIcs.ICALP.2022.122,
  author =	{Exibard, L\'{e}o and Filiot, Emmanuel and Khalimov, Ayrat},
  title =	{{A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{122:1--122:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16463},
  URN =		{urn:nbn:de:0030-drops-164634},
  doi =		{10.4230/LIPIcs.ICALP.2022.122},
  annote =	{Keywords: Synthesis, Register Automata, Transducers, Ordered Data Domains}
}

Keywords: Synthesis, Register Automata, Transducers, Ordered Data Domains
Collection: 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI