Preface

This volume contains the proceedings of the Fourth International Workshop on Strategic Reasoning (SR 2016), held in New York City (USA), July 10, 2016.

Strategic reasoning is a key topic in the multi-agent systems research area. The literature in this field is extensive and includes a variety of logics used for reasoning about the strategic abilities of the agents in the system. Results stemming from this research have been used in a wide range of applications including robotic teams endowed with adaptive strategies, and automatic players capable of beating expert human adversaries. A common feature in all these domains is the requirement for sound theoretical foundations and tools accounting for the strategies that agents may adopt in the presence of adversaries. The SR international workshop series aims to bring together researchers working on different aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view.

Each submission to SR 2016 was evaluated by three reviewers for quality and relevance to the topics of the workshop. All submissions with positive reviews were accepted for presentation, resulting in 9 contributed talks to the workshop.

In addition, SR 2016 hosted two invited talks:

• G. De Giacomo (Sapienza University of Rome). LTL and LDL on Finite Traces: Reasoning, Verification, and Synthesis.
• R. Alur (University of Pennsylvania). Quantitative Policies over Streaming Data.

We would like to thank the Program Committee members for their constructive and timely reviews of the submitted papers and all authors and invited speakers for contributing their work to the workshop. The workshop was partially supported by NSF Expeditions in Computing project "ExCAPE: Expeditions in Computer Augmented Program Engineering".

Workshop Chairs

• Alessio Lomuscio, Imperial College London (Program Chair)
• Moshe Y. Vardi, Rice University (General Chair)

Program Committee

• Natasha Alechina, University of Nottingham
• Francesco Belardinelli, Imperial College London
• Patricia Bouyer-Decitre, LSV - CNRS and ENS Cachan
• Nils Bulling, Delft University of Technology
• Krishnendu Chatterjee, IST Austria
• Catalin Dima, University of Paris-Est-Creteil
• Giuseppe De Giacomo, Sapienza University of Rome
• Wiebe van der Hoek, University of Liverpool
• Julian Gutierrez, University of Oxford
• Orna Kupferman, Hebrew University of Jerusalem
• Wojtek Jamroga, Polish Academy of Sciences
• François Laroussinie, University Paris Diderot
• Christof Löding, RWTH Aachen
• Emiliano Lorini, University Paul Sabatier
• Jakub Michaliszyn, University of of Wroclaw
• Aniello Murano, University of Naples
• Wojciech Penczek, Polish Academy of Sciences
• Sophie Pinchinat, University of Rennes
• Nir Piterman, University of Leicester
• Jean-Francois Raskin, Free University of Brussels
• Francesca Rossi, University of Padua
• Sasha Rubin, University di Naples
• Toby Walsh, University of New South Wales
• Michael Wooldridge, University of Oxford

Quantitative Policies over Streaming Data

Decision making in cyber-physical systems often requires dynamic monitoring of a data stream to compute performance-related quantitative properties. We propose Quantitative Regular Expressions as a high-level declarative language for modular specifications of such quantitative policies. This language is rooted in the emerging theory of regular functions, and every policy described in this language can be compiled into a space-efficient streaming implementation. We describe a prototype system that is integrated within an SDN controller and show how it can be used to specify and enforce dynamic updates for traffic engineering as well as in response to security threats. We conclude by outlining the rich opportunities for both theoretical investigations and practical systems for real-time decision making in IoT applications.

This talk is based on recent and ongoing work with Penn researchers Dana Fisman, Zack Ives, Sanjeev Khanna, Boon Thau Loo, Kostas Mamouras, Mukund Raghothaman, and Yifei Yuan.

LTL and LDL on Finite Traces: Reasoning, Verification, and Synthesis

In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of processes modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption has emerged. We will look at two specific logics (i) LTLf, i.e., LTL interpreted over finite traces, which has the expressive power of FOL and star-free regular expression over finite stings; and (ii) LDLf, i.e., Linear-time Dynamic Logic on finite traces, which has the expressive power of MSO and full regular expression. We review the main results on satisfiability, logical implication and verification. Then we turn to synthesis and we consider in particular reactive synthesis both under full and partial observability. We also show that these forma of synthesis can be considered generalizations of typical forms of Planning in Artificial Intelligence. The main catch is that working with these logics can be based on manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis.

LTL Reactive Synthesis under Assumptions (Abstract)

