Reasoning about strategies: on the model-checking problem

DOI10.1145/2631917MaRDI QIDQ2946746zbMATH OpenOpenAlexFDO

Authors Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1112.6275

behavioral strategies model checking strategy logic

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27) Applications of game theory (91A80)

Abstract: In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system 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, ATLstar, and the like. Recently, 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. CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, 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 games. We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL. Moreover, we prove that such a problem for SL is NonElementarySpace-hard. This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATLstar, with the hope of obtaining an elementary model-checking problem. Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals and, a single goal at a time. About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus not harder than the one for ATLstar.

Recommendations

Cites work

Cited in

(87)

Describes a project that uses

Uses Software

This page was built for publication: Reasoning about strategies: on the model-checking problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946746)