Reasoning About Strategies: On the Model-Checking Problem

Details Reasoning About Strategies: On the Model-Checking Problem Reasoning About Strategies: On the Model-Checking Problem

2011-12-29

arxiv.org/abs/1112.6275v2

Computer Science

Logic in Computer Science

Scientific paper

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, ATL\star, 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 ATL\star, 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 ATL\star.

Affiliated with

Also associated with

No associations

Rating

Reasoning About Strategies: On the Model-Checking Problem does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Reasoning About Strategies: On the Model-Checking Problem, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reasoning About Strategies: On the Model-Checking Problem will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-728418