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 work 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-B¨uchi tree auto...

• Type: Conference
• Year: 2005
• Where: FOCS
• Authors: Orna Kupferman, Moshe Y. Vardi
• Keywords: FOCS 2005, Nondeterministic Parity, Nondeterministic Parity Tree, Parity Tree Automata, Theoretical Computer Science