We extend the languages of Coalition Logic (CL) and Alternating-time Temporal Logic (ATL) with new modalities for welfare-affecting capabilities, capturing the benefit and harm that a coalition can bring to another coalition through its strategic choices. These languages are interpreted over concurrent games enriched with agents’ preferences. On the conceptual side, we use these languages to formalize the notions of potential benefactor and danger. A potential benefactor corresponds to a coalition having the capability to confer a benefit on another coalition. Danger corresponds to a coalition having the capability to inflict harm on another coalition. On the technical side, we present several results concerning their axiomatization, their relationships with standard CL and ATL, and their computational complexity.

International audience

We present a novel rule-based semantics for causal reasoning as well as a number of modal languages interpreted over it. They enable us to represent some fundamental concepts in the theory of causality including causal necessity, causal necessity post-intervention and causal counterfactuals. We provide complexity results for the satisfiability checking and model checking problems for these modal languages. Moreover, we study the relationship between our rule-based semantics and the structural equation modeling (SEM) approach to causal reasoning. Finally, we use our semantics to elucidate the relationship between causal counterfactuals and belief change.

We introduce a novel language for reasoning about agents' cognitive attitudes of both epistemic and motivational type. We interpret it by means of a computationally grounded semantics using belief bases. Our language includes five types of modal operators for implicit belief, complete attraction, complete repulsion, realistic attraction and realistic repulsion. We give an axiomatization and show that our operators are not mutually expressible and that they can be combined to represent a large variety of psychological concepts including ambivalence, indifference, being motivated, being demotivated and preference. We present a dynamic extension of the language that supports reasoning about the effects of belief change operations. Finally, we provide a succinct formulation of model checking for our languages and a PSPACE model checking algorithm relying on a reduction into TQBF. We present some experimental results for the implemented algorithm on computation time in a concrete example.

Causation plays a central role in the attribution of responsibility, especially in the legal domain, where complex causal scenarios frequently arise. Traditionally, legal reasoners have relied on the idea that a cause must be a necessary condition of its effect, which falls short in scenarios involving overdetermination, preemption, or omission, thereby failing to adequately identify causes-in-fact. In this paper, we present a novel analysis of selected legal cases, each exemplifying common causal dilemmas discussed in causal literature. We employ three different notions of cause in our analysis: abductive explanation (AXp), the NESS test (Necessary Element of a Sufficient Set) and actual cause. We express the three notions and some of their variants in a modal language for causal reasoning that we interpret on a rule-based semantics. We provide a model checking algorithm for our modal language relying on a reduction into TQBF as well as an implementation of the legal cases in our causal model checker to automatically verify “what is the cause of what” and what types of causes apply in each legal case. Our interdisciplinary approach highlights the usefulness of logic-based methods for legal analysis, offering a fully transparent model-checking toolbox that could potentially support legal reasoners in disentangling complex factual scenarios.

We present a computationally grounded semantics for counterfactual conditionals in which i) the state in a model is decomposed into two elements: a propositional valuation and a causal base in propositional form that represents the causal information available at the state; and ii) the comparative similarity relation between states is computed from the states' two components. We show that, by means of our semantics, we can elegantly formalize the notion of actual cause without recurring to the primitive notion of intervention. Furthermore, we provide a succinct formulation of the model checking problem for a language of counterfactual conditionals in our semantics. We show that this problem is PSPACE-complete and provide a reduction of it into QBF that can be used for automatic verification of causal properties.

Responsibility is one of the key notions in machine ethics and in the area of autonomous systems. It is a multi-faceted notion involving counterfactual reasoning about actions and strategies. In this paper, we study different variants of responsibility for LTLf outcomes based on strategic reasoning. We show a connection with notions in reactive synthesis, including the synthesis of winning, dominant, and best-effort strategies. This connection provides a strong computational grounding of responsibility, allowing us to characterize the worst-case computa- tional complexity and devise sound, complete, and optimal algorithms for anticipating and attributing responsibility.

