Safraless Decision Procedures
=============================

The automata-theoretic approach is one of the most fundamental
approaches to developing decision procedures in mathematical logics.
To decide whether a formula in a logic with the tree-model property is
satisfiable, one constructs an automaton that accepts all (or enough)
tree models of the formula and then checks that the language of this
automaton is nonempty. The standard approach translates formulas into
alternating parity tree automata, which are then translated, via
Safra's determinization construction, into nondeterministic parity
automata. This approach is not amenable to implementation because of
the difficulty of implementing Safra's construction and the
nonemptiness test for nondeterministic parity tree automata.

In this paper we offer an alternative to the standard
automata-theoretic approach. The crux of our approach is avoiding the
use of Safra's construction and of nondeterministic parity tree
automata.  Our approach goes instead via universal co-Buchi tree
automata and nondeterministic Buchi tree automata.  Our translations
are significantly simpler than the standard approach, less difficult
to implement, and have practical advantages like being amenable to
optimizations and a symbolic implementation.  We also show that our
approach yields better complexity bounds.