Léo Exibard ; Emmanuel Filiot ; Pierre-Alain Reynier - Synthesis of Data Word Transducers

lmcs:5982 - Logical Methods in Computer Science, March 18, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:22)2021
Synthesis of Data Word Transducers

Authors: Léo Exibard ; Emmanuel Filiot ; Pierre-Alain Reynier

    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 nondeterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for nondeterministic 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.

    Volume: Volume 17, Issue 1
    Published on: March 18, 2021
    Accepted on: February 1, 2021
    Submitted on: December 17, 2019
    Keywords: Computer Science - Formal Languages and Automata Theory
    Fundings :
      Source : OpenAIRE Research Graph
    • Challenges for Logic, Transducers and Automata; Funder: French National Research Agency (ANR); Code: ANR-16-CE40-0007

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2005.02596
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.fsttcs.2020.55
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2005.02596
    • 2005.02596
    • 10.4230/lipics.fsttcs.2020.55
    • 10.48550/arxiv.2005.02596
    What You Must Remember When Transforming Datawords
    Praveen, M. ;


    Consultation statistics

    This page has been seen 281 times.
    This article's PDF has been downloaded 151 times.