GAMES I/O AUTOMATA PLAY

We introduce a game approach for specifying reactive systems. In particular, we define a simple two-player game between System and Environment, and consider the outcomes of such a game as a specification of a reactive system. We introduce six classes of game languages. We then show that the class of languages generated by I/O automata equals one of our game classes. An immediate corollary to the proof is that the fairness condition of I/O\0 automata, which is defined as an extrinsic property by Lynch and Tuttle, can be incorporated as an intrinsic part of the automata. We also show closure properties of the six game classes. For example, we show that the class of languages defined by I/O automata is closed under union and hiding but not under intersection or complementation. The closure results are obtained by reasoning directly about games, thus demonstrating the advantage of the game-based approach.