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.

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, this paper proposes 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.

International audience

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula phi can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula.We implemented a generic SAT-based approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i.e. the number of modalities of phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e.g. K, KT, S4)

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

In this paper, some distances between KD45n Kripke models are introduced and investigated. We define several distances between Kripke models, based on different criteria, inspired by various concepts such as bisimulation and propositional distances between valuations for different modal degrees. We study the properties of these distances. Such distances are useful for defining belief change operators in multi-agent scenarios. We show that they can be used to define belief revision operators based on the standard AGM framework and suited to KD45n Kripke models.

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.

Public announcement logic extends multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. In this article, we propose a labelled tableau calculus for this logic, and show that it decides satisfiability of formulas in deterministic polynomial space. Since this problem is known to be PSPACE-complete, it follows that our proof method is optimal.

Public announcement logic is an extension of multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: □φ expresses that φ is true after an arbitrary announcement ψ. As this includes the trivial announcement ⊤, one might as well say that □φ expresses what remains true after any announcement: it therefore corresponds to truth persistence after (definable) relativisation. The dual operation ⋄φ expresses that there is an announcement after which φ. This gives a perspective on Fitch's knowability issues: for which formulas φ does it hold that φ → ⋄Kφ? We give various semantic results, and we show completeness for a Hilbert-style axiomatisation of this logic.