License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2019.24
URN: urn:nbn:de:0030-drops-109269
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10926/
Go to the corresponding LIPIcs Volume Portal

Exibard, Léo ; Filiot, Emmanuel ; Reynier, Pierre-Alain

Synthesis of Data Word Transducers

pdf-format:
LIPIcs-CONCUR-2019-24.pdf (0.5 MB)

Abstract

In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data omega-words instead, i.e., words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given or not.
In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.

BibTeX - Entry

@InProceedings{exibard_et_al:LIPIcs:2019:10926,
  author =	{L{\'e}o Exibard and Emmanuel Filiot and Pierre-Alain Reynier},
  title =	{{Synthesis of Data Word Transducers}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Wan Fokkink and Rob van Glabbeek},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10926},
  URN =		{urn:nbn:de:0030-drops-109269},
  doi =		{10.4230/LIPIcs.CONCUR.2019.24},
  annote =	{Keywords: Register Automata, Synthesis, Data words, Transducers}
}

Keywords: Register Automata, Synthesis, Data words, Transducers
Collection: 30th International Conference on Concurrency Theory (CONCUR 2019)
Issue Date: 2019
Date of publication: 20.08.2019

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