Reasoning About Strategies

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SLCHP, with the aim of getting a powerful framework for reasoning explicitly about strategies. SLCHP is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turned-based game structures where a non-elementary model-checking algorithm has been provided. While SLCHP is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent systems. We prove that SL strictly includes SLCHP, while maintaining a decidable model-checking problem. Indeed, we show that it is 2EXPTIME-COMPLETE, thus not harder than that for ATL* and a remarkable improvement of the same problem for SLCHP. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic SLCHP under the concurrent game semantics.