This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05)
Safraless Decision Procedures
Pittsburgh, Pennsylvania, USA
October 23-October 25
ISBN: 0-7695-2468-0
Orna Kupferman, Hebrew University
Moshe Y. Vardi, Rice University

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 B?uchi 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.

Citation:
Orna Kupferman, Moshe Y. Vardi, "Safraless Decision Procedures," focs, pp.531-542, 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.