Showing 1–16 of 16 results for author: Schwarzentruber, F

A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

Authors: Pierre Nunn, Marco Sälzer, François Schwarzentruber, Nicolas Troquard

Abstract: 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… ▽ More 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. △ Less

Submitted 30 April, 2024; originally announced May 2024.

Comments: arXiv admin note: text overlap with arXiv:2307.05150

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

Authors: Tiago de Lima, Emiliano Lorini, François Schwarzentruber

Abstract: 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 stat… ▽ More 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. △ Less

Submitted 27 July, 2023; originally announced July 2023.

A Modal Logic for Explaining some Graph Neural Networks

Authors: Pierre Nunn, François Schwarzentruber

Abstract: 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. 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. △ Less

Submitted 11 July, 2023; originally announced July 2023.

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

Authors: Sourav Chakraborty, Avijeet Ghosh, Sujata Ghosh, François Schwarzentruber

Abstract: 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 co… ▽ More 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. △ Less

Submitted 5 June, 2023; originally announced June 2023.

Comments: Accepted in KR 2023

On verifying expectations and observations of intelligent agents

Authors: Sourav Chakraborty, Avijeet Ghosh, Sujata Ghosh, François Schwarzentruber

Abstract: 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… ▽ More 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. △ Less

Submitted 12 May, 2022; v1 submitted 2 May, 2022; originally announced May 2022.

Comments: Accepted in IJCAI-ECAI 2022

Conflict-Based Search for Connected Multi-Agent Path Finding

Authors: Arthur Queffelec, Ocan Sankur, François Schwarzentruber

Abstract: 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 disconn… ▽ More 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. △ Less

Submitted 5 June, 2020; originally announced June 2020.

Dynamic Epistemic Logic Games with Epistemic Temporal Goals

Authors: Bastien Maubert, Aniello Murano, Sophie Pinchinat, François Schwarzentruber, Silvia Stranieri

Abstract: 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 instanc… ▽ More 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. △ Less

Submitted 20 January, 2020; originally announced January 2020.

The Complexity of Tiling Problems

Authors: François Schwarzentruber

Abstract: 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. 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. △ Less

Submitted 21 August, 2019; v1 submitted 28 June, 2019; originally announced July 2019.

The Packed Interval Covering Problem is NP-complete

Authors: Abdallah Saffidine, Sébastien Lê Cong, Sophie Pinchinat, François Schwarzentruber

Abstract: We introduce a new decision problem, called Packed Interval Covering (PIC) and show that it is NP-complete. We introduce a new decision problem, called Packed Interval Covering (PIC) and show that it is NP-complete. △ Less

Submitted 9 June, 2019; originally announced June 2019.

Reachability Games in Dynamic Epistemic Logic

Authors: Bastien Maubert, Sophie Pinchinat, François Schwarzentruber

Abstract: 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 contr… ▽ More 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. △ Less

Submitted 29 May, 2019; originally announced May 2019.

Comments: Long version of a work accepted at the conference IJCAI 2019

Reachability and Coverage Planning for Connected Agents: Extended Version

Authors: Tristan Charrier, Arthur Queffelec, Ocan Sankur, François Schwarzentruber

Abstract: Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. We study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents on… ▽ More Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. We study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents on various classes of topological graphs. We establish the complexity of these problems on known classes, and introduce a new class called sight-moveable graphs which admit efficient algorithms. △ Less

Submitted 11 March, 2019; originally announced March 2019.

Dynamic Connected Cooperative Coverage Problem

Authors: Tristan Charrier, François Schwarzentruber, Eva Soulier

Abstract: We study the so-called dynamic coverage problem by agents located in some topological graph. The agents must visit all regions of interest but they also should stay connected to the base via multi-hop. We prove that the algorithmic complexity of this planning problem is PSPACE-complete. Furthermore we prove that the problem becomes NP-complete for bounded plans. We also prove the same complexities… ▽ More We study the so-called dynamic coverage problem by agents located in some topological graph. The agents must visit all regions of interest but they also should stay connected to the base via multi-hop. We prove that the algorithmic complexity of this planning problem is PSPACE-complete. Furthermore we prove that the problem becomes NP-complete for bounded plans. We also prove the same complexities for the reachability problem of some positions. We also prove that complexities are maintained for a subclass of topological graphs. △ Less

Submitted 15 October, 2018; originally announced October 2018.

Dynamic Gossip

Authors: Hans van Ditmarsch, Jan van Eijck, Pere Pardo, Rahim Ramezanian, François Schwarzentruber

