Nicolas Troquard

TACAS Conference 2026 Conference Paper

Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring

• Mahrokh Mirani
• Paola Inverardi
• Patrizio Pelliccione
• Franco Raimondi
• Nicolas Troquard

AAMAS Conference 2026 Conference Paper

Leveraging Context-Oriented Programming to Implement Normative Rules in Autonomous Systems

• Roberto Casadei
• Martina De Sanctis
• Gianluca Filippone
• Sara Pettinari
• Gian Luca Scoccia
• Nicolas Troquard

Theincreasingsensitivitytohumanaspectsinautonomoussystems engineering calls for principled approaches to embed normative concerns into their behaviour. Recent research has focused on expressing and validating sets of social, legal, ethical, empathetic, and cultural (SLEEC) concerns as rules, and on verifying that a system design adheres to them. However, to date, there is limited work related to the actual implementation and actuation of SLEECaware behaviours. Yet, we believe that operationalising SLEEC rules can enable responsible behaviour of autonomous systems and advance research on the topic. For this purpose, we propose an operational solution for ethical-aware autonomous systems. Specifically, we devise a principled approach, which we call CO-SLEEC (Context-Oriented SLEEC), connecting the normative setting of SLEEC rules to context-oriented programming (COP). CO-SLEEC promotes runtime adaptation and exhibition of context-dependent ethical behaviour through a modular and transparent design.

AAMAS Conference 2026 Conference Paper

SLEECinFRET: A Tool to Manage Social, Legal, Ethical, Empathetic, and Cultural Requirements

• Mahrokh Mirani
• Franco Raimondi
• Nicolas Troquard

IJCAI Conference 2025 Conference Paper

Verifying Quantized Graph Neural Networks is PSPACE-complete

• Marco Sälzer
• Francois Schwarzentruber
• Nicolas Troquard

In this paper, we investigate 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.

IJCAI Conference 2024 Conference Paper

A Logic for Reasoning about Aggregate-Combine Graph Neural Networks

• Pierre Nunn
• Marco Sälzer
• François Schwarzentruber
• Nicolas Troquard

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.

AAAI Conference 2024 Conference Paper

Social, Legal, Ethical, Empathetic, and Cultural Rules: Compilation and Reasoning

• Nicolas Troquard
• Martina De Sanctis
• Paola Inverardi
• Patrizio Pelliccione
• Gian Luca Scoccia

The rise of AI-based and autonomous systems is raising concerns and apprehension due to potential negative repercussions arising 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.

ECAI Conference 2023 Conference Paper

A Semantic Approach to Decidability in Epistemic Planning

• Alessandro Burigana
• Paolo Felli
• Marco Montali
• Nicolas Troquard

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 S5n 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.

AAMAS Conference 2023 Conference Paper

A Semantic Approach to Decidability in Epistemic Planning

• Alessandro Burigana
• Paolo Felli
• Marco Montali
• Nicolas Troquard

Dynamic Epistemic Logic (DEL) provides a very rich planning formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. The general framework is notoriously undecidable. In this paper, we pursue a novel semantic approach to achieve decidability, by focussing on the logic for epistemic planning, rather then to limit the syntax of the accepted modal formulae. Specifically, we augment the logic S5𝑛 by introducing a new interaction axiom that we call knowledge alignment, in order to control the ability of agents to unboundedly reason on the knowledge of other agents. We show that the resulting epistemic planning problem is decidable. In doing so, we prove that this framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest.

JELIA Conference 2023 Conference Paper

Non-Normal Modal Description Logics

• Tiziano Dalmonte
• Andrea Mazzullo
• Ana Ozaki
• Nicolas Troquard

