Title: Lazy Automata Techniques for WS1S,
Abstract: We present a new decision procedure for the logic WS1S. It originates from
the classical approach, which first builds an automaton accepting all models of
a formula and then tests whether its language is empty. The main novelty is to
test the emptiness on the fly, while constructing a symbolic, term-based
representation of the automaton, and prune the constructed state space from
parts irrelevant to the test. The pruning is done by a generalization of two
techniques used in antichain-based language inclusion and universality checking
of finite automata: subsumption and early termination. The richer structure of
the WS1S decision problem allows us, however, to elaborate on these techniques
in novel ways. Our experiments show that the proposed approach can in many
cases significantly outperform the classical decision procedure (implemented in
the MONA tool) as well as recently proposed alternatives.