On control of systems modelled as deterministic Rabin automata (Q1902499)

Recent results on the control of infinite behaviour of finite automata are extended to allow Rabin acceptance conditions as modelling assumptions as well as specifications. The key result is a fixed point characterization of the automaton's controllability subset -- the set of states from which it can be controlled to the satisfaction of its associated specification. The fixed point characterization allows for a straightforward computation of the subset and for effective synthesis of controllers. The results have potential applications to supervisory control synthesis, the synthesis of reactive systems, and decision procedures for modal logics.