符号交替有限自动机的符号化判定过程
形式语言与自动机理论
2016-10-07 v1
摘要
我们引入符号交替有限自动机（s-AFA），作为一种表达力强、简洁且可判定的模型，用于描述任意字母表上的有限序列集合。s-AFA上的布尔运算具有线性复杂度，这与非交替符号自动机求交和求并的二次代价形成鲜明对比。由于这种简洁性，空性检查和等价性检查是PSpace难的。我们引入一种基于同余下互模拟的算法，用于检查两个s-AFA的等价性。该算法使我们能够利用SAT和SMT求解器的能力，高效搜索s-AFA的状态空间。我们在两个验证和安全应用上评估了我们的判定过程：1）检查有限迹上线性时序逻辑公式的可满足性；2）检查正则表达式布尔组合的等价性。我们的实验表明，我们的技术通常优于现有技术，并且在这两种应用中都能带来益处。
引用
@article{arxiv.1610.01722,
title = {A Symbolic Decision Procedure for Symbolic Alternating Finite Automata},
author = {Loris D'Antoni and Zachary Kincaid and Fang Wang},
journal= {arXiv preprint arXiv:1610.01722},
year = {2016}
}
备注
12 pages