Summarising Game Segments

One of the major challenges towards applying game-based methods to the analysis of complex interactive systems is scalability. Besides the state-explosion problem intrinsic to multi-component designs, keeping track of the control flow along game transitions determined by different players adds a layer of mental and computational complexity to system models. Abstraction is a generic approach to handling state-explosion by down-scaling models in such a way that essential properties are preserved. The approach has been very successful in the static analysis of sequential programs where the basic control-flow problem amounts to a question of reachability. For interactive programs, and in general for games, the control-flow problem corresponds to alternating reachability, an analysis that regards the power of an agent to reach a set of states, independently of the choice of the other agents. In this contribution, we propose a method for reducing the state space of game models that consists in replacing game segments with so-called called summaries in such a way that the security level of all players, as well as the structure of their security strategies