基于FORQ的语言包含性形式化测试
摘要：一种用于决定（非确定性）布奇自动机之间语言包含关系的新算法：一种PSPACE完全问题。我们的方法与其他方法一样利用了一种准序的概念，通过丢弃被其他准序包含的候选项来剪枝搜索反例。被丢弃的候选项保证不会影响算法的完备性。我们的工作的创新之处在于用于丢弃候选项的准序。我们引入了FORQs（右准序的族群），它们是通过对Maler和Staiger在1993年提出的右等同族群的概念进行调整而得到的。我们定义了一种基于FORQ的包含算法，并证明了其正确性，并为称为结构FORQ的特定FORQ实例化。由此得到的实现称为FORKLIFT，在包括程序验证和对词组组合定理证明的各种基准测试中表现更好。
作者：Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi
论文ID：2207.13549
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-07-28