The interaction between a system and its environment corresponds to a game in which the system and the environment generate a word over the alphabet of assignments to the input and output signals. The system player wins if the generated word satisfies a desired specification. A correct reactive system has to satisfy its specification in all environments, and thus corresponds to a winning strategy for the system player in the above game. This view is the key to the game-based approach for reactive synthesis. It reduces synthesis to the problem of generating winning strategies in two-player games whose winning conditions are on-going behaviors, which can be specified by automata on infinite words. The paper presents the game-based approach, focusing on ways to cope with the fact that the game cannot be played over nondeterministic automata.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Playing Games on Automata

  • Orna Kupferman

摘要

The interaction between a system and its environment corresponds to a game in which the system and the environment generate a word over the alphabet of assignments to the input and output signals. The system player wins if the generated word satisfies a desired specification. A correct reactive system has to satisfy its specification in all environments, and thus corresponds to a winning strategy for the system player in the above game. This view is the key to the game-based approach for reactive synthesis. It reduces synthesis to the problem of generating winning strategies in two-player games whose winning conditions are on-going behaviors, which can be specified by automata on infinite words. The paper presents the game-based approach, focusing on ways to cope with the fact that the game cannot be played over nondeterministic automata.