Preface

This volume contains the proceedings of the Second International Workshop on Strategic Reasoning 2014 (SR 2014), held in Grenoble (France), April 5-6, 2014.

The SR workshop aims to bring together researchers, possibly with different backgrounds, working on various aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view.

Strategic reasoning is one of the most active research area in multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modeling strategic ability. Theoretical results are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, efficient resource management for smart-city models, and automatic players capable of beating expert human adversary, just to cite a few. All these examples share the challenge of developing novel theories and tools for agent-based reasoning that takes into account the likely behavior of adversaries.

This year SR has hosted four invited talks:

• Simulation Games
  Thomas A. Henzinger (IST Austria)
• Two Themes in Modal Logic
  Wiebe van der Hoek (University of Liverpool)
• Model Checking Systems Against Epistemic Specifications
  Alessio R. Lomuscio (Imperial College London)
• What are "Good" Winning Strategies in Infinite Games?
  Wolfgang Thomas (RWTH Aachen)

Each submission to SR 2014 was evaluated by four reviewers for quality and relevance to the topics of the workshop. All submissions with positive scores were accepted, leading to 14 contributed talks at the workshop.

We would like to acknowledge the people and institutions, which contributed to the success of this edition of SR. We thank the organizers of the European Joint Conferences on Theory and Practice of Software (ETAPS 2014) for giving us the opportunity to host SR 2014. Many thanks go to all the Program Committee members and the additional reviewers for their excellent work, the fruitful discussions and the active participation during the reviewing process. We also thank Loredana Sorrentino for her work as member of the Organizing Committee. We would like to acknowledge the EasyChair organization for supporting all tasks related to the selection of contributions, and both EPTCS and arXiv for hosting the proceedings. We gratefully acknowledge the financial support to SR 2014 by ExCAPE - an NSF-funded Expeditions Project in Computer Augmented Program Engineering and by OR.C.HE.S.T.R.A. an Italian Ministry and EU research funded project on ORganization of Cultural HEritage for Smart Tourism and Real-time Accessibility. Finally, we acknowledge the patronage from the Department of Electrical Engineering and Information Technology of the Università degli Studi di Napoli Federico II.

Grenoble, April 2014
Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi

General Chair

Moshe Y. Vardi, Rice University, Houston, Texas, USA

Program Co-Chair

• Fabio Mogavero, Università degli Studi di Napoli Federico II, Napoli, Italy
• Aniello Murano, Università degli Studi di Napoli Federico II, Napoli, Italy

Program Committee

• Natasha Alechina, University of Nottingham, Nottingham, England, UK
• Thomas Ågotnes, University of Bergen, Bergen, Norway
• Nils Bulling, Clausthal University of Technology, Clausthal-Zellerfeld, Germany
• Krishnendu Chatterjee, IST Austria, Klosterneuburg, Austria
• Wojtek Jamroga, University of Luxembourg, Luxembourg City, Luxembourg
• François Laroussinie, Université Paris Diderot, Paris, France
• Christof Löding, RWTH Aachen, Aachen, Germany
• Emiliano Lorini, Université Paul Sabatier, Toulouse, France
• John-Jules C. Meyer, Utrecht University, Utrecht, Netherlands
• Eric Pacuit, University of Maryland, College Park, Maryland, USA
• Wojciech Penczek, Polish Academy of Sciences, Warsaw, Poland
• Sophie Pinchinat, University of Rennes, Rennes, France
• Jean-Francois Raskin, Université Libre de Bruxelles, Bruxelles, Belgium
• Francesca Rossi, Università di Padova, Padova, Italy
• Toby Walsh, University of New South Wales, Kensington, New South Wales, Australia
• Michael Wooldridge, University of Oxford, Oxford, England, UK

Organizing Committee

• Fabio Mogavero, Università degli Studi di Napoli Federico II, Napoli, Italy
• Aniello Murano, Università degli Studi di Napoli Federico II, Napoli, Italy
• Loredana Sorrentino, Università degli Studi di Napoli Federico II, Napoli, Italy

Additional Referees
Benjamin Aminof, Ioana Boureanu, Xi Chen, Rachid Echahed, Pietro Galliani, Paul Hunter, Rasmus Ibsen-Jensen, Michał Knapik, Tomas Kroupa, Matthijs Melissen, Artur Meski, Jan Otop, Truls Pedersen, Guillermo Perez, Henning Schnoor, Olivier Serre, Paolo Turrini.

Simulation Games

Milner's simulation relation is a fundamental concept to compare the behaviors of two discrete dynamical systems. While originally defined for safety properties of state transition graphs, its game-theoretic formulation allows a natural generalization to liveness and quantitative properties. The resulting games are implication games on product graphs, i.e., the derived (simulation) objective takes the form of a logical implication between primary (system) objectives. We summarize the hardness of such implication games for important classes of system objectives: in some cases the implication game is no harder to solve than the corresponding primary game; in other cases the implication game is open even though we know how to solve the primary game.

Two Themes in Modal Logic

