Abstract
Traditional synthesis algorithms return, given a specification over finite sets of input and output Boolean variables, a finitestate transducer all whose computations satisfy the specification. Many reallife systems have an infinite state space. In particular, behaviors of systems with a finite control yet variables that range over infinite domains, are specified by automata with infinite alphabets. A register automaton has a finite set of registers, and its transitions are based on a comparison of the letters in the input with these stored in its registers. Unfortunately, reasoning about register automata is complex. In particular, the synthesis problem for specifications given by register automata, where the goal is to generate correct register transducers, is undecidable.
We study the synthesis problem for systems with a bounded number of registers. Formally, the registerbounded realizability problem is to decide, given a specification register automaton A over infinite input and output alphabets and numbers k_s and k_e of registers, whether there is a system transducer T with at most k_s registers such that for all environment transducers T' with at most k_e registers, the computation TT', generated by the interaction of T with T', satisfies the specification A. The registerbounded synthesis problem is to construct such a transducer T, if exists. The bounded setting captures better reallife scenarios where bounds on the systems and/or its environment are known. In addition, the bounds are the key to new synthesis algorithms, and, as recently shown in [A. Khalimov et al., 2018], they lead to decidability. Our contributions include a stronger specification formalism (universal register parity automata), simpler algorithms, which enable a clean complexity analysis, a study of settings in which both the system and the environment are bounded, and a study of the theoretical aspects of the setting; in particular, the differences among a fixed, finite, and infinite number of registers, and the determinacy of the corresponding games.
BibTeX  Entry
@InProceedings{khalimov_et_al:LIPIcs:2019:10927,
author = {Ayrat Khalimov and Orna Kupferman},
title = {{RegisterBounded Synthesis}},
booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
pages = {25:125:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771214},
ISSN = {18688969},
year = {2019},
volume = {140},
editor = {Wan Fokkink and Rob van Glabbeek},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10927},
URN = {urn:nbn:de:0030drops109277},
doi = {10.4230/LIPIcs.CONCUR.2019.25},
annote = {Keywords: Synthesis, Register Automata, Register Transducers}
}
Keywords: 

Synthesis, Register Automata, Register Transducers 
Collection: 

30th International Conference on Concurrency Theory (CONCUR 2019) 
Issue Date: 

2019 
Date of publication: 

20.08.2019 