论文标题
一种通用解决方案，用于与分散订单的应用程序结合的合成
A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders
论文作者
论文摘要
我们研究了使用无限数据域与环境相互作用的反应性系统的合成。指定和建模此类系统的流行形式主义是寄存器自动机和传感器。他们通过将寄存器添加到存储数据值并将传入的数据值与存储数据值进行比较来扩展有限状态自动机。一般来说，来自非确定或通用寄存器自动机的合成是不可确定的。但是，它的寄存器结合的变体（此外，还对所寻求的换能器中的寄存器数量绑定了，也可以对通用寄存器自动机进行确定，该寄存器可以比较数据的平等数据，即数据域$（n，=）$。本文以线性顺序将可定性边界扩展到自然数的域$（n，<）$。我们的解决方案是通用的：我们在数据域（常规近似性）上定义了足够的条件，以确定寄存器结合的合成性。该条件被$（n，<）$之类的自然数据域满足。它允许人们使用简单的语言理论论点，并避免技术游戏理论推理。此外，通过定义数据域之间可降低性的一般概念，我们显示了在域中的$（n^d，<^d）中合成的确定性，该数字的数字是配备了组件的部分顺序以及域$（σ^*，\ prec）的有限条件的$（σ^*，\ prec）。
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain $(N,=)$. This paper extends the decidability border to the domain $(N,<)$ of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. The condition is satisfied by natural data domains like $(N,<)$. It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain $(N^d,<^d)$ of tuples of numbers equipped with the component-wise partial order and in the domain $(Σ^*,\prec)$ of finite strings with the prefix relation.