Abstract 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 \(\smash {\mathcal {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 \(\textsc {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 \(\textsc {ExpTime}\) complexity results.

KR Conference 2023 Conference Paper

Succinctness and Complexity of ALC with Counting Perceptrons

• Pietro Galliani
• Oliver Kutz
• Nicolas Troquard

Perceptron operators have been introduced to knowledge representation languages such as description logics in order to define concepts by listing features with associated weights and by giving a threshold. Semantically, an individual then belongs to such a concept if the weighted sum of the listed features it belongs to reaches that threshold. Such operators have been subsequently applied to cognitively-motivated modelling scenarios and to building bridges between learning and reasoning. However, they suffer from the basic limitation that they cannot consider the weight or number of role fillers. This paper introduces an extension of the basic perceptron operator language to address this shortcoming, defining the language ALCP and answering some basic questions regarding the succinctness and complexity of the new language. Namely, we show firstly that in ALCP+, when weights are positive, the language is expressively equivalent to ALCQ, whilst it is strictly more expressive in the general case allowing also negative weights. Secondly, ALCP+ is shown to be strictly more succinct than ALCQ. Thirdly, capitalising on results concerning the logic ALCSCC, we show that despite the added expressivity, reasoning in ALCP remains EXPTIME-complete.

AAMAS Conference 2023 Conference Paper

Synthesis of Resource-Aware Controllers Against Rational Agents

• Rodica Condurache
• Catalin Dima
• Youssouf Oualhadj
• Nicolas Troquard

This paper proposes new contributions from the field of formal multiagent systems in the pursued efforts of engineering solutions for the sustainable management of common-pool resources in presence of rational agents. Non-cooperative rational synthesis is the task of automatically constructing a controller for a reactive system that ensures a given specification against any individually rational behavior of the system’s components. In this paper we consider the case where the controller has to ensure that the system’s resources are never depleted. We report complexity results for classical specification such as the one given in linear temporal logic.

IJCAI Conference 2022 Conference Paper

Asymmetric Hybrids: Dialogues for Computational Concept Combination (Extended Abstract)

• Guendalina Righetti
• Daniele Porello
• Nicolas Troquard
• Oliver Kutz
• Maria Hedblom
• Pietro Galliani

When considering two concepts in terms of extensional logic, their combination will often be trivial, returning an empty extension. Consider e. g. “a Fish Vehicle”, i. e. , “a Vehicle which is also a Fish”. Still, people use sophisticated strategies to produce new, non-empty concepts. All these strategies involve the human ability to mend the conflicting attributes of the input concepts and to create new properties of the combination. We focus in particular on the case where a Head concept has superior ‘asymmetric’ control over steering the resulting combination (or hybridisation) with a Modifier concept. Specifically, we propose a dialogical model of the cognitive and logical mechanics of this asymmetric form of hybridisation. Its implementation is then evaluated using a combination of example ontologies.

LAMAS&SR Workshop 2022 Workshop Paper

Careful rational synthesis in games with multiple common resources

• Rodica Condurache
• Catalin Dima
• Madalina Jitaru
• Youssouf Oualhadj
• Nicolas Troquard

AAMAS Conference 2021 Conference Paper

Rational Synthesis in the Commons with Careless and Careful Agents

• Rodica Condurache
• Catalin Dima
• Youssouf Oualhadj
• Nicolas Troquard

Turn-based games on graphs are games where the states are controlled by one and only one player who decides which edge to follow. Each player has a temporal objective that he tries to achieve. 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 that satisfies the controller’s objective. In this paper, we tackle this problem in the context of a commons, where each action has a cost or a benefit on one shared common pool energy resource. The paper investigates the problem of synthesising the controller in a commons such that there exists an individually rational behaviour of all the agents in the commons 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 solve the problem of cooperative rational synthesis in these games, focusing on parity objectives.

JELIA Conference 2019 Conference Paper

Learning Ontologies with Epistemic Reasoning: The E\! L Case

• Ana Ozaki
• Nicolas Troquard

Abstract 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 \(\mathcal{E\! L}\) and show some complexity results for an epistemic extension of \(\mathcal{E\! L}\) where epistemic operators can be applied over the axioms. Finally, we transfer known results for \(\mathcal{E\! L}\) ontologies and its fragments to our learning model based on epistemic reasoning.

AAAI Conference 2018 Conference Paper

Repairing Ontologies via Axiom Weakening

• Nicolas Troquard
• Roberto Confalonieri
• Pietro Galliani
• Rafael Peñaloza
• Daniele Porello
• Oliver Kutz

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.

AAAI Conference 2018 Conference Paper

Rich Coalitional Resource Games

• Nicolas Troquard

We propose a simple model of interaction for resourceconscious agents. The resources involved are expressed in fragments of Linear Logic. We investigate a few problems relevant to cooperative games, such as deciding whether a group of agents can form a coalition and act together in a way that satisfies all of them. In terms of solution concepts, we study the computational aspects of the core of a game. The main contributions are a formal link with the existing literature, and complexity results for several classes of models.

IJCAI Conference 2018 Conference Paper

Two Approaches to Ontology Aggregation Based on Axiom Weakening

• Daniele Porello
• Nicolas Troquard
• Rafael Peñaloza
• Roberto Confalonieri
• Pietro Galliani
• Oliver Kutz

Axiom weakening is a novel technique that allows for fine-grained repair of inconsistent ontologies. In a multi-agent setting, integrating ontologies corresponding to multiple agents may lead to inconsistencies. Such inconsistencies can be resolved after the integrated ontology has been built, or their generation can be prevented during ontology generation. We implement and compare these two approaches. First, we study how to repair an inconsistent ontology resulting from a voting-based aggregation of views of heterogeneous agents. Second, we prevent the generation of inconsistencies by letting the agents engage in a turn-based rational protocol about the axioms to be added to the integrated ontology. We instantiate the two approaches using real-world ontologies and compare them by measuring the levels of satisfaction of the agents w. r. t. the ontology obtained by the two procedures.

IJCAI Conference 2016 Conference Paper

Nash Equilibria and Their Elimination in Resource Games

• Nicolas Troquard

We introduce a class of resource games where resources and preferences are described with the language of a resource-sensitive logic. We present two decision problems, the first of which is deciding whether an action profile is a Nash equilibrium. When dealing with resources, interesting questions arise as to whether some undesirable equilibria can be eliminated by a central authority by redistributing the available resources among the agents. We will thus study the decision problem of rational elimination. We will consider them in the contexts of dichotomous or pseudo-dichotomous preferences, and of logics that admit or not the weakening rule. This will offer a variety of complexity results that are applicable to a large number of settings.

ECAI Conference 2014 Conference Paper

A resource-sensitive logic of agency

• Daniele Porello
• Nicolas Troquard

We study a fragment of Intuitionistic Linear Logic combined with non-normal modal operators. Focusing on the minimal modal logic, we provide a Gentzen-style sequent calculus as well as a semantics in terms of Kripke resource models. We show that the proof theory is sound and complete with respect to the class of minimal Kripke resource models. We also show that the sequent calculus allows cut elimination. We put the logical framework to use by instantiating it as a logic of agency. In particular, we apply it to reason about the resource-sensitive use of artefacts.

JAAMAS Journal 2013 Journal Article

Reasoning about coalitional agency and ability in the logics of “bringing-it-about”

• Nicolas Troquard

Abstract The logics of “bringing-it-about” have been part of a prominent tradition for the formalization of individual and institutional agency. They are the logics to talk about what states of affairs an acting entity brings about while abstracting away from the means of action. Elgesem’s proposal analyzes the agency of individual agents as the goal-directed manifestation of an individual ability. It has become an authoritative modern reference. The first contribution of this paper is to extend Elgesem’s logic of individual agency and ability to coalitions. We present a general theory and later propose several possible specializations. As a second contribution, we offer algorithms to reason with the logics of bringing-it-about and we analyze their computational complexity.

AAMAS Conference 2012 Conference Paper

Coalitional Agency and Evidence-Based Ability

• Nicolas Troquard

The logics of “bringing it about” have been part of a prominent tradition for the formalization of individual and institutional agency. Our objective here is to extend Elgesem’s logic of individual agency and ability to coalitions.

JELIA Conference 2012 Conference Paper

On Satisfiability in ATL with Strategy Contexts

• Nicolas Troquard
• Dirk Walther 0002

Abstract This paper is a study of Brihaye et al. ’s ATL with strategy contexts. We focus on memory-less strategies and establish that the resulting logic is undecidable. An immediate corollary follows that the problem of satisfiability checking of every variant of ATL with strategy context introduced by Brihaye et al. is undecidable. We also relate ATL \(_{\textit{sc}}\) with memory-less strategies with ATL with explicit strategies, providing a decidable fragment.

IJCAI Conference 2011 Conference Paper

A Dynamic Logic of Normative Systems

• Andreas Herzig
• Emiliano Lorini
• Fr
• eacute; d
• eacute; ric Moisan
• Nicolas Troquard

We propose a logical framework to represent and reason about agent interactions in normative systems. Our starting point is a dynamic logic of propositional assignments whose satisfiability problem is PSPACE-complete. We show that it embeds Coalition Logic of Propositional Control CL-PC and that various notions of ability and capability can be captured in it. We illustrate it on a water resource management case study. Finally, we show how the logic can be easily extended in order to represent constitutive rules which are also an essential component of the modelling of social reality.

AAMAS Conference 2011 Conference Paper

Knowledge and Control

• Wiebe van der Hoek
• Nicolas Troquard
• Michael Wooldridge

Logics of propositional control, such as van der Hoek and Wooldridge's CL-PC, were introduced in order to represent and reason about scenarios in which each agent within a system is able to exercise unique control over some set of system variables. Our aim in the present paper is to extend the study of logics of propositional control to settings in which these agents have incomplete information about the society they occupy. We consider two possible sources of incomplete information. First, we consider the possibility that an agent is only able to "read" a subset of the overall system variables, and so in any given system state, will have partial information about the state of the system. Second, we consider the possibility that an agent has incomplete information about which agent controls which variables. For both cases, we introduce a logic combining epistemic modalities with the operators of CL-PC, investigate its axiomatization, and discuss its properties.

AAMAS Conference 2010 Conference Paper

Alternating-time Dynamic Logic

• Nicolas Troquard
• Dirk Walther

We propose Alternating-time Dynamic Logic (ADL) as amulti-agent variant of Dynamic Logic in which atomic programs are replaced by coalitions. In ADL, the DynamicLogic operators are parametrised with regular expressionsover coalitions and tests. Such regular expressions describethe dynamic structure of a coalition. This means that, whenmoving from Dynamic Logic to ADL, the focus shifts awayfrom describing what is executed and when, toward describing who is acting and when. While Dynamic Logic providesfor reasoning about complex programs, ADL facilitates reasoning about coalitions with an inner dynamic structure, so-called coordinated coalitions. The semantics for such coalitions involves partial strategies and a variety of ways to combine them. Different combinations of partial strategies giverise to different semantics for ADL. In this paper, we mainlyfocus on one version of the semantics but we provide a discussion on other semantic variants of ADL together withpossible syntactic extensions. We see ADL to be suitablefor the specification and the verification of scheduling andplanning systems, and we therefore present a model checking algorithm for ADL and investigate its computationalcomplexity.

AAMAS Conference 2009 Conference Paper

A Logic of Games and Propositional Control

• Nicolas Troquard
• Wiebe van der Hoek
• Michael Wooldridge

We present a logic for reasoning about strategic games. The logic is a modal formalism, based on the Coalition Logic of Propositional Control, to which we add the notions of outcomes and preferences over outcomes. We study the underlying structure of powers of coalitions as they are expressed in their effectivity function, and formalise a collection of solution concepts. We provide a sound and complete axiomatisation for the logic, and we demonstrate its features by applying it to some problems from social choice theory.

TARK Conference 2009 Conference Paper

A logic of propositional control for truthful implementations

• Nicolas Troquard
• Wiebe van der Hoek
• Michael J. Wooldridge

We introduce a logic designed to support reasoning about social choice functions. The logic includes operators to capture strategic ability, and operators to capture agent preferences. We give a correspondence between formulae in the logic and properties of social choice functions, and show that the logic is expressively complete with respect to social choice functions, i. e. , that every social choice function can be characterised as a formula of the logic. We show the decidability of the logic and give a complete axiomatization. To demonstrate the value of the logic, we show in particular how it can be applied to the problem of determining whether a social choice function is strategy-proof.

TARK Conference 2007 Conference Paper

A normal simulation of coalition logic and an epistemic extension

• Jan M. Broersen
• Andreas Herzig
• Nicolas Troquard

In this paper we show how coalition logic can be reduced to the fusion of a normal modal STIT logic for agency and a standard normal temporal logic for discrete time, and how this multi-modal system can be suitably extended with an epistemic modality. Both systems are complete, and we provide a new axiomatization for the STIT-fragment. The epistemic extension enables us to express that agents see to something under uncertainty about the present state or uncertainty about which action is being taken. In accordance with established terminology in the planning community, we call this version of STIT the ‘conformant STIT’. The conformant STIT enables us to express that agents are able to perform a uniform strategy. As a final word of recommendation for this paper we want to point out that its subject is at the junction of four academic fields, viz. modal logic, philosophy, game-theory and AI-planning.

AAMAS Conference 2007 Conference Paper

Delegation and Mental States

• Emiliano Lorini
• Nicolas Troquard
• Andreas Herzig
• Cristiano Castelfranchi

In the recent literature on multiagent systems there have been several proposals of formal systems for reasoning about delegation. Most of these approaches have dealt with the concept of delegation leaving mental states such as beliefs, goals and intentions out of consideration. The aim of this paper is to develop a formal approach for reasoning about delegation by modeling intentions and beliefs of the delegating agent in an explicit way. We present a logic where it is possible to investigate the relations between the concept of Intention to be and the concept of Delegation.

JELIA Conference 2006 Conference Paper

A STIT-Extension of ATL

• Jan M. Broersen
• Andreas Herzig
• Nicolas Troquard

Abstract A problem in many formalisms for reasoning about multi-agent systems, like ATL or PDL, is the inability to express that a certain complex action (as in PDL), choice or strategy (as in ATL) is performed by an agent. However, in so called STIT-logics, this is exactly the main operator: seeing to it that a certain condition is achieved. Here we present an extension of ATL, introducing ideas from STIT-theory, that can express that a group of agents A perform a certain strategy. As a demonstration of the applicability of the formalism, we show how it sheds new light on the problem of modelling ‘uniform strategies’ in epistemic versions of ATL.

ECAI Conference 2006 Conference Paper

Towards a Logic of Agency and Actions with Duration

• Nicolas Troquard
• Laure Vieu

As far as we know, there is no multi-agent system allowing to talk both about choices of agents or groups of agents, strategies, and about sufficiently rich actions. This paper aims at offering a path towards a new more expressive logical framework by mixing a STIT-like logic of agency with a PDL-like logic of action. We present the syntax and ontological motivations, and we highlight the expressivity of the resulting framework on an example.

AAMAS Conference 2006 Conference Paper

Uniform Choices in STIT

• Nicolas Troquard
• Andreas Herzig