Control of ω-automata, church’s problem, and the emptiness problem for tree ω-automata

Abstract

Church’s problem and the emptiness problem for Rabin automata on infinite trees, which represent basic paradigms for program synthesis and logical decision procedures, are formulated as a control problem for automata on infinite strings. The alphabet of an automaton is interpreted not as a set of input symbols giving rise to state transitions but rather as a set of output symbols generated during spontaneous state transitions; in addition, it is assumed that automata can be “controlled” through the imposition of certain allowable restrictions on the set of symbols that may be generated at a given instant. The problems in question are then recast as that of deciding membership in a deterministic Rabin automaton’s controllability subset - the set of states from which the automaton can be controlled to the satisfaction of its own acceptance condition. The new formulation leads to a direct, efficient and natural solution based on a fixpoint representation of the controllability subset. This approach combines advantages of earlier solutions and admits useful extensions incorporating liveness assumptions.