We present a knowledge compilation approach for existential and universal quantification in alternating automata. Knowledge compilation transforms formulas into normal forms with special properties that enable efficient answering of questions of interest. For Boolean formulas, several normal forms that have proven effective for existential/universal quantification, and even for functional synthesis, have been studied in the literature. For infinite word automata, quantification is a fundamental operation in verification tasks such as QPTL satisfiability checking and HyperLTL model checking. Existing algorithms rely on nondeterministic infinite word automata, where existential projection can be efficiently performed state-wise, but universal projection requires complementation. Complementing nondeterministic infinite word automata, however, is expensive in practice, making existing algorithms infeasible for automata in practice. Towards addressing this problem, we propose novel knowledge compilation techniques for existential and universal quantification on alternating safety automata. Our approach compiles alternating automata into normal forms where projection can be applied uniformly and efficiently to each state's transition function. Using the compilations for each type of quantification, we can effectively eliminate a sequence of alternating quantifiers in formulas without complementation. Our BDD-based prototype demonstrates the practical effectiveness of our algorithms on a suite of QPTL satisfiability benchmarks.

翻译：我们提出了一种面向交替自动机中存在量词和全称量词的知识编译方法。知识编译将公式转化为具有特殊性质的规范形式，从而能够高效回答特定查询问题。对于布尔公式，已有文献研究了多种在存在/全称量化及功能综合场景下被证明有效的规范形式。在无限词自动机中，量化是QPTL可满足性检测和HyperLTL模型检验等验证任务的基础操作。现有算法依赖非确定性无限词自动机，其中存在投影可按状态高效执行，但全称投影需要补集操作。然而，非确定性无限词自动机的补集操作在实际应用中代价高昂，导致现有算法难以处理实际自动机。针对这一问题，我们提出了面向交替安全自动机存在量词和全称量词的新型知识编译技术。该方法将交替自动机编译为规范形式，使得投影操作能够统一且高效地应用于每个状态的转移函数。通过针对每种量化类型进行编译，我们可以在无需补集操作的情况下有效消解公式中的交替量词序列。基于BDD的原型系统在QPTL可满足性基准测试集上的实验验证了我们算法的实际有效性。