|
|
Safraless decision procedures
Orna Kupferman
Hebrew University and UC Berkeley
Wednesday, July
30th,
2003, 2:30pm - 3:30pm
521 Cory Hall (Hogan Classroom)
|
Abstract
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.
Speaker
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.
|