This work contributes to the ongoing discussion about how to meaningfully formalize an answer to the question "What is synthesis?". As starting point, we observe that reasoning about action and planning in AI involves describing and formally representing the interaction between an agent and its environment, as well as assumptions on how the environment works (e.g., effects of actions) and assumptions on how the agent works (e.g., preconditions of actions) [1]. The idea is to find a plan for the agent that guarantees some goal while respecting the agent assumptions and taking advantage of the environment assumptions. Such settings can often be translated into instances of LTL Reactive Synthesis [2]. That is, environment assumptions, agent assumptions, and goals are expressed in LTL, and the planning problem corresponds to synthesizing a strategy for the agent in a two-player game.

The main motivation for this work is to understand, in the context of LTL reactive synthesis, when a given LTL formula can reasonably be said to be an assumption for a given player. We argue that not all LTL formulas can be used as assumptions, since it might not be clear which player (the agent or the environment) is responsible for it.

We formalize when one might call an LTL formula an assumption (for a given player). We justify our definition by noting that specifications of planning domains in most AI formalisms for reasoning about action and planning can be separated into formulas that meet our definition. We suggest a second, weaker definition of assumption for a given player and argue that it captures the intuitive meaning of being an assumption. We define LTL synthesis under assumptions, show that it generalizes plain LTL synthesis, and establish that its computational complexity is no harder than that of LTL synthesis.

References

Pushdown ωB-Regular Games (Abstract)

The main result of this work is to show that solving two-player pushdown games equipped with conditions defined by non-deterministic ωB automata is decidable. It is obtained in two steps: the first is a reduction to the case of deterministic automata, and the second a solution for this subcase using the theory of regular cost functions. To solve games with ω-regular conditions, the usual way is to construct a deterministic parity automaton recognising the condition and to compose the game with this automaton, yielding a parity game. However, in the context of ωB automata, non-deterministic automata are more expressive than deterministic ones, so this technique does not apply. Our solution uses the notion of history-deterministic automata developed in the theory of regular cost functions. The surprising aspect of this solution is that one can show that history-deterministic automata are actually weaker than non-deterministic ones; the crucial point to prove that our reduction is correct is a new determinacy result for pushdown games.

Strategic Disclosure of Opinions on a Social Network (Extended Abstract)

At the micro-level, social influence can be conceived as a process where an agent forms her opinion on the basis of the opinions expressed by other agents in the society. Social influence depends on trust since an agent can be influenced by another agent, so that her opinions are affected by the expressed opinions of the other, only if she trusts her. At the macro-level, social influence is the basic mechanism driving the diffusion of opinions in human societies: certain agents in the society influence other agents in the society towards a given view, and these agents, in turn, influence other agents to acquire the same view, and so on.

There exists formal models of opinion diffusion that combined methods and techniques from social network analysis with methods and techniques from belief merging and judgment aggregation. The two models aim at studying how opinions of agents on a given set of issues evolve over time due to the influence of other agents in the population. The basic component of these models is the trust network, as it is assumed that the opinions of a certain agent are affected only by the opinions of the agents that she trusts (i.e., the agents in the trust network that are directly linked to her). Specifically, the opinions of a certain agent at a given time are the result of aggregating the opinions of the trustworthy agents at the previous time.

In this work we build on these models to look at social influence from a strategic perspective. We do so by introducing a new class of games, called games of influence. Specifically, a game of influence is an infinite repeated game with incomplete information in which, at each stage of interaction, an agent can make her opinions visible (public) or invisible (private) to the other agents. Incompleteness of information is determined by the fact that an agent has uncertainty about the private opinions of the other agents, as she cannot see them. At each stage of the game, every agent is influenced by the public opinions of the agents she trusts (i.e., her neighbors in the trust network) and changes her opinions on the basis of the aggregation criterion she uses. Games of influence provide a simple abstraction to explore the effects of the trust network structure on the agents' behaviour. We consider solution concepts from game-theory such as Nash equilibrium, weak dominance and winning strategies. For instance, in the context of games of influence, we can study how the relative position of an agent in the trust network determines her influencing power, that is, her capacity to influence opinions of other agents, no matter what the others decide to do (which corresponds to the concept of uniform strategy). Moreover, in games of influence one can study how the structure of the trust network determines existence of Nash equilibria, depending on the form of the agents' goals. For instance, we will show that if the trust network is fully connected and every agent wants to reach a consensus about a certain proposition p, then there always exists a least one Nash equilibrium.

