Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)

TL;DR

This paper introduces a lazy decision procedure for WSkS logic that constructs and evaluates automata terms on the fly, enabling faster satisfiability checks compared to classical methods.

Contribution

It extends language terms to automata terms for WSkS, allowing on-the-fly state space construction and pruning, improving efficiency over classical procedures.

Findings

Prototype implementation outperforms classical methods on certain formulas.

Automata terms enable top-down evaluation and pruning.

Significant speed-ups observed in specific formula classes.

Abstract

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.