寄存器自动机与符号迹语言的 Myhill-Nerode 定理

Frits Vaandrager; Abhisek Midya

寄存器自动机与符号迹语言的 Myhill-Nerode 定理

形式语言与自动机理论 2021-04-01 v2 计算机科学中的逻辑

作者: Frits Vaandrager , Abhisek Midya

摘要

我们为寄存器自动机(扩展有限状态机)提出一种新的符号迹语义,其记录运行过程中出现的输入符号序列以及该运行所施加的对输入参数的约束。我们的主要结果是将经典 Myhill-Nerode 定理推广到这一符号设定。我们的推广需要使用三种关系来刻画寄存器自动机的附加结构。位置等价 $\equiv_l$ 刻画符号迹终止于同一位置,转移等价 $\equiv_t$ 刻画它们共享同一最终转移,而部分等价关系 $\equiv_r$ 刻画在符号迹 $w$ 和 $w'$ 之后符号值 $v$ 和 $v'$ 被存储于同一寄存器。若关系 $\equiv_l$ 、 $\equiv_t$ 和 $\equiv_r$ 存在并满足特定条件(特别是它们均具有有限指数),则定义符号语言为正则的。我们证明与寄存器自动机相关联的符号语言是正则的,并为每个正则符号语言构造一个接受该语言的寄存器自动机。我们的结果为灰盒学习算法提供了基础,其中对数据参数的约束可使用例如符号/混合执行或污点分析工具从代码中提取。我们认为转向灰盒设定对于克服最先进黑盒学习算法的可扩展性问题至关重要。

关键词

寄存器自动机符号迹语言 Myhill-Nerode 定理扩展有限状态机灰盒学习正则语言

引用

@article{arxiv.2007.03540,
  title  = {A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages},
  author = {Frits Vaandrager and Abhisek Midya},
  journal= {arXiv preprint arXiv:2007.03540},
  year   = {2021}
}

备注

This is the full version of a paper that appeared in the proceedings of ICTAC'20

寄存器自动机与符号迹语言的 Myhill-Nerode 定理

摘要

关键词

引用

备注

相关论文