Note: An extended abstract on this topic has been presented at AAMAS-2016. This work was partially supported by Labex CIMI (ANR-11-LABX-0040-CIMI) project on "Social Choice on Networks", within the program ANR-11-IDEX-0002-02.

Expressiveness and Nash Equilibrium in Iterated Boolean Games (Abstract)

Temporal logics are probably the most successful and widely used class of formalisms for the specification and verification of computer systems. A natural question concerns their expressive power: what system properties is it possible to express within a particular temporal logic or temporal logic fragment? We introduce and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic properties of multi-agent systems. We focus on iterated Boolean games, in which each agent tries to satisfy a goal represented by a formula in a fragment of Linear Temporal Logic (LTL) by choosing in each of an infinite number of rounds a valuation for a set of Boolean variables over which it exercises exclusive control. Each player is assumed to act strategically in order to bring about computations satisfying their goal. The result of play is an infinite computation, that is, a model for LTL.

In this setting, we apply the standard game-theoretic concept of Nash equilibrium. The Nash equilibria of an iterated Boolean game induce a set of computations. The temporal property expressed thus may or may not be expressible in a particular LTL fragment. The novel notion of expressiveness that study for a range of known fragments L of LTL is then then as follows: what temporal properties are characterised by the Nash equilibria of games in which agent goals are expressed in L?

The following temporal variation on the Battle of the Sexes game illustrates and motivates this issue. Suppose that every weekend Gregory and Wolf go out to either the ballet or to a prize fight. Gregory wishes always to go out together, whereas Wolf wants to go to the ballet together with Gregory at least once but also wishes to see the prize fight on his own at least once. This defines an iterated Boolean game where Gregory controls variable p and Wolf variable q. By setting his variable to true, an agent goes to the ballet, and by setting it to false to the prize fight. Using the temporal operators F (``eventually'') and G (``always'') only, the preferences of Gregory and Wolf can then be represented by G(p↔q) and F(p∧q)∧(p∧¬q), respectively. We find that the run {p,q}, ∅,∅,∅... is induced by a Nash equilibrium of this game, but {p,q},{p,q}, ∅,∅,∅... is not. The runs that are sustained by a Nash equilibrium are precisely those in which always either {p,q} or ∅ is the case and {p,q} occurs only once. Yet, this property cannot be expressed in the (stutter-invariant) fragment of LTL with F and G as sole temporal operators. This raises the question which properties are characterised by the Nash equilibria of iterated Boolean games with the players' preferences formulated in this and other LTL-fragments.

Acknowledgments    This work was presented at KR 2016 and published in:

J. Gutierrez, P. Harrenstein, G. Perelli, and M. Wooldridge (2016): Expressiveness and Nash Equi- librium in Iterated Boolean Games. In: Proceedings of AAMAS 2016, pp. 707-715.

Imperfect Information in Reactive Modules Games (Abstract)

Reactive Modules is a high-level modelling language for concurrent and multi-agent systems, which is used in a number of practical model checking tools (e.g., MOCHA and Prism). Reactive Modules Games are a game-theoretic extension of Reactive Modules, in which agents in a system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. Reactive Modules Games with perfect information have been closely studied, and the complexity of game theoretic decision problems relating to such games have been comprehensively classified. However, to date, no work has considered the imperfect information case. In this paper we address this gap, investigating Reactive Modules Games in which agents have only partial visibility of their environment.

Our key results are as follows. We show that Reactive Modules Games with imperfect information are undecidable if three or more players are allowed. In contrast, if restricted to two players, the games are decidable and their solution (computing a Nash equilibrium if one exists) can be obtained in 2EXPTIME. For the latter decidability result, we use a conceptually simple decision procedure based on synthesis techniques for CTL* under imperfect information. We also explore a number of variants of the general imperfect-information framework. For instance, we study variants of these games with respect to the class of strategies under consideration, e.g., memoryless, myopic, polynomially bounded, and show that such games can be solved, respectively, in NEXPTIME, EXPSPACE, and PSPACE.

In Table 1 we report a summary of the complexity results.

Acknowledgments    This work was presented at KR 2016 and published in:

J. Gutierrez, G. Perelli, and M. Wooldridge (2016): Imperfect Information in Reactive Modules Games. In: Proceedings of the Fifteenth International Conference, KR 2016.