CONTROL OF OMEGA-AUTOMATA UNDER STATE FAIRNESS ASSUMPTIONS

This article studies the deadlock-free control of finite automata subj ect to specifications in the form of Rabin acceptance conditions. Auto mata are assumed to satisfy a state fairness condition, whereby any tr ansition that is infinitely often enabled (by both the underlying dyna mics and the control mechanism) must eventually occur. The problem of computing the automaton's controllability subset - the set of states f rom which it can be controlled to satisfy its acceptance condition - i s solved through a fixpoint characterization of this state subset. The stare fairness condition simplifies the fixpoint characterization and allows the controllability subset to be computed in polynomial time. The problem represents a modified version of Church's problem and the emptiness problem for automata on infinite trees, and has potential ap plications to the verification and synthesis of reactive systems and t o supervisory control. (C) 1998 Elsevier Science B.V. All rights reser ved.