无限状态系统迹包含关系的抽象精炼
计算机科学中的逻辑
2015-10-22 v3 形式语言与自动机理论
摘要
数据自动机 (data automaton) 是一种配备有变量（计数器或寄存器）的有限自动机，这些变量取值于无限数据域。数据自动机的迹 (trace) 是自动机执行过程中字母表符号与计数器取值的交替序列。本文解决的问题是此类自动机识别的迹集（数据语言）之间的包含关系。由于该问题在一般情况下是不可判定的，我们给出了一种基于抽象精炼的半算法，证明了其可靠性和完备性，但不保证终止性。我们将该技术实现为一个原型工具，并在若干非平凡示例上展示了令人鼓舞的结果。
引用
@article{arxiv.1410.5056,
title = {Abstraction Refinement for Trace Inclusion of Infinite State Systems},
author = {Radu Iosif and Adam Rogalewicz and Tomas Vojnar},
journal= {arXiv preprint arXiv:1410.5056},
year = {2015}
}
备注
24 pages