Systems Design Seminar
Safraless decision procedures
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
nonempty. The standard approach translates formulas into alternating
automata, which are then translated, via Safra's determinization
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
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-Buchi tree automata and nondeterministic Buchi tree automata. Our translations are simpler than the standard approach, leading us to believe that they are less difficult to implement. We also show that our approach yields better complexity bounds.
Our approach is useful in many other problems where Safra's determinization is currently used. This includes realizability, synthesis, and determinization.
Joint work with Moshe Vardi.
Orna Kupferman is a Senior Lecturer in the School
of Computer Science
and Engineering at the Hebrew University in Israel. Her research
interests are in formal verification of reactive systems. Orna
received her B.Sc. from the Technion in 1991, and her PhD from the
Technion in 1995.