|
Published: 1st March 2013 DOI: 10.4204/EPTCS.112 ISSN: 2075-2180 |
This volume contains the proceedings of the First International Workshop on Strategic Reasoning 2013 (SR 2013), held in Rome (Italy), March 16-17, 2013.
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 reasoning. Theoretical results are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, 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 behavior of adversaries.
This year SR has hosted four invited talks:
The program committee also selected 13 papers among the 23 contributions submitted. Contributions were selected according to quality and relevance to the topics of 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 2013) for giving us the opportunity to host SR 2013. 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 Giuseppe Perelli and Loredana Sorrentino for their great work as members 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 2013 by ExCAPE - an NSF-funded Expeditions Project in Computer Augmented Program Engineering. Finally, we acknowledge the patronage from the Department of Electrical Engineering and Information Technology of the Università degli Studi di Napoli Federico II.
Rome, March 2013Program Co-Chair
Program Committee
Organizing Committee
Additional Referees
Benjamin Aminof, Massimo Benerecetti, Thomas Brihaye, Sjur Kristoffer
Dyrkolbotn, Marco Faella, Lukasz Kaiser, Prateek Karandikar, Martin Lange,
Erik Parmann, Madhusudan Parthasarathy, Soumya Paul, Truls Pedersen, Giuseppe
Perelli, Nir Piterman, Luigi Sauro, Olivier Serre, Nicolas Troquard, Yi Wang.
Turn-based Büchi games and maximal end-component decomposition are two classic graph theoretic problems that are core algorithmic problems in synthesis and verification of probabilistic systems. Moreover, many other problems on graph games reduce to them, and as an example we will first describe how analysis of reachability objectives in concurrent games reduces to Büchi games. We will present recent results that break the O(n*m) barrier for Büchi games, and show how the same techniques break the barrier for maximal end-component decomposition.
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.
We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, which are two classical quantitative objectives. While for single dimensional objectives all results for mean-payoff and total-payoff coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, then the problem can be solved in polynomial time, and (ii) the existence of a bounded window can be decided in NP and in coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is ExpTime-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.
In economics, an equilibrium is a steady-state situation, which obtains because no participant has any rational incentive to deviate from it. Equilibrium concepts are arguably the most important and widely used analytical weapons in the game theory arsenal. The concept of Nash equilibrium in particular has found a huge range of applications, in areas as diverse and seemingly unrelated as biology and moral philosophy. However, there remain fundamental problems associated with Nash equilibria and their application. First, there may be multiple Nash equilibria, in which case, how should we choose between them? Second, some equilibria may be undesirable, in which case, how can we avoid them? In this presentation, I will introduce work that we have done addressing these problems from a computational/AI perspective. Assuming no prior knowledge of game theory or economic solution concepts, I will discuss various ways in which we can try to engineer a game so that desirable equilibria result, or else engineer out undesirable equilibria. In particular, I will consider thee possible devices for the management of equilibria: taxation, communication, and law-making. While all of these devices are regularly used in human societies, in this work, we consider these as computational problems.