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 open 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. In particular, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies. It is obtained by using first-order quantification 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 CHP-SL 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. In particular, we show that SL strictly includes CHP-SL, 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 CHP-SL. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic CHP-SL under the concurrent game semantics.