论文标题
基于forq的语言包容性正式测试
FORQ-based Language Inclusion Formal Testing
论文作者
论文摘要
我们提出了一种新型算法，以决定（非确定）Büchi自动机之间的语言包含，这是一个PSPACE完全问题。我们的方法像以前一样，利用了Quasiorder的概念来修剪寻找反例，通过丢弃其他人为Quasiorder所包含的候选人。丢弃的候选人保证不会损害算法的完整性。我们作品的新颖性在于用于丢弃候选人的Quasiorder。 We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign.所得的实现称为叉车，比在各种基准上的最先进的缩放缩放得更好，包括程序验证的基准和Word Compinatorics证明的定理。
We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.
