Searcharxiv⌕ Search

arXiv subjects

François Schwarzentruber

Publications and source records attributed to François Schwarzentruber.

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↗
arXiv2026

Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality

We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that ``everyone knows everything Alice says''. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana.

cs.AI↗
arXiv2025

On Dynamic Programming Theory for Leader-Follower Stochastic Games

Leader-follower general-sum stochastic games (LF-GSSGs) model sequential decision-making under asymmetric commitment, where a leader commits to a policy and a follower best responds, yielding a strong Stackelberg equilibrium (SSE) with leader-favourable tie-breaking. This paper introduces a dynamic programming (DP) framework that applies Bellman recursion over credible sets-state abstractions formally representing all rational follower best responses under partial leader commitments-to compute SSEs. We first prove that any LF-GSSG admits a lossless reduction to a Markov decision process (MDP) over credible sets. We further establish that synthesising an optimal memoryless deterministic leader policy is NP-hard, motivating the development of ε-optimal DP algorithms with provable guarantees on leader exploitability. Experiments on standard mixed-motive benchmarks-including security games, resource allocation, and adversarial planning-demonstrate empirical gains in leader value and runtime scalability over state-of-the-art methods.

cs.GT↗
arXiv2025

Lecture Notes on Verifying Graph Neural Networks

In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.

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

Reasoning About Knowledge on Regular Expressions is 2EXPTIME-complete

Logics for reasoning about knowledge and actions have seen many applications in various domains of multi-agent systems, including epistemic planning. Change of knowledge based on observations about the surroundings forms a key aspect in such planning scenarios. Public Observation Logic (POL) is a variant of public announcement logic for reasoning about knowledge that gets updated based on public observations. Each state in an epistemic (Kripke) model is equipped with a set of expected observations. These states evolve as the expectations get matched with the actual observations. In this work, we prove that the satisfiability problem of $\POL$ is 2EXPTIME-complete.

cs.AI↗
arXiv2025

Linear Planar 3-SAT and Its Applications in Planning

Several fragments of the satisfiability problem have been studied in the literature. Among these, Linear 3-SAT is a satisfaction problem in which each clause (viewed as a set of literals) intersects with at most one other clause; moreover, any pair of clauses have at most one literal in common. Planar 3-SAT is a fragment which requires that the so-called variable-clause graph is planar. Both fragments are NP-complete and have applications in encoding NP-hard planning problems. In this paper, we investigate the complexity and applications of the fragment obtained combining both features. We define Linear Planar 3-SAT and prove its NP-completeness. We also study the reconfiguration problem of Linear Planar 3-SAT and show that it is PSPACE-complete. As an application, we use these new results to prove the NP-completeness of Bounded Connected Multi-Agent Pathfinding and the PSPACE-completeness of Connected Multi-Agent Pathfinding in two-dimensional grids.

cs.CC↗
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

A Computationally Grounded Framework for Cognitive Attitudes (extended version)

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.

cs.LO↗
arXiv2023

Base-based Model Checking for Multi-Agent Only Believing (long version)

We present a novel semantics for the language of multi-agent only believing exploiting belief bases, and show how to use it for automatically checking formulas of this language and of its dynamic extension with private belief expansion operators. We provide a PSPACE algorithm for model checking relying on a reduction to QBF and alternative dedicated algorithm relying on the exploration of the state space. We present an implementation of the QBF-based algorithm and some experimental results on computation time in a concrete example.

cs.AI↗
arXiv2023

A Modal Logic for Explaining some Graph Neural Networks

In this paper, 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 each GNN can be transformed into a formula. We show that the satisfiability problem is decidable. We also discuss some variants that are in PSPACE.

cs.AI↗
arXiv2023

On simple expectations and observations of intelligent agents: A complexity study

Public observation logic (POL) reasons about agent expectations and agent observations in various real world situations. The expectations of agents take shape based on certain protocols about the world around and they remove those possible scenarios where their expectations and observations do not match. This in turn influences the epistemic reasoning of these agents. In this work, we study the computational complexity of the satisfaction problems of various fragments of POL. In the process, we also highlight the inevitable link that these fragments have with the well-studied Public announcement logic.

cs.LO↗
arXiv2022

On verifying expectations and observations of intelligent agents

Public observation logic (POL) is a variant of dynamic epistemic logic to reason about agent expectations and agent observations. Agents have certain expectations, regarding the situation at hand, that are actuated by the relevant protocols, and they eliminate possible worlds in which their expectations do not match with their observations. In this work, we investigate the computational complexity of the model checking problem for POL and prove its PSPACE-completeness. We also study various syntactic fragments of POL. We exemplify the applicability of POL model checking in verifying different characteristics and features of an interactive system with respect to the distinct expectations and (matching) observations of the system. Finally, we provide a discussion on the implementation of the model checking algorithms.

cs.LO↗
arXiv2020

Conflict-Based Search for Connected Multi-Agent Path Finding

We study a variant of the multi-agent path finding problem (MAPF) in which agents are required to remain connected to each other and to a designated base. This problem has applications in search and rescue missions where the entire execution must be monitored by a human operator. We re-visit the conflict-based search algorithm known for MAPF, and define a variant where conflicts arise from disconnections rather than collisions. We study optimizations, and give experimental results in which we compare our algorithms with the literature.

cs.AI↗
arXiv2020

Dynamic Epistemic Logic Games with Epistemic Temporal Goals

Dynamic Epistemic Logic (DEL) is a logical framework in which one can describe in great detail how actions are perceived by the agents, and how they affect the world. DEL games were recently introduced as a way to define classes of games with imperfect information where the actions available to the players are described very precisely. This framework makes it possible to define easily, for instance, classes of games where players can only use public actions or public announcements. These games have been studied for reachability objectives, where the aim is to reach a situation satisfying some epistemic property expressed in epistemic logic; several (un)decidability results have been established. In this work we show that the decidability results obtained for reachability objectives extend to a much more general class of winning conditions, namely those expressible in the epistemic temporal logic LTLK. To do so we establish that the infinite game structures generated by DEL public actions are regular, and we describe how to obtain finite representations on which we rely to solve them.

cs.LO↗
arXiv2019

The Complexity of Tiling Problems

In this document, we collected the most important complexity results of tilings. We also propose a definition of a so-called deterministic set of tile types, in order to capture deterministic classes without the notion of games. We also pinpoint tiling problems complete for respectively LOGSPACE and NLOGSPACE.

cs.CC↗
arXiv2019

Reachability Games in Dynamic Epistemic Logic

We define reachability games based on Dynamic Epistemic Logic (DEL), where the players' actions are finely described as DEL action models. We first consider the setting where an external controller with perfect information interacts with an environment and aims at reaching some epistemic goal state regarding the passive agents of the system. We study the problem of strategy existence for the controller, which generalises the classic epistemic planning problem, and we solve it for several types of actions such as public announcements and public actions. We then consider a yet richer setting where agents themselves are players, whose strategies must be based on their observations. We establish several (un)decidability results for the problem of existence of a distributed strategy, depending on the type of actions the players can use, and relate them to results from the literature on multiplayer games with imperfect information.

cs.LO↗