Contact : Andreas Herzig (herzig@irit.fr) Frédéric Maris (maris@irit.fr)
| GDR IA |  |
Contact : Andreas Herzig (herzig@irit.fr) Frédéric Maris (maris@irit.fr)
| GDR IA | |
| Accueil — IRIT - Université Toulouse III, Toulouse | |
| Hall de l'IRIT |
| Ouverture des 8èmes journées MAFTEC | |
| IRIT, salle du conseil |
Frédéric Maris (IRIT, Université Toulouse III - Paul Sabatier, Toulouse)
Présentation du groupe de travail MAFTEC et du rapport d'activité.
| Exposés et discussion | |
| IRIT, salle du conseil |
François Schwarzentruber (IRISA, ENS Rennes)
Formula synthesis in propositional dynamic logic with shuffle.
Joint work with Sasha Rubin and Sophie PinchinatAbstract:We introduce the formula-synthesis problem for Propositional Dynamic Logic with Shuffle (PDLS). This problem, which generalises the model-checking problem againsts PDLS is the following: given a finite transition system and a regular term-grammar that generates (possibly infinitely many) PDLS formulas, find a formula generated by the grammar that is true in the structure (or return that there is none). We prove that the problem is undecidable in general, but that adding restrictions either on the input structure or on the input grammar yields decidability. In particular, we prove that (1) if the grammar only generates formulas in PDL (without shuffle), then the problem is EXPTIME-complete, and a further restriction to linear grammars is PSPACE-complete, and a further restriction to non-recursive grammars is NP-complete, and (2) if one restricts the input structure to have only simple paths then the problem is in 2-EXPTIME. This work is motivated by and opens up connections to other forms of synthesis from hierarchical descriptions, including HTN problems in Planning and Attack-tree Synthesis problems in Security.
Tiago de Lima (CRIL, Université d'Artois, Lens)
Checking agent intentions in games.
Joint work with Nathalie Chetcuti-Sperandio, Alix Goudyme and Sylvain LagrueAbstract: Rational agents’ decisions are driven by their intentions, in the sense that agents execute actions that most probably lead to situations where their intentions are achieved. Using that insight, we propose a method for ‘intention checking’: let a description of a game, a state and the action executed by the agent at that state be given, the method checks whether the agent acted with the intention to reach a situation where some proposition ‘p’ is true. We use a logic with epistemic and temporal operators to reason about games and extend it with an intention operator ‘IX’. Formulas of the form ‘IX(p)’ are defined to be true in the situations where the intention check method verifies that the agent acts with the intention to achieve ‘p’ in the next state of the game. We show that this operator satisfies the principles of Bratman’s Asymmetry Thesis, and we also compare it to other theories of intention.
| Pause déjeuner | |
| Cafétéria de l'IRIT |
| Exposés et sessions de travail | |
| IRIT, salle du conseil |
Elise Perrotin (CRIL, Lens)
Lightweight Epistemic Planning.Abstract: The aim of epistemic planning is to plan with agents who can reason not only about the world around them, but about what other agents know, know that they know, and so on. The most general way of incorporating this kind of knowledge into planning is to use Dynamic Epistemic Logic (DEL), however DEL planning is undecidable in general. In this talk I will present a lightweight epistemic planning framework based on the Epistemic Logic of Observation (EL-O). The main features of this framework are the restricted reasoning capabilities of the agents as well as the use of 'knowing whether', or 'seeing', operators rather than the standard 'knowing that' operators. These allow for simple translations to classical propositional calculus and classical planning, giving us a method for epistemic reasoning and planning which retains classical costs. I will finish by discussing a possible extension of the principles of EL-O to logics of knowledge and belief.
Emiliano Lorini (IRIT-CNRS, Toulouse)
The Power of Belief Bases: Epistemic Concepts and Application to Planning.Abstract: In this talk I will present our recent work on a novel semantics for multi-agent epistemic logic exploiting belief bases and a variety of epistemic concepts that can be naturally represented in this semantics. The latter include static concepts such as explicit and implicit belief, awareness, graded belief, distributed and common belief as well as dynamic concepts such as belief expansion, forgetting and revision. I will show how a rich variety of epistemic and cognitive planning problems involving different types of epistemic events and speech acts such as assertions, questions and learning actions of private and public nature can be formulated in the context of this semantics. Time permitting, I will show in which sense our framework generalizes existing lightweight approaches to epistemic planning based on the notion of observability and how it relates to standard dynamic epistemic logic (DEL).
Jorge Luis Fernandez Davila (IRIT, Université Toulouse III - Paul Sabatier, Toulouse)
A Simple Framework for Cognitive Planning.
Joint work with Dominique Longin, Emiliano Lorini and Frédéric MarisAbstract: We present a novel approach to cognitive planning, i.e., an agent’s planning aimed at changing the cognitive attitudes of another agent including her beliefs and intentions. We encode the cognitive planning problem in an epistemic logic with a semantics exploiting belief bases. We study a NP-fragment of the logic whose satisfiability problem is reduced to SAT. We provide complexity results for the cognitive planning problem. Moreover, we illustrate its potential for applications in human-machine interaction in which an artificial agent is expected to interact with a human agent through dialogue and to persuade the human to behave in a certain way. A Simple Framework for Cognitive Planning
Jorge Luis Fernandez Davila, Dominique Longin, Emiliano Lorini, Frédéric Maris
Atelier — Groupes de discussion
| Sessions de travail | |
| IRIT, salle du conseil |
Atelier — Groupes de discussion
| Accueil — IRIT - Université Toulouse III, Toulouse | |
| Hall de l'IRIT |
| Exposé et discussion | |
| IRIT, salle du conseil |
Thomas Ågotnes (University of Bergen, Norsk)
Somebody-knows and Other Imaginary Notions of Group Belief.Abstract: In the talk I will revisit standard notions of group knowledge and belief in epistemic logic such as common, distributed and general (everybody-believes) belief. The properties of these notions vary depending on the properties we assume of (individual) belief, but I will (provocatively) make the argument that there is no such thing as group belief except in very special cases. I will particularly focus on a notion of group knowledge that so far has received far less attention than those just mentioned: somebody-knows. While something is general knowledge if it is known by everyone, this notion holds if it is known by someone. Somebody-knows is thus weaker than general knowledge but stronger than distributed knowledge. I introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike the other mentioned group knowledge modalities, somebody-knows is not a normal modality; in particular it lacks the conjunctive closure property. I provide an equivalent neighbourhood semantics for the language with a single somebody-knows modality, together with a completeness result: the somebody-knows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom. The neighbourhood semantics and the completeness and complexity results also carry over to logics for so-called local reasoning (Fagin et al., 1995) with bounded ``frames of mind'', correcting an existing completeness result in the literature (Allen 2005). The talk is based on joint work with Yi N. Wang.
| Exposé et discussion | |
| IRIT, salle du conseil |
Hans van Ditmarsch (Open University of the Netherlands)
Everyone knows that everyone knows.Abstract: A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a telephone call wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition is that all agents are experts. Instead, we explore protocols wherein the termination condition is that all agents know that all agents are experts. We call such agents super experts. Additionally, we model that agents who are super experts do not make and do not answer calls. Such agents are called engaged agents. We also model that such gossip protocols are common knowledge among the agents. We investigate conditions under which protocols terminate, both in the synchronous case, where there is a global clock, and in the asynchronous case, where there is not. We show that protocols with engaged agents may terminate faster than protocols without engaged agents.
In recent progress on this topic we show that stronger termination conditions than that all agents are super experts are unsatisfiable. In other words, it is the best you can do if only secrets are exchanged. This is a sharp contrast with the work by Frédéric Maris wherein agents exchange messages containing knowledge about secrets, and wherein arbitrary higher-order epistemic goals can be reached. The latter comes closer to the well-known full-information protocols in distributed computing.Everyone Knows that Everyone Knows: Gossip Protocols for Super Experts
Hans van Ditmarsch, Malvin Gattinger, Rahim Ramezanian
Catalin Dima (LACL, Université Paris-Est Créteil)
Energy Sensitive Rational Synthesis
Joint work with Rodica Condurache, Youssouf Oualhadj and Nicolas TroquardTurn-based multi-agent games on graphs are games where the states are controlled by a single player who decides which edge to follow. Each player has a temporal objective that he tries to achieve, and one player is the designated ‘controller’, whose objective captures the desirable outcomes of the whole system. Cooperative rational synthesis is the problem of computing a Nash equilibrium (w.r.t. the individual temporal objectives) that satisfies the controller’s objective. In this presentation, we tackle this problem in the context where each action has a cost or a benefit on one shared common pool energy resource. The paper investigates the problem of synthesizing the controller such that there exists an individually rational behavior of all the agents that satisfies the controller’s objective and does not deplete the resource. We consider two types of agents: careless and careful. Careless agents only care for their temporal objective, while careful agents also pay attention not to deplete the system’s resource. We study the complexity of the problem of cooperative rational synthesis with parity or Büchi objectives, careful or careless agents, and costs encoded in binary or unary.
| Pause déjeuner | |
| Cafétéria de l'IRIT |
| Soutenance - HDR | |
| IRIT, salle du conseil, et en visioconférence Zoom |
Frédéric Maris (IRIT, Université Toulouse III - Paul Sabatier, Toulouse)
Automated Planning with Solvers: Temporal and Epistemic Aspects.Abstract: My research interests cover, in particular, planning and the complexity-theoretic and algorithmic aspects of reasoning. During the last years, I supervised students and made numerous contributions in this field and in particular for temporal and epistemic planning and the use of solvers for the resolution of such problems.
I have studied theoretical aspects of temporal planning (tractable classes and temporal relaxations, and classes of temporal languages and temporal cycles), and have built a temporal planner which has participated in the International Planning Competition. In recent work, we have shown that simple models of epistemic planning are PSPACE-complete, with many interesting epistemic planning problems being in NP or even P, even in the presence of temporal constraints. I have also introduced simple models for cognitive planning which is a generalization of epistemic planning. An orthogonal approach I have investigated to mitigate the high complexity of planning is compilation, which transfers the burden of solving computationally-hard problems to offline preprocessing. I also proposed promising QBF encodings for classical planning that we aim to improve and extend to other aspects. These promising first results indicate that it may be possible to re-use the large body of existing work on classical planning and its extensions.
During my HDR defence, I will give an overview of my contributions which is representative of my work belonging the following three axes:
- Automated Reasoning and SAT Planning
- Concurrent Planning with Temporal Constraints
- Lightweight Epistemic Logics and Epistemic Planning
| Accueil — Université Toulouse III, Toulouse | |
| Hall de l'IRIT |
| Exposés et sessions de travail | |
| IRIT, salle du conseil |
Exposés libres et démonstrations (proposés durant les journées).
Atelier — Groupes de discussion
| Exposés et sessions de travail |
Exposés libres et démonstrations (proposés durant les journées).
Atelier — Groupes de discussion
| Pause déjeuner | |
| Cafétéria de l'IRIT |
| Exposés et sessions de travail | |
| IRIT, salle du conseil |
Arnaud Lequen (IRIT, Université Toulouse III - Paul Sabatier, Toulouse)
Extraction of adaptable plans from a compiled planning problem.
Joint work with Martin Cooper and Hélène FargierAbstract: Compiling offline a classical planning problem into another language comes at a cost, but can allow efficient online replanning. In this work, we study the compilation of STRIPS problems into specific sets of d-DNNF or OBDDs. First, we present a complexity map that details which operations are tractable when a problem is compiled. Then, we propose a technique that extracts a propositional formula modelling an instance of a problem, out of the compiled form of a more general instance of the same domain. This formula can be used to obtain plans online, and allows some resilience to various kinds of unexpected events that can happen during the acting phase.
Aïdin Sumic (Laboratoire LGP, Ecole Nationale d’Ingenieurs de Tarbes)
Négociation de la flexibilité dans une approche coopérative pour une prise de décision optimale : le cas de la crise sanitaire.
Joint work with Thierry Vidal and Hedi KarrayRésumé : Face au besoin de coordination, dans un système décentralisé, pour répondre à des objectifs à la fois globaux et privés dans le domaine de la planification temporelle multi-agents, les agents sont amené à négocier leurs propres flexibilité tout en répondant à des critères d’optimisation. Ici, nous nous intéressons aux problèmes de planification dans un contexte de crise. Nous sommes donc confrontés à un problème d’optimisation multicritères tel que la flexibilité, l’anticipation, de calcul d’impacts et de formalisation d’indicateurs particulièrement complexes face au besoin à la nécessité de coordination. Notre contribution s’articule autour de l’utilisation du modèle STNU (accronyme de Simple Temporal Network with Uncertainty) tout en se basant sur la crise sanitaire du Covid19.
François Schwarzentruber (IRISA, ENS Rennes)
Planning for Connected Agents in a Partially Known Environment
Joint work with Arthur Queffelec and Ocan Sankur.Abstract: The Connected Multi-Agent Path Finding (CMAPF) problem asks for a plan to move a group of agents in a graph while respecting a connectivity constraint. We study a generalization of CMAPF in which the graph is not entirely known in advance, but is discovered by the agents during their mission. We present a framework introducing this notion and study the problem of searching for a strategy to reach a configuration in this setting. We prove the problem to be PSPACE-complete when requiring all agents to be connected at all times, and NEXPTIME-complete in the decentralized case, regardless of whether we consider a bound on the length of the execution.
Atelier — Groupes de discussion
| Table ronde - Prospective, et sessions de travail | |
| IRIT, salle du conseil |
Session de prospective
animée par Tiago de Lima, Frédéric Maris et François Schwarzentruber
Atelier — Groupes de discussion