惰性WSkS决策过程中的自动机项（技术报告）
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)
摘要：
我们提出了一个懒惰的决策过程的逻辑WSkS。它建立了一个基于术语的符号表示的状态空间的树自动机（TA）构造的经典WSkS决策过程。经典的决策过程通过自底向上的遍历将符号表示转换为TA，然后测试其语言非空性，这对应于公式的可满足性。另一方面，我们从顶部开始评估表示，动态构建状态空间，并利用机会修剪掉与语言空虚测试无关的状态空间部分。为了做到这一点，我们需要将我们前面的逻辑线性片段（所谓的WS1S）过程中使用的语言项（表示语言派生）的概念扩展为自动机项。我们实现了我们的决策过程，并确定了我们的原型实现明显快于Mona工具中实现的经典过程的公式类。
英文摘要：
We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical WSkS decision procedure. The classical decision procedure transforms the symbolic representation into a TA via a bottom-up traversal and then tests its language non-emptiness, which corresponds to satisfiability of the formula. On the other hand, we start evaluating the representation from the top, construct the state space on the fly, and utilize opportunities to prune away parts of the state space irrelevant to the language emptiness test. In order to do so, we needed to extend the notion of language terms (denoting language derivatives) used in our previous procedure for the linear fragment of the logic (the so-called WS1S) into automata terms. We implemented our decision procedure and identified classes of formulae on which our prototype implementation is significantly faster than the classical procedure implemented in the Mona tool.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