Modal logics form the basis for knowledge representation languages in AI, enabling us to reason about time, knowledge, beliefs, desires and obligations of agents. In my talk, I will address two contemporary research themes in this field.
A good old fashioned line of research in modal logic is that of "correspondence theory" which establishes a direct link between first order properties on Kripke models (basically, graphs) and modal sentences. Standard results have a typical global flavour: in terms of beliefs for instance, reflexive models guarantee that the agent's beliefs are correct, and inclusion of the doxastic relation of agent a in that of agent b guarantees that agent a believes whatever b believes. However, such results cannot cater for cases where we want to express that such properties only hold locally, as in "agent a believes his beliefs are correct, but this is not the case", or in "agent a believes anything agent b believes, but this will cease to hold as soon as b reads the letter". I will present a logic that can deal with such local cases.
The second theme concerns the question how we compare different logics. Standard ways to compare L1 with L2 address their expressivity, or the computational complexity of reasoning problems one can perform in each. In many cases, two logics are comparable on both measures. Only recently the field of knowledge representation has started to address the issue of succinctness: how economically can one express properties in each logic? I give a working definition of what it means that L1 is exponentially more succinct than L2, and then I present a tool which can be used to prove succinctness results, the so-called Formula Size Games. Such games are played on two sets of models, and it establishes a relation between the number of moves needed to win the game, and the length of a formula that discriminates between the sets. I will present some examples of succinctness results.

Model Checking Systems Against Epistemic Specifications

Twenty years after the publication of the influential article "Model checking vs theorem proving: a manifesto" by Halpern and Vardi, the area of model checking systems against agent-based specifications is flourishing.
In this talk I will present some of the approaches I have developed with collaborators. I will begin by discussing BDD-based model checking for epistemic logic combined with ATL operators and then move to abstraction techniques including symmetry reduction. I will then highlight how, in our experience, bounded model checking can also successfully be used in this context, particularly in combination with BDDs, and how synthesis problems can be formulated and solved in an epistemic setting.
The talk will include examples in the context of security protocols and a brief demo of MCMAS, an open-source model checker implementing some of these techniques.
(This talk was meant to feature in the SR 2013 programme but could not be given due to ill health of the speaker).

What are "Good" Winning Strategies in Infinite Games?

Infinite games were invented in descriptive set theory, where the dominating question was determinacy - the mere existence of a winning strategy for one of the two players. In computer science the problem was put into an algorithmic setting: Can one decide who wins and can one effectively construct a winning strategy? In this talk we address quantitative refinements of the problem, reflecting a major current trend of research: How to construct winning strategies that are "good" or even "optimal" in some sense? The size of memory of finite-state machines executing winning strategies is a well-known criterion. Other criteria refer to the "efficient behavior" of strategies, as captured by the application of the solution of mean-payoff games. A third approach aims at novel formats of winning strategies, e.g. as "programs" (rather than state-machines). We survey old and recent work on these topics, spanning the literature from the beginnings (Büchi-Landweber 1969) to recent results obtained in the Aachen research group, among them the study of winning strategies as Boolean programs (Brütsch 2013) and the Turing machine based model of "strategy machine" (Gelderie 2014).
(Research supported by the project Cassting (Collective Adaptative Systems Synthesis With Non-Zero-Sum Games) funded as part of the FoCAS collaborative action by the European Commission under FP7.)

Doomsday Equilibria for Games on Graphs

Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.

In this work we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated. More precisely, given $n$ objectives $\varphi_1,\dots, \varphi_n$ and $n$ strategies $\Lambda_1,\dots,\Lambda_n$ for each of the $n$ players respectively, the strategy profile $\Lambda = (\Lambda_1,\dots,\Lambda_n)$ is a doomsday equilibrium if:

• all players satisfy their own objectives, that is $outcome(\Lambda) \in \varphi_i$ for all $1 \leq i \leq n$ (where $outcome(\Lambda)$ is the path obtained according to the strategies in the profile), and
• if any coalition of players deviates and violates even one of the players objective, then doomsday follows (every player objective is violated), that is for all $1 \leq i \leq n$, for all strategy profiles $\Lambda' = (\Lambda'_1,\dots,\Lambda'_n)$ such that $\Lambda'_i = \Lambda_i$, if $outcome(\Lambda') \not\in \varphi_i$, then $outcome(\Lambda') \not\in \varphi_j$ for all $1 \leq j \leq n$.

In the case of two-player non-zero-sum games they coincide with the secure equilibria ([1]) where objectives of both players are satisfied.

We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of $\omega$-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games. More specifically:

1. Perfect-information games: We show that deciding the existence of doomsday equilibria in multi-player perfect-information games is (i) PTIME-complete for reachability, Büchi, and coBüchi objectives; (ii) PSPACE-complete for safety objectives; and (iii) in PSPACE and both NP-hard and coNP-hard for parity objectives.
2. Imperfect-information games: We show that deciding the existence of doomsday equilibria in multi-player imperfect-information games is EXPTIME-complete for reachability, safety, Büchi, coBüchi, and parity objectives.

References

1. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski (2006): Games with secure equilibria. In: Theoretical Computer Science (TCS), vol. 365, pp. 67–82, doi:10.1016/j.tcs.2006.07.032.