Abstract: A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. The goal is for all agents to get to know all secrets, in which case we call the execution of the protocol successful. We consider distributed and dynamic gossip protocols. In distributed gossip the agents themselves instead of a global scheduler determine whom to call. In dynamic gossip not o… ▽ More A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. The goal is for all agents to get to know all secrets, in which case we call the execution of the protocol successful. We consider distributed and dynamic gossip protocols. In distributed gossip the agents themselves instead of a global scheduler determine whom to call. In dynamic gossip not only secrets are exchanged but also telephone numbers (agent identities). This results in increased graph connectivity. We define six such distributed dynamic gossip protocols, and we characterize them in terms of the topology of the graphs on which they are successful, wherein we distinguish strong success (the protocol always terminates, possibly assuming fair scheduling) from weak success (the protocol sometimes terminates). For five of these protocols strong (fair) and weak success are characterized by weakly connected graphs. This result is surprising because the protocols are fairly different. In the sixth protocol an agent may only call another agent if it does not know the other agent's secret. Strong success for this protocol is characterized by graphs for which the set of non-terminal nodes is strongly connected. Weak success for this protocol is characterized by weakly connected graphs satisfying further topological constraints that we define in the paper. One direction of this characterization is surprisingly harder to prove than the other results in this contribution. △ Less

Submitted 12 February, 2018; v1 submitted 3 November, 2015; originally announced November 2015.

Journal ref: Bulletin of the Iranian Mathematical Society, 2018

DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE

Authors: Philippe Balbiani, Andreas Herzig, François Schwarzentruber, Nicolas Troquard

Abstract: We prove that the model checking and the satisfiability problem of both Dynamic Logic of Propositional Assignments DL-PA and Coalition Logic of Propositional Control and Delegation DCL-PC are in PSPACE. We explain why the proof of EXPTIME-hardness of the model checking problem of DL-PA presented in (Balbiani, Herzig, Troquard, 2013) is false. We also explain why the proof of membership in PSPACE o… ▽ More We prove that the model checking and the satisfiability problem of both Dynamic Logic of Propositional Assignments DL-PA and Coalition Logic of Propositional Control and Delegation DCL-PC are in PSPACE. We explain why the proof of EXPTIME-hardness of the model checking problem of DL-PA presented in (Balbiani, Herzig, Troquard, 2013) is false. We also explain why the proof of membership in PSPACE of the model checking problem of DCL-PC given in (van der Hoek, Walther, Wooldridge, 2010) is wrong. △ Less

Submitted 28 November, 2014; originally announced November 2014.

Ceteris Paribus Structure in Logics of Game Forms

Authors: Davide Grossi, Emiliano Lorini, Francois Schwarzentruber

Abstract: The article introduces a ceteris paribus modal logic interpreted on the equivalence classes induced by sets of propositional atoms. This logic is used to embed two logics of agency and games, namely atemporal STIT and the coalition logic of propositional control (CL-PC). The embeddings highlight a common ceteris paribus structure underpinning the key modal operators of both logics, they clarify th… ▽ More The article introduces a ceteris paribus modal logic interpreted on the equivalence classes induced by sets of propositional atoms. This logic is used to embed two logics of agency and games, namely atemporal STIT and the coalition logic of propositional control (CL-PC). The embeddings highlight a common ceteris paribus structure underpinning the key modal operators of both logics, they clarify the relationship between STIT and CL-PC, and enable the transfer of complexity results to the ceteris paribus logic. △ Less

Submitted 23 October, 2013; originally announced October 2013.

Comments: 11 pages, Contributed talk at TARK 2013 (arXiv:1310.6382) http://www.tark.org

Report number: TARK/2013/p94

On the Complexity of Dynamic Epistemic Logic

Authors: Guillaume Aucher, Francois Schwarzentruber

Abstract: Although Dynamic Epistemic Logic (DEL) is an influential logical framework for representing and reasoning about information change, little is known about the computational complexity of its associated decision problems. In fact, we only know that for public announcement logic, a fragment of DEL, the satisfiability problem and the model-checking problem are respectively PSPACE-complete and in P. We… ▽ More Although Dynamic Epistemic Logic (DEL) is an influential logical framework for representing and reasoning about information change, little is known about the computational complexity of its associated decision problems. In fact, we only know that for public announcement logic, a fragment of DEL, the satisfiability problem and the model-checking problem are respectively PSPACE-complete and in P. We contribute to fill this gap by proving that for the DEL language with event models, the model-checking problem is, surprisingly, PSPACE-complete. Also, we prove that the satisfiability problem is NEXPTIME-complete. In doing so, we provide a sound and complete tableau method deciding the satisfiability problem. △ Less

Submitted 23 October, 2013; originally announced October 2013.

Comments: 10 pages, Contributed talk at TARK 2013 (arXiv:1310.6382) http://www.tark.org

Report number: TARK/2013/p19