Hans van Ditmarsch (CNRS, LORIA)
"Awareness and knowledge"
ABSTRACT.
Modal logics of knowledge model uncertainty. Logics of awareness model incompleteness (as in vocabulary restriction) - a topic considered of great interest in economics. I have been working on these matters with Tim French (Perth), Fernando Velazquez (Sevilla), and Yi Wang (Bergen). We compare different epistemic notions in the presence of awareness of propositional variables: the logics of implicit knowledge (in which explicit knowledge is definable as implicit knowledge plus awareness), explicit knowledge, and speculative knowledge. Speculative knowledge goes back to the motivation in Levesque's 'A Logic of Implicit and Explicit Belief': one can speculate over variables of which one is unaware, e.g. if you are unaware of p, then p v ~p is still speculatively known by you. A cornerstone of this framework is the notion of awareness bisimulation - this is the proper notion of structural similarity on the structures enriched with awareness of propositional variables proposed by Fagin and Halpern in 'Belief, awareness, and limited reasoning'. A more 'standard' sort of bisimulation is also suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. The logic of speculative knowledge is equally expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than both. The logics have complete axiomatizations. Dynamics can also be added: any conceivable change of knowledge or awareness can be modelled in this setting. The dynamic versions of all three logics are, surprising, equally expressive.
Florence Dupin de Saint-Cyr - Bannay (Université Paul Sabatier, IRIT, Toulouse; joint work with Pierre Bisquert, Claudette Cayrol and Marie-Christine Lagasquie)
"Enforcement in Argumentation is a kind of Update"
ABSTRACT.
In the literature, enforcement consists in changing an argumentation system in order to force it to accept a given set of arguments. In this paper, we extend this notion by allowing incomplete information about the initial argumentation sys- tem. Generalized enforcement is an operation that maps a propositional formula describing a system and a propositional formula that describes a goal, to a new formula describing the possible resulting systems. This is done under some constraints about the allowed changes. We give a set of postulates restraining the class of enforcement operators and provide a representation theorem linking them to a family of proximity relations on argumentation systems.
Jérôme Lang (CNRS, LAMSADE, Paris; joint work with Bruno Zanuttini)
"From knowledge-based programming to planning"
ABSTRACT.
Knowledge-based programs (KBPs) are high-level protocols describing the course of action an agent should perform as a function of its knowledge. The use of KBPs for expressing action policies in AI planning has been surprisingly overlooked. Given that to each KBP corresponds an equivalent plan and vice versa, KBPs are typically more succinct than standard plans, but imply more on-line computation time. Here we make this argument formal, and prove that there exists an exponential succinctness gap between knowledge-based programs and standard plans. Then we address the complexity of plan existence. Some results trivially follow from results already known from the literature on planning under incomplete knowledge, but many were unknown so far.
Yongmei Liu (Sun Yat-sen University, Guangzhou; joint work with Quan Yu, Ximing Wen)
"Multi-agent Epistemic Explanatory Diagnosis via Reasoning about Actions"
ABSTRACT.
The task of explanatory diagnosis conjectures actions to explain observations. This is a common task in real life and an essential ability of intelligent agents. It becomes more complicated in multi-agent scenarios, since agents’ actions may be partially observable to other agents, and observations might involve agents’ knowledge about the world or other agents’ knowledge or even common knowledge of a group of agents. For example, we might want to explain the observation that p does not hold, but Ann believes p, or the observation that Ann, Bob, and Carl commonly believe p. In this paper, we formalize the multi-agent explanatory diagnosis task in the framework of dynamic epistemic logic, where Kripke models of actions are used to represent agents’ partial observability of actions. Since this task is undecidable in general, we identify important decidable fragments via techniques of reducing the potentially infinite search spaces to finite ones of epistemic states or action sequences.
Yongmei Liu (Sun Yat-sen University, Guangzhou; joint work with Naiqi Li, Yi Fan)
"Reasoning about State Constraints in the Situation Calculus"
ABSTRACT.
In dynamic systems, state constraints are formulas that hold in every reachable state. It has been shown that state constraints can be used to greatly reduce the planning search space. They are also useful in program verification. In this paper, we propose a sound but incomplete method for automatic verification and discovery of state constraints for a class of action theories that include many planning benchmarks. Our method is formulated in the situation calculus, theoretically based on Skolemization and Herbrand Theorem, and implemented with SAT solvers. Basically, we verify a state constraint by strengthening it in a novel and smart way so that it becomes a state invariant. We experimented with the blocks world, logistics and satellite domains, and the results showed that, almost all known state constraints can be verified in a reasonable amount of time, and meanwhile succinct and intuitive related state constraints are discovered.
Emiliano Lorini (CNRS, IRIT, Toulouse; joint work with Teddy Bouziat, Andreas Herzig, Dominique Longin and Laurent Perrussel)
"Reasoning about moral agents"
ABSTRACT.
The aim of this work is to provide a logical analysis of moral agency. Although this concept has been extensively studied in moral philosophy and in economics, it has been far less studied in the areas of logics of agents and multi-agent systems. We discuss different aspects of moral agency such as the distinction between desires and moral values and the concept of moral choice. All these concepts are formalized in a logic of actions and agents’ mental attitudes including knowledge, desires, moral values and preferences.
Faustine Maffre (Université Paul Sabatier, IRIT, Toulouse; joint work with Andreas Herzig and Emiliano Lorini)
"Strategies and commitments"
ABSTRACT.
ATL (Alternating-time Temporal Logic) is a modal logic which expresses strategies of agents in a multi-agents system: can a set of agents ensure a property by choosing specific actions? This logic provides a good basis but suffers from some problems: one of them is it does not express explicitly actions composing strategies. To fix this, we propose the logics ATLEA and ATLEP which adds actions to the language of ATL to explicit them in addition to strategies. We also add epistemic extension to ATLEA to reason about knowledge and uniform strategies.
Frederic Moisan (Université Paul Sabatier, IRIT, Toulouse; joint work with Emiliano Lorini)
"When the group matters: an analysis of team reasoning and social ties"
ABSTRACT.
In this paper, we investigate a central theory from the economics literature whose aim is to clarify how agents reason and are able to cooperate when acting as members of the same group: Bacharach's theory of team reasoning. After discussing the various limitations of this theory in modeling various types of social interactions, we introduce a new model of social ties which appears to provide a simpler and more intuitive approach to modeling collaborative actions in the context of complex strategic games where competing groups may coexist. We illustrate the advantage of this model by performing a detailed comparative analysis of both theories.
Laurent Perrussel (Université Toulouse 1 Capitole, IRIT, Toulouse; joint work with Jerusa Marchi, Jean-Marc Thévenin and Dongmo Zhang)
"Relevant Minimal Change in Belief Update"
ABSTRACT.
The notion of Relevance was introduced by Parikh in the belief revision field for handling minimal change. It prevents the loss of beliefs that do not have connections with the epistemic input. But, the problem of minimal change and relevance is still an open issue in belief update. In this paper, a new framework for handling minimal change and relevance in the context of belief update is introduced. This framework goes beyond relevance in Parikh's sense and enforces minimal change by first rewriting the Katzuno-Mendelzon postulates for belief update and second by introducing a new relevance postulate. We show that relevant minimal change can be characterized by setting agent's preferences on beliefs where preferences are indexed by subsets of models of the belief set. Each subset represents a prime implicant of the belief set and thus stresses the key propositional symbols for representing the belief set.
Pilar Pozos Parra (Universidad Juarez Autonoma de Tabasco; joint work with Kevin McAreavey and Weiru Liu)
"On the Merit of Selecting Different Belief Merging Operators"
ABSTRACT.
Belief merging operators combine multiple belief bases (a profile) into a collective one. When the conjunction of belief bases is consistent, all the operators agree on the result. However, if the conjunction of belief bases is inconsistent, the results vary between operators. There is no formal manner to measure the results and decide on which operator to select. So, we propose to evaluate the result of merging operators by using three ordering relations (fairness, satisfaction and strength) over operators for a given profile. Moreover, a relation of conformity over operators is introduced in order to classify how well the operator conforms to the de.nition of a merging operator. By using the four proposed relations we provide a comparison of some classical merging operators and evaluate the results for some specific pro.files.
François Schwarzentruber (Ecole Normale Supérieure Cachan, IRISA, Rennes; joint work with Guillaume Aucher)
"On the Complexity of Dynamic Epistemic Logic"
ABSTRACT.
In this talk, we present the language of DEL with event models and the union construction for programs. We are interested in decision procedures for automated reasoning. We prove that the model checking problem is PSPACE-complete and that the satisfiability problem is NEXPTIME-complete.
Ezgi Iraz Su (Université Paul Sabatier, IRIT, Toulouse; joint work with Luis Fariñas del Cerro and Andreas Herzig)
"Combining equilibrium logic and dynamic logic"
ABSTRACT.
We extend the language of here-and-there logic by two kinds of atomic programs allowing to minimally update the truth value of a propositional variable here or there, if possible. These atomic programs are combined by the usual dynamic logic program connectives. We investigate the mathematical properties of the resulting extension of equilibrium logic: we prove that the problem of logical consequence in equilibrium models is EXPTIME complete by relating equilibrium logic to dynamic logic of propositional assignments.