Strategy Games: A Renewed Framework

Game theory is a useful framework in multi-agent system verification. In this context, an important contribution is given by modal logics for strategic ability, such as ATL∗, SL, and the like, which allow to describe the interaction among players for the achievement of specific goals. However, most of the attempts carried out so far have focused on specific forms of games in which strategic-reasoning aspects are glued with agent temporal goals. In this paper, we propose a revisit of logics for strategic reasoning by following the general guidelines of game-theory, where the definition of solution concepts abstracts away the underlying cost-benefit analysis. Specifically, we introduce a game-theoretic framework consisting of three entities: the arena, shaping the rules of the game, the extension describing the property of interest of each possible play, and the schema, representing the agent roles and their interaction. In particular, to describe the latter, we use a variant of SL, by casting away its LTL temporal core. The new framework allows to gain in flexibility, modularity, and technical simplification, as well as, to grasp new features and better complexity results about logics previously studied. To give an evidence of this, by rephrasing SL in our framework, we improve known results about some of its fragments.