Epistemic logic and the theory of argumentation have only very recently started to interact, despite the central role that the epistemic view of argument plays in contemporary epistemology. In this paper, we present a novel epistemic language for reasoning about three types of beliefs of agents: explicit belief, plain implicit belief, and focused implicit belief. We use it to represent the concept of deductive argument and to elucidate its connection with the concept of belief. Our language is interpreted through a formal semantics that relies on belief bases. This semantics allows us to naturally represent the reasons an agent has for believing something, which we show to be closely related to the notion of argument. We provide results on expressiveness, axiomatization and decidability for the language.

Analogical proportions are statements of the form “α is to β as γ is to δ”, noted α:β::γ:δ, and can be understood as “α differs from β as γ differs from δ” and conversely “β differs from α as δ differs from γ”. In this paper, α, β, γ, δ are supposed to be propositional logic formulas, which are appropriate for representing concepts. There exists one approach, developed over the last 15 years, where “α differs from β” is understood in terms of the negation of the material implication α → β. The paper investigates another view where “α differs from β” is interpreted in terms of transformations where some variables become false, some variables become true, and some variables become irrelevant. Both approaches satisfy the three basic postulates of analogical proportions (reflexivity, symmetry, and stability under central permutation), as well as other interesting properties such as transitivity and unicity of δ such that α:β::γ:δ. However, the two approaches depart from each other since they do not validate the same analogical proportions. In particular, when p,q,r are atoms the proportion p:(p∧r)::q:(q∧r) holds in the new approach, while it fails to do so for the other. The new approach exhibits also a good behaviour with respect to integrity constraints. It is advocated that this makes it appropriate for handling analogy between concepts, while the other approach has proved to be fruitful for Boolean features-based representations. The paper provides a thorough analysis of the differences between the two approaches.

Responsibility anticipation is the process of determining if the actions of an individual agent may cause it to be responsible for a particular outcome. This can be used in a multi-agent planning setting to allow agents to anticipate responsibility in the plans they consider. The planning setting in this paper includes partial information regarding the initial state and considers formulas in linear temporal logic as positive or negative outcomes to be attained or avoided. We firstly define attribution for notions of active, passive and contributive responsibility, and consider their agentive variants. We then use these to define the notion of responsibility anticipation. We prove that our notions of anticipated responsibility can be used to coordinate agents in a planning setting and give complexity results for our model, discussing equivalence with classical planning. We also present an outline for solving some of our attribution and anticipation problems using PDDL solvers.

A moral planning agent (MPA) seeks to compare two plans or compute an optimal plan in an interactive setting with other agents, where relative ideality and optimality of plans are defined with respect to a prioritized value base. We model MPAs whose values are expressed by formulas of linear temporal logic (LTL) and define comparison for both joint plans and individual plans. We introduce different evaluation criteria for individual plans including an optimistic (risk-seeking) criterion, a pessimistic (risk-averse) one, and two criteria based on the use of anticipated responsibility. We provide complexity results for a variety of MPA problems.

We present a novel rule-based semantics for causal reasoning as well as a number of modal languages interpreted over it. They enable us to represent some fundamental concepts in the theory of causality including causal necessity and possibility, interventionist conditionals and Lewisian conditionals. We provide complexity results for the satisfiability checking and model checking problem for these modal languages. Moreover, we study the relationship between our rule-based semantics and the structural equation modeling (SEM) approach to causal reasoning, as well as between our rule-based semantics for causal conditionals and the standard semantics for belief base change.

This article continues the research initiated in [1,2], which established a connection between Boolean classifiers and legal case-based reasoning. We relax the assumption that case bases are such that all situations have been decided in favour of the defendant or the plaintiff and we introduce an inductive strategy for assigning plausible outcomes to undecided cases. Using counterfactual reasoning, we propose a method to determine whether, at each step of the induction, a feature is a factor, i.e., it consistently favours a single outcome, or is irrelevant, i.e., it is does not favour any outcome, or is ambiguous, i.e., it favours opposite outcomes.

Conditional logics are usually interpreted in terms of closest world and minimal change. It relies on a measure of distance between worlds which is defined abstractly, i.e. as an element of the model. The typical example of a concrete measure in literature is the Hamming distance. We show that given countably infinite atomic propositions in the language, Hamming distance is not merely an example, but grounded for two arguably most important conditional logics, Lewis' VC and VCU. That means, a formula is satisfied in a VC (resp. VCU) model, if and only if it is satisfied in a VC (resp. VCU) model whose distance between worlds is Hammingian.

