Synthesis of Data Word Transducers
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5982/pdf |
| _version_ | 1797268584965079040 |
|---|---|
| author | Léo Exibard Emmanuel Filiot Pierre-Alain Reynier |
| author_facet | Léo Exibard Emmanuel Filiot Pierre-Alain Reynier |
| author_sort | Léo Exibard |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:49Z |
| format | Article |
| id | doaj.art-b8485681673e40079b2fc4ec4ecd713f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:49Z |
| publishDate | 2021-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b8485681673e40079b2fc4ec4ecd713f2024-03-08T10:33:16ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-03-01Volume 17, Issue 110.23638/LMCS-17(1:22)20215982Synthesis of Data Word TransducersLéo ExibardEmmanuel FiliotPierre-Alain ReynierIn 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.https://lmcs.episciences.org/5982/pdfcomputer science - formal languages and automata theory |
| spellingShingle | Léo Exibard Emmanuel Filiot Pierre-Alain Reynier Synthesis of Data Word Transducers Logical Methods in Computer Science computer science - formal languages and automata theory |
| title | Synthesis of Data Word Transducers |
| title_full | Synthesis of Data Word Transducers |
| title_fullStr | Synthesis of Data Word Transducers |
| title_full_unstemmed | Synthesis of Data Word Transducers |
| title_short | Synthesis of Data Word Transducers |
| title_sort | synthesis of data word transducers |
| topic | computer science - formal languages and automata theory |
| url | https://lmcs.episciences.org/5982/pdf |
| work_keys_str_mv | AT leoexibard synthesisofdatawordtransducers AT emmanuelfiliot synthesisofdatawordtransducers AT pierrealainreynier synthesisofdatawordtransducers |