Published: 10th July 2016|
|Preface Alessio Lomuscio and Moshe Y. Vardi|
|Invited Presentation: Quantitative Policies over Streaming Data Rajeev Alur|
|Invited Presentation: LTL and LDL on Finite Traces: Reasoning, Verification, and Synthesis Giuseppe De Giacomo|
|Extended Graded Modalities in Strategy Logic Benjamin Aminof, Vadim Malvone, Aniello Murano and Sasha Rubin||1|
|Representing Strategies Hein Duijf and Jan Broersen||15|
|Extending Finite Memory Determinacy to Multiplayer Games Stéphane Le Roux and Arno Pauly||27|
|Rational Verification in Iterated Electric Boolean Games Youssouf Oualhadj and Nicolas Troquard||41|
|LTL Reactive Synthesis under Assumptions (Abstract) Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Fabio Patrizi and Sasha Rubin||52|
|Pushdown ωB-Regular Games (Abstract) Krishnendu Chatterjee and Nathanaël Fijalkow||53|
|Strategic Disclosure of Opinions on a Social Network (Extended Abstract) Umberto Grandi, Emiliano Lorini and Laurent Perussel||54|
|Expressiveness and Nash Equilibrium in Iterated Boolean Games (Abstract) Julian Gutierrez, Paul Harrestein, Giuseppe Perelli and Michael Wooldridge||55|
|Imperfect Information in Reactive Modules Games (Abstract) Julian Gutierrez, Giuseppe Perelli and Michael Wooldridge||56|
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:
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".New York City, July 2016.
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.
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.
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) . 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 . 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.
 Hector Geffner and Blai Bonet, A Concise Introduction to Models and Methods for Automated Plan-
ning. Morgan & Claypool Publishers.
 A. Pnueli and R. Rosner, On the Synthesis of a Reactive Module, POPL'89, 1989.
 R. Bloem, R. Ehlers, S. Jacobs and R. Könighofer, How to Handle Assumptions in Synthesis, SYNT'14, 2014.