arXiv subjects

Nicolas Troquard

Publications and source records attributed to Nicolas Troquard.

At least 19 recordsLinked to original sources

arXiv2026

Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable

We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for quantized GNNs with readout are (co)NEXPTIME-complete. This result implies that the verification of quantized GNNs is computationally intractable, prompting substantial research efforts toward ensuring the safety of GNN-based systems. We also experimentally demonstrate that quantized ACR-GNN models are lightweight while maintaining good accuracy and generalization capabilities with respect to non-quantized models.

cs.LO↗

arXiv2025

A Simple Logic of Cohesive Group Agency

We propose a structure to represent the social fabric of a group. We call it the `cohesion network' of the group. It can be seen as a graph whose vertices are strict subgroups and whose edges indicate a prescribed `pro-social behaviour' from one subgroup towards another. In social psychology, pro-social behaviours are building blocks of full-blown cooperation, which we assimilate here with `group cohesiveness'. We then define a formal framework to study cohesive group agency. To do so, we simply instantiate pro-social behaviour with the more specific relation of `successful assistance' between acting entities in a group. The relations of assistance within a group at the moment of agency constitute the social fabric of the cohesive group agency. We build our logical theory upon the logic of agency "bringing-it-about". We obtain a family of logics of cohesive group agency, one for every class of cohesion networks.

cs.LO↗

arXiv2025

Verifying Quantized Graph Neural Networks is PSPACE-complete

In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.

cs.LO↗

arXiv2025

A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.

cs.AI↗

arXiv2024

Tracking and managing deemed abilities

Information about the powers and abilities of acting entities is used to coordinate their actions in societies, either physical or digital. Yet, the commonsensical meaning of an acting entity being deemed able to do something is still missing from the existing specification languages for the web or for multi-agent systems. We advance a general purpose abstract logical account of evidence-based ability. A basic model can be thought of as the ongoing trace of a multi-agent system. Every state records systemic confirmations and disconfirmations of whether an acting entity is able to bring about something. Qualitative inductive reasoning is then used in order to infer what acting entities are deemed able to bring about in the multi-agent system. A temporalised modal language is used to talk about deemed ability, actual agency, and confirmation and disconfirmation of deemed ability. What constitutes a confirmation and a disconfirmation is left to the modeller as in general it depends on the application at hand. So to illustrate the methodology we propose two extended examples, one in practical philosophy, the other in system engineering. We first use a logic of agency and ability to obtain a version of Mele's general practical abilities. Then, we look at the management of abilities in a supervised system.

cs.MA↗

arXiv2024

Social, Legal, Ethical, Empathetic, and Cultural Rules: Compilation and Reasoning (Extended Version)

The rise of AI-based and autonomous systems is raising concerns and apprehension due to potential negative repercussions stemming from their behavior or decisions. These systems must be designed to comply with the human contexts in which they will operate. To this extent, Townsend et al. (2022) introduce the concept of SLEEC (social, legal, ethical, empathetic, or cultural) rules that aim to facilitate the formulation, verification, and enforcement of the rules AI-based and autonomous systems should obey. They lay out a methodology to elicit them and to let philosophers, lawyers, domain experts, and others to formulate them in natural language. To enable their effective use in AI systems, it is necessary to translate these rules systematically into a formal language that supports automated reasoning. In this study, we first conduct a linguistic analysis of the SLEEC rules pattern, which justifies the translation of SLEEC rules into classical logic. Then we investigate the computational complexity of reasoning about SLEEC rules and show how logical programming frameworks can be employed to implement SLEEC rules in practical scenarios. The result is a readily applicable strategy for implementing AI systems that conform to norms expressed as SLEEC rules.

cs.AI↗

arXiv2024

On Representing Humans' Soft-Ethics Preferences As Dispositions

The aim of this paper is to represent humans' soft-ethical preferences by means of dispositional properties. We begin by examining real-life situations, termed as scenarios, that involve ethical dilemmas. Users engage with these scenarios, making decisions on how to act and providing justifications for their choices. We adopt a dispositional approach to represent these scenarios and the interaction with the users. Dispositions are properties that are instantiated by any kind of entity and that may manifest if properly triggered. In particular, the dispositional properties we are interested in are the ethical and behavioural ones. The approach will be described by means of examples. The ultimate goal is to implement the results of this work into a software exoskeleton solution aimed at augmenting human capabilities by preserving their soft-ethical preferences in interactions with autonomous systems.

cs.HC↗

arXiv2024

Existence and Verification of Nash Equilibria in Non-Cooperative Contribution Games with Resource Contention

In resource contribution games, a class of non-cooperative games, the players want to obtain a bundle of resources and are endowed with bags of bundles of resources that they can make available into a common for all to enjoy. Available resources can then be used towards their private goals. A player is potentially satisfied with a profile of contributed resources when his bundle could be extracted from the contributed resources. Resource contention occurs when the players who are potentially satisfied, cannot actually all obtain their bundle. The player's preferences are always single-minded (they consider a profile good or they do not) and parsimonious (between two profiles that are equally good, they prefer the profile where they contribute less). What makes a profile of contributed resources good for a player depends on their attitude towards resource contention. We study the problem of deciding whether an outcome is a pure Nash equilibrium for three kinds of players' attitudes towards resource contention: public contention-aversity, private contention-aversity, and contention-tolerance. In particular, we demonstrate that in the general case when the players are contention-averse, then the problem is harder than when they are contention-tolerant. We then identify a natural class of games where, in presence of contention-averse preferences, it becomes tractable, and where there is always a Nash equilibrium.

cs.GT↗

arXiv2023

A Semantic Approach to Decidability in Epistemic Planning (Extended Version)

The use of Dynamic Epistemic Logic (DEL) in multi-agent planning has led to a widely adopted action formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. As such expressive power comes at the cost of undecidability, several decidable fragments have been isolated, mainly based on syntactic restrictions of the action formalism. In this paper, we pursue a novel semantic approach to achieve decidability. Namely, rather than imposing syntactical constraints, the semantic approach focuses on the axioms of the logic for epistemic planning. Specifically, we augment the logic of knowledge S5$_n$ and with an interaction axiom called (knowledge) commutativity, which controls the ability of agents to unboundedly reason on the knowledge of other agents. We then provide a threefold contribution. First, we show that the resulting epistemic planning problem is decidable. In doing so, we prove that our framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest. Second, we study different generalizations of the commutativity axiom, with the goal of obtaining decidability for more expressive fragments of DEL. Finally, we show that two well-known epistemic planning systems based on action templates, when interpreted under the setting of knowledge, conform to the commutativity axiom, hence proving their decidability.

cs.AI↗

arXiv2023

Non-Normal Modal Description Logics (Extended Version)

Modal logics are widely used in multi-agent systems to reason about actions, abilities, norms, or epistemic states. Combined with description logic languages, they are also a powerful tool to formalise modal aspects of ontology-based reasoning over an object domain. However, the standard relational semantics for modalities is known to validate principles deemed problematic in agency, deontic, or epistemic applications. To overcome these difficulties, weaker systems of so-called non-normal modal logics, equipped with neighbourhood semantics that generalise the relational one, have been investigated both at the propositional and at the description logic level. We present here a family of non-normal modal description logics, obtained by extending ALC-based languages with non-normal modal operators. For formulas interpreted on neighbourhood models over varying domains, we provide a modular framework of terminating, correct, and complete tableau-based satisfiability checking algorithms in NExpTime. For a subset of these systems, we also consider a reduction to satisfiability on constant domain relational models. Moreover, we investigate the satisfiability problem in fragments obtained by disallowing the application of modal operators to description logic concepts, providing tight ExpTime complexity results.

cs.LO↗

arXiv2022

Careful Autonomous Agents in Environments With Multiple Common Resources

Careful rational synthesis was defined in (Condurache et al. 2021) as a quantitative extension of Fisman et al.'s rational synthesis (Fisman et al. 2010), as a model of multi-agent systems in which agents are interacting in a graph arena in a turn-based fashion. There is one common resource, and each action may decrease or increase the resource. Each agent has a temporal qualitative objective and wants to maintain the value of the resource positive. One must find a Nash equilibrium. This problem is decidable. In more practical settings, the verification of the critical properties of multi-agent systems calls for models with many resources. Indeed, agents and robots consume and produce more than one type of resource: electric energy, fuel, raw material, manufactured goods, etc. We thus explore the problem of careful rational synthesis with several resources. We show that the problem is undecidable. We then propose a variant with bounded resources, motivated by the observation that in practical settings, the storage of resources is limited. We show that the problem becomes decidable, and is no harder than controller synthesis with Linear-time Temporal Logic objectives.

cs.LO↗

arXiv2021

Resource separation in dynamic logic of propositional assignments

We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.

cs.LO↗

arXiv2020

Individual Resource Games and Resource Redistributions

We introduce a class of resource games where resources and preferences are specified with the language of a resource-sensitive logic. The agents are endowed with a bag of resources and try to achieve a resource objective. For each agent, an action consists in making available a part of their endowed resources. All the resources made available can be used towards the agents' objectives. We study three decision problems, the first of which is deciding whether an action profile is a Nash equilibrium: when all the agents have chosen an action, it is a Nash Equilibrium if no agent has an incentive to change their action unilaterally. When dealing with resources, interesting questions arise as to whether some equilibria can be eliminated or constructed by a central authority by redistributing the available resources among the agents. In our economies, division of property in divorce law exemplifies how a central authority can redistribute the resources of individuals and why they would desire to do so. We thus study two related decision problems: (i) rational elimination: given an action profile's outcome, can the endowed resources be redistributed so that it is not the outcome of a Nash equilibrium? (ii) Rational construction: given an action profile's outcome, can the endowed resources be redistributed so that it is the outcome of a Nash equilibrium? Among other results, we prove that all three problems are PSPACE-complete when the resources are described in the very expressive language of the propositional multiplicative and additive linear logic. We also identify a new modest fragment of linear logic that we call MULT, suitable to represent multisets and reason about the inclusion and equality of bags of resources. We show that when the resources are described in MULT, the problem of deciding whether a profile is a Nash equilibrium is in PTIME.

cs.GT↗

arXiv2019

Learning Ontologies with Epistemic Reasoning: The EL Case

We investigate the problem of learning description logic ontologies from entailments via queries, using epistemic reasoning. We introduce a new learning model consisting of epistemic membership and example queries and show that polynomial learnability in this model coincides with polynomial learnability in Angluin's exact learning model with membership and equivalence queries. We then instantiate our learning framework to EL and show some complexity results for an epistemic extension of EL where epistemic operators can be applied over the axioms. Finally, we transfer known results for EL ontologies and its fragments to our learning model based on epistemic reasoning.

cs.AI↗

arXiv2018

The Complexity of Concurrent Rational Synthesis

In this paper, we investigate the rational synthesis problem for concurrent game structure for a variety of objectives ranging from reachability to Muller condition. We propose a new algorithm that establishes the decidability of the non cooperative rational synthesis problem that relies solely on game theoretic technique as opposed to previous approaches that are logic based. Thanks to this approach, we construct a zero-sum turn-based game that can be adapted to each one of the afore mentioned objectives thus obtain new complexity results. In particular, we show that reachability, safety, Büchi, and co-Büchi conditions are PSpace-complete, Muller, Street, and Rabin are PSpace-hard and in ExpTime.

cs.LO↗

arXiv2017

Repairing Ontologies via Axiom Weakening

Ontology engineering is a hard and error-prone task, in which small changes may lead to errors, or even produce an inconsistent ontology. As ontologies grow in size, the need for automated methods for repairing inconsistencies while preserving as much of the original knowledge as possible increases. Most previous approaches to this task are based on removing a few axioms from the ontology to regain consistency. We propose a new method based on weakening these axioms to make them less restrictive, employing the use of refinement operators. We introduce the theoretical framework for weakening DL ontologies, propose algorithms to repair ontologies based on the framework, and provide an analysis of the computational complexity. Through an empirical analysis made over real-life ontologies, we show that our approach preserves significantly more of the original knowledge of the ontology than removing axioms.

cs.AI↗

arXiv2016

Rational Verification in Iterated Electric Boolean Games

Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems.

cs.GT↗

arXiv2015

Non-normal modalities in variants of Linear Logic

This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of Linear Logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic Linear Logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatization and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the logical framework to use by instantiating it as logics of agency. In particular, we propose a logic to reason about the resource-sensitive use of artefacts and illustrate it with a variety of examples.

cs.LO↗