Abstract Recent years have witnessed a renewed interest in the explanation of classifier systems in the field of explainable AI (XAI). The standard approach is based on propositional logic. We present a modal language which supports reasoning about binary input classifiers and their properties. We study a family of classifier models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. Moreover, we show that the satisfiability checking problem for our modal language is NEXPTIME-complete in the infinite-variable case, while it becomes polynomial in the finite-variable case. We moreover identify an interesting NP fragment of our language in the infinite-variable case. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations and biases. Finally, we present two extensions of our language: a dynamic extension by the notion of assignment enabling classifier change and an epistemic extension in which the classifier’s uncertainty about the actual input can be represented.

Abstract We introduce a multi-agent logic of explicit, implicit belief and awareness with a semantics using belief bases. The novelty of our approach is that an agent’s awareness is not a primitive but is directly computed from the agent’s belief base. We prove soundness and completeness of the logic relative to the belief base semantics. Furthermore, we provide a polynomial embedding of the logic of propositional awareness into it and a polynomial embedding of our logic into the logic of general awareness. Thanks to the latter embedding, we show that the satisfiability checking problem for our logic is PSPACE complete. Finally, we extend it by the notions of public announcement and private belief expansion.

(short version)

We introduce a simple model of agency that is based on the concepts of control and attempt. Both relate agents and propositional variables. Moreover, they can be nested: an agent i may control whether another agent j controls a propositional variable p; i may control whether j attempts to change p; i may attempt to change whether j controls p; i may attempt to change whether j attempts to change p; and so on. In this framework we define several modal operators of time and agency: the LTL operators on the one hand, and the Chellas and the deliberative stit operator on the other. While in the standard stit framework the model checking problem is unfeasible because its models are infinite, in our framework models are represented in a finite and compact way: they are grounded on the primitive concepts of control and attempt. This makes model checking practically feasible. We prove its PSPACE-completeness and we show how the concept of social influence can be captured.

This paper brings together factor-based models of case-based reasoning (CBR) and the logical specification of classifiers. Horty [8] has developed the factor-based models of precedent into a theory of precedential constraint. In this paper we combine binary-input classifier logic (BCL) to classifiers and their explanations given by Liu & Lorini [13, 14] with Horty’s account of factor-based CBR, since both a classifier and CBR map sets of features to decisions or classifications. We reformulate case bases in the language of BCL, and give several representation results. Furthermore, we show how notions of CBR can be analyzed by notions of classifier explanation.

Abstract We present a formal semantics for deontic logic based on the concept of ceteris paribus preferences. We introduce notions of unconditional obligation and permission as well as conditional obligation and permission that are interpreted relative to this semantics. We show that these notions satisfy some intuitive properties and, at the same time, do not encounter some problems and paradoxes that have been extensively discussed in the deontic logic literature. We prove that the satisfiability problem for our logic is in NP. Finally, we show that the fragment of our logic in which the content of a deontic operator is a literal has an equivalent representation based on conditional preference networks (CP-nets).

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.

We present a generalization of belief base revision to the multi-agent case. In our approach agents have belief bases containing both propositional beliefs and higher-order beliefs about their own beliefs and other agents’ beliefs. Moreover, their belief bases are split in two parts: the mutable part, whose elements may change under belief revision, and the core part, whose elements do not change. We study a belief revision operator inspired by the notion of screened revision. We provide complexity results of model checking for our approach as well as an optimal model checking algorithm. Moreover, we study complexity of epistemic planning formulated in the context of our framework.

We present a logical analysis of influence and control over the actions of others, and address consequential causal and normative responsibilities. We first account for the way in which influence can be exercised over the behaviour of autonomous agents. On this basis we determine the conditions under which influence leads to control on the implementation of positive and negative values. We finally define notions of causal and normative responsibility for the action of others. Our logical framework is based on STIT logic and is complemented with a series of examples illustrating the application. Our analysis applies to interactions between humans as well as to those involving autonomous artificial agents.

