Transducer Synthesis from Universal Register Automata in (N
Ayrat Khalimov, Emmanuel Filiot, Léo Exibard · arXiv (Cornell University) · 2021
This paper concerns the problem of reactive synthesis of systems interacting with its environment via letters from an infinite data domain. Register automata and transducers are popular formalisms for specifying and modeling such systems. They extend finite-state automata by introducing registers that are used to store data and to test incoming data against the stored one. Unlike the standard automata, the expressive power of register automata depends on whether they are deterministic, non-deterministic, or universal. Among these, universal register automata suit synthesis best as they can specify request-grant properties and allow for succinct conjunction. Because the synthesis problem from universal register automata is undecidable, researchers studied a decidable variant, called register-bounded synthesis, where additionally a bound on the number of registers in a sought transducer is given. In those synthesis works, however, automata can only compare data for equality, which limits synthesis applications. In this paper, we extend register-bounded synthesis to domains with the natural order <. To this end, we prove a key Pumping Lemma for a finite abstraction of behaviour of register automata, which allows us to reduce synthesis to synthesis of register-free transducers. As a result, we show that register-bounded synthesis from universal register automata over domain (N, <) is decidable in 2ExpTime as in the equality-only case, giving the order for free.