Game Models for Open Systems

Abstract

An open system is a system whose behavior is jointly determined by its internal structure, and by the input it receives from the environment. To solve control and verification problems, open systems have often been modeled as games between the system and the environment; we argue that the game view of open systems should be extended also to the definitions of system refinement and composition. We give a symmetrical interpretation to games between system and environment: the moves of the system represent the outputs that the system can generate (the output guarantees), and symmetrically, the moves of the environment represent the inputs that the system can accept (the input assumptions). We argue in favor of defining refinement of open systems in terms of alternating simulation, which is the relation between games that plays the same role of simulation between transition systems. Alternating simulation captures the principle that a component refines another if it has weaker input assumptions, and stronger output guarantees. Furthermore, we argue in favor of a notion of composition that accounts for the compatibility between input assumptions and output guarantees, and that enables the synthesis of new input guarantees for the composed system. These game-theoretical notions of refinement and compatibility are related to the type-theoretical notions of subtyping and type compatibility, and give rise to an expressive modeling framework for component-based design and verification.

This research was supported in part by the NSF CAREER award CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.