Knowledge Compilation for Quantification in Alternating Automata

TL;DR

This paper introduces a knowledge compilation method for quantification in alternating automata, enabling efficient verification tasks without costly complementation of nondeterministic automata.

Contribution

It proposes novel compilation techniques for alternating automata that simplify quantification, improving efficiency in verification processes like QPTL satisfiability checking.

Findings

BDD-based prototype shows practical effectiveness on benchmarks.

Compilation enables elimination of alternating quantifiers without automata complementation.

Approach improves efficiency in verification tasks involving infinite word automata.

Abstract

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.