Seminar by Aniello Murano on Reasoning About Strategies - Dec. 11, 2012 11:30-12:00 - Aula Magna

TITLE: Reasoning About Strategies

SPEAKER: Aniello Murano  Università degli Studi di Napoli Federico II.

WHEN & WHERE: December 11, 2012 11:30-12:00 - Aula Magna

ABSTRACT:  In open-system verification, a fundamental area of research is the study of modal logics for strategic reasoning. An important contribution in this field has been the development of Alternating-Time Temporal Logic, ATL* for short. Several decision problems have been investigated about ATL*; both its model-checking and satisfiability problems are decidable in 2EXPTIME. Despite its powerful expressiveness, ATL* suffers from the strong limitation that strategies are treated only implicitly through modalities that refer to games between competing coalitions. In this talk, we present Strategy Logic, denoted SL, as a general framework for explicit reasoning about strategies in multi-agent concurrent games. Specifically, strategies are used as first-order objects. The explicit treatment of strategies makes this logic very useful and more expressive than ATL*. The price that one has to pay for this extra expressiveness is the lack of important model-theoretic properties and an increased complexity of related decision problems. In particular, it holds that SL does not have the bounded-tree model property and the satisfiability problem is undecidable. Moreover, the model checking problem is nonelementary-complete. The negative complexity results on the decision problems of SL with respect ATL* has provided motivations for the investigation of fragments of SL, strictly subsuming ATL*, having a better complexity. Here we talk about Nested-Goal, Boolean-Goal, and One-Goal Strategy Logic, respectively denoted by SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special prenex normal form having nested temporal goals, Boolean combinations of goals, and a single goal at a time, respectively. As main results about these fragments, we show that the satisfiability and the model-checking problems for SL[1G] are 2EXPTIME-COMPLETE, thus not harder than the ones for ATL*. On the contrary, for SL[NG], the model checking problem is nonelementary and the satisfiability is undecidable.

This talk is mainly based on the papers

1) F. Mogavero, A. Murano, and M.Y. Vardi. Reasoning About Strategies. FSTTCS 2010

2) F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic. CONCUR 2012.