Electronic Systems Design Seminar

 Orna Kupferman

Safraless decision procedures

Orna Kupferman
Hebrew University and UC Berkeley

Wednesday, July 30th, 2003, 2:30pm - 3:30pm
521 Cory Hall (Hogan Classroom)


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-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.

©2002-2018 U.C. Regents