Safraless Decision Procedures

9 years 1 months ago
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...
Orna Kupferman, Moshe Y. Vardi
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where FOCS
Authors Orna Kupferman, Moshe Y. Vardi
Comments (0)