有界合成的通用解决方案及其在离散序中的应用
摘要：使用无限数据域与环境交互的反应系统合成的研究。一种用于指定和建模此类系统的流程自动机和转换器的流行形式主义。它们通过添加寄存器来扩展有限状态自动机，从而存储数据值并将传入的数据值与存储的数据值进行比较。从非确定性或通用寄存器自动机进行合成一般是不可判定的。然而，它的寄存器有界变体，其中还给出了在所寻求的转换器中寄存器数量的上界，已知对于可以比较相等性的通用寄存器自动机（即数据域（N，=））是可判定的。本文将可判定性边界扩展到具有线性顺序的自然数（N，<）的域。我们的解决方案是通用的：我们为数据域（正则可逼近性）定义了一个足够的条件，以便寄存器有界合成是可判定的。这个条件适用于自然数据域，如（N，<）。它使得我们可以使用简单的语言理论论证，并避免繁琐的博弈论推理。此外，通过定义数据域之间的通用可约性概念，我们展示了元组数（配备分量间部分顺序）领域（N^d，<^d）和有限字符串（带有前缀关系的（Sigma^*，prec））领域的合成的可判定性。
作者：L''eo Exibard, Emmanuel Filiot, Ayrat Khalimov
论文ID：2105.09978
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-05-23