Published: 1st April 2014|
|Preface Fabio Mogavero, Aniello Murano and Moshe Y. Vardi|
|Invited Presentation: Simulation Games Thomas A. Henzinger|
|Invited Presentation: Two Themes in Modal Logic Wiebe van der Hoek|
|Invited Presentation: Model Checking Systems Against Epistemic Specifications Alessio R. Lomuscio|
|Invited Presentation: What are "Good" Winning Strategies in Infinite Games? Wolfgang Thomas|
|Expectations or Guarantees? I Want It All! A crossroad between games and MDPs Véronique Bruyère, Emmanuel Filiot, Mickael Randour and Jean-François Raskin||1|
|Games for the Strategic Influence of Expectations Lluís Godo and Enrico Marchioni||9|
|On Defendability of Security Properties Wojciech Jamroga, Matthijs Melissen and Henning Schnoor||17|
|Reasoning about Knowledge and Strategies: Epistemic Strategy Logic Francesco Belardinelli||27|
|An Epistemic Strategy Logic (Extended Abstract) Xiaowei Huang and Ron van der Meyden||35|
|Doomsday Equilibria for Games on Graphs Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot and Jean-François Raskin||43|
|Nash Equilibria in Symmetric Games with Partial Observation Patricia Bouyer, Nicolas Markey and Steen Vester||49|
|Refining and Delegating Strategic Ability in ATL Dimitar P. Guelev||57|
|A Resolution Prover for Coalition Logic Cláudia Nalon, Lan Zhang, Clare Dixon and Ullrich Hustadt||65|
|Efficient Decomposition of Bimatrix Games (Extended Abstract) Xiang Jiang and Arno Pauly||75|
|First Cycle Games Benjamin Aminof and Sasha Rubin||83|
|Games with recurring certainty Dietmar Berwanger and Anup Basil Mathew||91|
|Automata Techniques for Epistemic Protocol Synthesis Guillaume Aucher, Bastien Maubert and Sophie Pinchinat||97|
|Partial Preferences for Mediated Bargaining Piero A. Bonatti, Marco Faella and Luigi Sauro||105|
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:
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
Moshe Y. Vardi, Rice University, Houston, Texas, USA
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.
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.
Modal logics form the basis for knowledge representation languages in AI,
enabling us to reason about time, knowledge, beliefs, desires and obligations of
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.
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).
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
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"
(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.)
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,
In the case of two-player non-zero-sum games they coincide with the secure equilibria () 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: