Report
Teaser, summary, work performed and final results
Periodic Reporting for period 1 - LoGIcInMAS (Logics and Games for Imperfect Information in Multi-Agent Systems)
Teaser
This project’s aim was to develop formal methods based on logics and game theory to model, specify and analyse multi-agent systems (MAS). Such systems, in which autonomous agents interact and strategise to achieve private and/or common objectives, are central in many...
Summary
This project’s aim was to develop formal methods based on logics and game theory to model, specify and analyse multi-agent systems (MAS). Such systems, in which autonomous agents interact and strategise to achieve private and/or common objectives, are central in many endeavours of high potential societal impact, such as the development of smart cities or robotic rescue teams for nuclear accidents. Because of the criticality of many application areas, there has been over the recent years much effort put in bringing together the formal methods community and the MAS community in order to develop theoretical paradigms and practical tools to help design provably correct multi-agent systems. The logical approach has until now been particularly successful. The most recent and promising proposal was made by Chatterjee, Henzinger and Piterman, who in 2007 introduced Strategy Logic, a logic tailored to reason about rich game-theoretic notions in two-player turn-based games. In 2010 this logic was extended to (concurrent) multi-agent systems by Mogavero, Murano and Vardi, resulting in a very expressive logic (SL) that enjoys interesting properties and has been well studied, but only considers systems with perfect information.
However, in most real-life applications, agents only have imperfect information about their environment. Typically, rescue robots each have only a local, partial view of their environment. Their sensors may even get damaged during the mission, due to radiations for example. Considering imperfect information deeply impacts the strategizing process, and it also calls for a modelling of agents’ uncertainty.
This project had two main objectives: the first was to extend SL to account for imperfect information in strategies, and the second was to allow for reasoning about agents’ knowledge.
Work performed
\"Concerning the first objective, we defined an extension of Strategy Logic for imperfect information, called SLii, in which one can say what observation power a strategy should have. For this very expressive logic, it is undecidable to check whether a given system satisfies a given formula (a problem called model checking). But by taking inspiration from the theory of games with imperfect information and distributed synthesis we defined a fragment of SLii for which we proved the model checking to be decidable.
The main results obtained concerning this objective have been published in the following article, presented at the international conference LICS 2017:
Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin and Moshe Vardi, “Strategy Logic with Imperfect Informationâ€, LICS 2017
In addition, the methods developed to study SLii have allowed us to derive similar results for other logics of strategic reasoning. These results have been presented at the international conference AAMAS 2017:
Raphaël Berthon, Bastien Maubert and Aniello Murano, \"\"Decidability results for ATL* with imperfect information and perfect recall\"\", AAMAS 2017.
An extended version of this work with applications of the main result to the resolution of several strategic problems such as existence of Nash equilibria and rational synthesis, is about to be submitted to the international journal ACM Transactions on Computational Logic.
Concerning the second objective of the project, we first had to study a new phenomenon in temporal epistemic logics. In SLii, agents\' observations can change along time when agents change strategy. Such dynamic changes of observation power had never been studied in logics of knowledge and time, and we thus had to start by understanding what they mean for the semantics of knowledge. As a first step we thus left aside the strategic aspect and studied this phenomenon in the simpler setting of epistemic temporal logic. We introduced a new operator that indicates an agent changing observation power, we defined a natural semantics for this logic, we showed that this observation-change operator increases the expressivity of the logic, and we solved the model-checking problem.
The next step has been to integrate epistemic operators with observation change in our logic SLii. We studied an epistemic extension of SLii, and we solved its model-checking problem, once more for a fragment based on the concept of hierarchical information. This work is the object of two submissions to the international conference KR 2018.
In addition we also made progress in a direction that was not foreseen in the initial project’s objectives, even though it still is about extending Strategy Logic to make it more fit to study realistic problems of multi-agent systems.
One limitation of Strategy Logic is that it is purely qualitative. We extended Strategy Logic to include quantitative aspects in a way that can express bounds on “how quickly†and “how manyâ€. We devised a general technique, based on the study of automata with counters, that solves the model-checking problems for this logic. This work will be presented at the international conference CSL 2018.
Nathanaël Fijalkow, Bastien Maubert, Aniello Murano and Sasha Rubin, “Quantifying Bounds in Strategy Logicâ€, CSL 2018.
In addition, all these results will be presented at the international workshop Strategic Reasoning 2018, which will take place in Oxford in July as part of the Federated Logic Conference 2018 (FLOC).
\"
Final results
\"The main objectives of the project have been reached: we extended Strategy Logic to take into account strategies with imperfect information in an elegant way that also can handle agents changing observation power, and we then extended further this logic with epistemic operators to reason about agents’ knowledge. The main result of this project is an algorithm to decide whether a formula of the latter, very expressive logic, holds in a given system with hierarchical information. This notion of hierarchical information is important in strategic problems with imperfect information, as it is one of the two main particular cases that are known to bring back decidability of distributed synthesis.
This algorithm shows that besides distributed synthesis, many more strategic problems can be decided when information is hierarchical. For instance, it was not previously known that in this case the existence of Nash equilibria or subgame-perfect equilibria can be decided. Our algorithm solves these problems, as well as rational synthesis for instance. Furthermore, with the addition of epistemic operators it is possible to solve such problems for specifications or objectives that refer to agents’ knowledge: for instance, one can express that some agent’s objective is to make sure that some other agent never gets to know some piece of information that should remain secret.
The research carried out during this project has thus permitted to make significant progress concerning the verification of multi-agent systems, and provided an algorithm to solve a wide class of strategic problems with epistemic aspects on an important class of multi-agent systems.
Finally, we also made progress in another direction, enriching Strategy Logic with the possibility to express some quantitative properties of systems, such as \"\"how quickly will my goal be achieved\"\", or \"\"how many bad executions are there\"\", and we developed an algorithm to evaluate such properties in multi-agent systems. We now aim at combining these quantitative aspects with the imperfect information introduced during this project.
\"