Abstract In this paper, we present two models for reasoning about strategic actions in opinion diffusion. In both models, the agents are endowed with goals expressed compactly in a suitably defined language of linear temporal logic and are connected in an influence network which defines the underlying opinion diffusion process. The agents can act by exerting their influence or retain from it: in one case, we assume an initial state of incomplete information about the agents’ opinions, while in the other, we assume that the agents have complete information. We investigate the interplay between simple network structures (e.g. certain acyclic graphs) and the existence of game-theoretic solution concepts for the unanimity aggregator. We also give bounds for the computational complexity of strategic reasoning in both our models on arbitrary networks.

Abstarct We present a general logical framework for reasoning about agents’ cognitive attitudes of both epistemic type and motivational type. We show that it allows us to express a variety of relevant concepts for qualitative decision theory including the concepts of knowledge, belief, strong belief, conditional belief, desire, conditional desire, strong desire, and preference. We also present two extensions of the logic, one by the notion of choice and the other by dynamic operators for belief change and desire change, and we apply the former to the analysis of single-stage games under incomplete information. We provide sound and complete axiomatizations for the basic logic and for its two extensions.

International audience

This work deals with logical formalization and problem solving using automated solvers. We present the automatic translator TouIST that provides a simple language to generate logical formulas from a problem description. Our tool allows us to model many static or dynamic combinatorial problems and to benefit from the regular improvements of SAT, QBF or SMT solvers in order to solve these problems efficiently. In particular, we show how to use TouIST to solve different classes of planning tasks in Artificial Intelligence.

Evidence logics model agents' belief revision process as they incorporate and aggregate information obtained from multiple sources. This information is captured using neighbourhood structures, where individual neighbourhoods represent pieces of evidence. In this paper we propose an extended framework which allows one to explicitly quantify either the number of evidence sets, or effort, needed to justify a given proposition, provide a complete deductive calculus and a proof of decidability, and show how existing frameworks can be embedded into ours.

We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization and a decidability result for our logic.

We study agents expressing propositional goals over a set of binary issues to reach a collective decision. We adapt properties and rules from the literature on Social Choice Theory to our setting, providing an axiomatic characterisation of a majority rule for goal-based voting. We study the computational complexity of finding the outcome of our rules (i.e., winner determination), showing that it ranges from Nondeterministic Polynomial Time (NP) to Probabilistic Polynomial Time (PP).

In this study we present a game-theoretic model of guilt in relation to sensitivity to norms of fairness. We focus on a specific kind of fairness norm à la Rawls according to which a fair society should be organized so as to admit economic inequalities to the extent that they are beneficial to the less advantaged agents. In a first step, we analyze the impact of the sensitivity to this fairness norm on the behavior of agents who play a repeated Prisoner’s Dilemma and learn via fictitious play. In a second step we transform the base game into a meta-game that represents a static description of a repeated game updated via fictitious play. We analyze such a meta-game under population dynamics by means of evolutionary game theory. Our results reveal two things: first of all, a great sensitivity to the fairness norm is beneficial in the long term when agents have the time to converge to mutual cooperation. Secondly, cooperativeness and fairness norm sensitivity can coevolve in a population of initially solely defectors.

We present a simple Ceteris Paribus Logic (CP) and study its relationship with existing logics that deal with the representation of choice and power in games in normal form including atemporal STIT, Coalition Logic of Propositional Control (CL-PC) and Dynamic Logic of Propositional Assignments (DL-PA). Thanks to the polynomial reduction of the satisfiability problem for atemporal STIT in the satisfiability problem for CP, we obtain a complexity result for the latter problem.

We present a logical analysis of the relation between social influence and responsibility. In particular, we precisely characterise a notion of influence-based responsibility, namely, a responsibility that depends on the fact that an agent causes a primary violation by another agent. This notion captures the core of the idea of indirect (also called secondary or accomplice) responsibility in legal systems, and can be useful in the governance of multiagent systems. Our analysis uses the STIT logic of action (the logic of seeing to it that). On this basis we shall first formalise a notion of influence between agents, and then the idea of influence-based responsibility.

