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