The Community for Technology Leaders
2013 IEEE 54th Annual Symposium on Foundations of Computer Science (2005)
Pittsburgh, Pennsylvania, USA
Oct. 23, 2005 to Oct. 25, 2005
ISBN: 0-7695-2468-0
pp: 531-542
Moshe Y. Vardi , Rice University
Orna Kupferman , Hebrew University
<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>
Moshe Y. Vardi, Orna Kupferman, "Safraless Decision Procedures", 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, vol. 00, no. , pp. 531-542, 2005, doi:10.1109/SFCS.2005.66
79 ms
(Ver 3.3 (11022016))