The article introduces a ceteris paribus modal logic, called CP, interpreted on the equivalence classes induced by finite sets of propositional atoms. This logic is studied and then used to embed three logics of strategic interaction, namely atemporal STIT, the coalition logic of propositional control (CL−PC) and the starless fragment of the dynamic logic of propositional assignments (DL−PA). The embeddings highlight a common ceteris paribus structure underpinning the key operators of all these apparently very different logics and show, we argue, remarkable similarities behind some of the most influential formalisms for reasoning about strategic interaction

We propose a modal logic that supports reasoning about trust-based belief change. The term trust-based belief change refers to belief change that depends on the degree of trust the receiver has in the source of information.

International audience

The past years have seen increasing cooperation between psychology and computer science in the field of computational modeling of emotion. However, to realize its potential, the exchange between the two disciplines, as well as the intradisciplinary coordination, should be further improved. We make three proposals for how this could be achieved. The proposals refer to: 1) systematizing and classifying the assumptions of psychological emotion theories; 2) formalizing emotion theories in implementation-independent formal languages (set theory, agent logics); and 3) modeling emotions using general cognitive architectures (such as Soar and ACT-R), general agent architectures (such as the BDI architecture) or general-purpose affective agent architectures. These proposals share two overarching themes. The first is a proposal for modularization: deconstruct emotion theories into basic assumptions; modularize architectures. The second is a proposal for unification and standardization: Translate different emotion theories into a common informal conceptual system or a formal language, or implement them in a common architecture.

International audience

International audience

We propose a formal semantics of intention and plan dynamics based on the notion of local assignment. The function of a local assignment is to change the truth value of a given proposition at a specific time point along a history. We combine a static modal logic including a temporal modality and modal operators for mental attitudes belief and choice, with three kinds of dynamic modalities and corresponding three kinds of local assignments operating on agent's beliefs, on agent's choices and on the physical world. An agent's intention is defined in our approach as the agent's choice to perform a given action at a certain time point in the future and two operations called intention generation and intention reconsideration are defined as specific kinds of local assignments on choices. In Section 1 we introduce a static logic of time, action, and mental attitudes. In Section 2 we add the dynamic notion of local assignment to the logic of Section 1. In Section 3, we focus on two specific kinds of local assignment on choice which allow to model the processes of intention and plan generation and reconsideration.

In the recent years, several formal approaches to the specification of normative multi-agent systems (MASs) and artificial institutions have been proposed. The aim of this article is to advance the state of the art in this area by proposing an approach in which a normative MAS is conceived to be autonomous, in the sense that it is able to create, maintain and eventually change its own institutions by itself, without the intervention of an external designer in this process. In our approach the existence and the dynamics of an institution (norms, rules, institutional facts, etc.) are determined by the (individual and collective) acceptances of its members, and its dynamics depends on the dynamics of these acceptances. In order to meet this objective, we propose the logic 𝒜ℒ (Acceptance Logic) in which the acceptance of a proposition by the agents qua members of an institution is introduced. Such propositions are true w.r.t. an institutional context and correspond to facts that are instituted in an attitude-dependent way. The second part of the article is devoted to the logical characterization of some important notions in the theory of institutions. We provide a formalization of the concept of constitutive rule, expressed by a statement of the form ‘X counts as Y in the context of institution x’. Then, we formalize the concepts of obligation and permission (so called regulative rules). In our approach, constitutive rules and regulative rules of a certain institution are attitude-dependent facts which are grounded on the acceptances of the members of the institution.

Some symbolic AI models, for example, BDI (belief, desire, intention) models are conceived as explicit and operational models of the intentional pursuit and belief dynamics. The main concern of these models is to provide a clear understanding of the functional roles of different kinds of epistemic and motivational states (beliefs, acceptances, expectations, intentions, goals, desires, etc. …), of the relational properties among them. Mental configurations of appraisal (involving different kinds of motivational and epistemic states) which correspond to particular cognitive emotions such as disappointment, fear, relief, shame, etc. … have been analyzed by several authors close to the BDI theoretical tradition. The main objective of this work is a formal analysis of Surprise in a BDI-like cognitive architecture. A clarification of the functional role of Surprise in a BDI-like cognitive architecture with respect to resource bounded belief revision is given.