License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2010.133
URN: urn:nbn:de:0030-drops-28597
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2859/
Go to the corresponding LIPIcs Volume Portal

Mogavero, Fabio ; Murano, Aniello ; Vardi, Moshe Y.

Reasoning About Strategies

pdf-format:
13.pdf (0.2 MB)

Abstract

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 SL-CHP, with the aim of getting a powerful framework for reasoning explicitly about strategies. SL-CHP is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turn-based
game structures where a non-elementary model-checking algorithm has been provided. While SL-CHP 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 SL-CHP, 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 SL-CHP. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic SL-CHP under the concurrent game semantics.

BibTeX - Entry

@InProceedings{mogavero_et_al:LIPIcs:2010:2859,
  author =	{Fabio Mogavero and Aniello Murano and Moshe Y. Vardi},
  title =	{{Reasoning About Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{133--144},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2859},
  URN =		{urn:nbn:de:0030-drops-28597},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.133},
  annote =	{Keywords: open systems, multi-agent systems, verification, strategy quantifier, alternating temporal logic, model-checking}
}

Keywords: open systems, multi-agent systems, verification, strategy quantifier, alternating temporal logic, model-checking
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI