The Community for Technology Leaders
RSS Icon
Subscribe
Pittsburgh, Pennsylvania, USA
Oct. 23, 2005 to Oct. 25, 2005
ISBN: 0-7695-2468-0
pp: 531-542
Orna Kupferman , Hebrew University
Moshe Y. Vardi , Rice University
ABSTRACT
<p>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.</p> <p>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.</p>
INDEX TERMS
null
CITATION
Orna Kupferman, Moshe Y. Vardi, "Safraless Decision Procedures", FOCS, 2005, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science 2005, pp. 531-542, doi:10.1109/SFCS.2005.66
20 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool