Omega-automata, games, and synthesis
Sriram C. Krishnan, Robert K. Brayton · 1998
In this dissertation we investigate the complexity of translation among deterministic $\omega$-automata (DOA), employ our new and improved translations among DOA to derive improved property synthesis algorithms, and consider games to model synthesis problems that arise in practice. $\omega$-automata are finite state automata that accept infinite strings. The acceptance condition can be one of many types: Buchi, Co-Buchi, Rabin, Streett, etc., each specified by a set of pairs of subsets of states. Restricting the number of pairs permitted in the acceptance condition induces an infinite hierarchy on the languages accepted by DOA. The minimum number of pairs required to accept a language by a DOA--the Rabin Index--is a function of the topological complexity of the language, and determines the structural complexity of any DOA accepting the language. Given a DOA, we address the problem of deciding its Rabin Index; we present a translation of a DOA into an equivalent minimum-pair DOA whose size is exponential in the Rabin Index of the language. We also prove lower bounds ta establish the optimality of our translation procedures. The synthesis of a Finite State Machine (FSM) that satisfies a property specified as a DOA can be viewed as a two-person Gale-Stewart game of perfect information (GSP game) played on the DOA, called the game automaton, between the FSM: and its adversarial environment (that supplies the FSM's input). We relate the complexity of synthesis to the complexity of the language describing the property--the game language; we employ our translations among DOA to derive a synthesis algorithm that decides the winner in a GSP game on a DOA in time that is exponential only in the Rabin Index of the game language (rather than the number of pairs of the game automaton). For instance, we can decide the winner of a GSP game played on a Rabin DOA with n states and h pairs in time $O((nh)\sp{3k})$, where k is Rabin Index of the game language; this algorithm is optimal. The size of the winner's winning strategy is also at most exponential in the Rabin Index of the game language. We investigate lower bounds for strategy size in relation to the size of the game automaton, and also examine the problem of synthesizing minimum-state strategies. We study variants of the GSP game on DOA: incomplete information and fair Gale-Stewart games on DOA, as well as GSP games requiring a strategy FSM with no initial state (uninitialized GSP game). These games enable the modeling of synthesis problems arising in practice. All these games are not determined, i.e., there may not be a winner with a deterministic winning strategy. While incomplete information and fair Gale-Stewart games on DOA may be decided by defining appropriate GSP games, this does not appear possible for the uninitialized GSP game. We have devised a synthesis algorithm for the uninitialized GSP game when the game language is a topologically closed set. This yields a synthesis procedure to utilize the maximum flexibility afforded by the safe-replaceability (46) criterion which permits a FSM with no initial state to be replaced by another uninitialized FSM such that the change is not detectable by any environment.