ABSTRACT. The starting point of this paper is work by Lakemeyer and Levesque, who proposed an epistemic logic where the beliefs of aknowledge-based agent are characterized in terms of increasing levels of complexity. At the lowest level, the agent is only able to draw simple conclusions from its knowledge base. Higher levels lead to more and more inferences and computing the beliefs at any particular level turns out to be tractable. What makes this logic particularly appealing is the fact that the underlying semantics is based on possible worlds. However, the work is still limited in that only beliefs about what is true in the world are considered, that is, an agent's beliefs about its own beliefs are ignored. In this paper we will close this gap and generalize the earlier work by proposing a model of limited belief where anagent is able to fully introspect on its own beliefs without sacrificing tractability.

ABSTRACT. The cops and robber game is a well-studied model for investigating pursuit-evasion phenomena among many others. While many variants of this game have been studied in the literature, the epistemic assumptions underlying their game designs are often left implicit. In this work, we focus on the imperfect information version of the game and re-examine it from an epistemic perspective to explore the levels of player knowledge that are essential for playing the game. To facilitate our investigations, we discuss two kinds of strategies for the players, history-based and positional, and show what matters in this context. Our study eventually sheds light on the implicit assumptions prevalent in the existing literature in terms of player knowledge while playing the game.

ABSTRACT. We present SRIP, a SAT-based system for solving the Independent Set Reconfiguration Problem (ISRP) under the Token Jumping (TJ) rule. SRIP formulates ISRP with SAT problems employing a clique-partition-based constraint model and a set of pruning constraints that strengthen propagation and reduce the search space for reconfiguration. The resulting model is compiled into a sequence of SAT problems and solved using incremental SAT within a bounded model checking framework, enabling SRIP to compute shortest reconfiguration sequences efficiently. We evaluate SRIP on benchmark instances from the CoRe Challenge, a competition series dedicated to ISRP under TJ. SRIP finds optimal (shortest) reconfiguration sequences for 477 out of 693 instances, achieving the best results among state-of-the-art solvers on this benchmark suite.

ABSTRACT. Answer set programming (ASP) in the NP fragment can be solved by translating into propositional satisfiability (SAT). However, for non-tight programs, this requires additional encodings to enforce acyclicity of the underlying dependency graph, making acyclicity handling a key challenge in translating ASP encodings of decision and optimization problems into SAT and maximum satisfiability (MaxSAT). Various SAT encodings of acyclicity exploiting structural graph properties have recently been proposed for various settings. Focusing on ASP, we show that such encodings are captured by a generalized transitive closure framework. The framework can be instantiated for obtaining various types of refined transitive closure encodings. We consider four concrete instantiations framework, analyzing their correctness and size. Putting the framework into practice, we show through extensive empirical evaluation that current state-of-the-art SAT and MaxSAT solvers are competitive with, and can often outperform, state-of-the-art native ASP solvers on both decision and optimization problems.

ABSTRACT. The acceptance of AI agents in daily life hinges on their alignment with social, moral, and legal norms, and in recent years, attempts to build norm-sensitive AI agents --- including reinforcement learning (RL) agents --- have gained traction. However, while there are many promising approaches, they tend to be geared toward environments with modest state spaces, and adaptations to the \textit{deep RL} context are lacking. In this paper we present a deep learning adaptation of \textit{normative restraining bolts} (NRBs). Our contributions are twofold; we combine NRBs with deep Q-networks (DQNs) and proximal policy optimization (PPO) to learn optimal behaviour compliant with challenging norms in a complex environment, demonstrating our agent's ability to learn difficult normative behaviours in the game Pac-Man, which has been used to benchmark normative RL techniques in the past. Secondly, while past work has assumed a lexicographic ordering over conflicting norms when finding appropriate weights for norms, we discuss the shortcomings of this approach, and provide an alternative which is both far more scalable, and allows for the selection of policies deemed ideal by more complex metrics.

ABSTRACT. A normative supervisor is an external module that uses a for- mal reasoning engine to impose normative constraints on re- inforcement learning agents, by either dynamic action mask- ing or feeding the agent additional punishments when vio- lations of norms occur (or both). In this paper, we use a normative supervisor implemented with a solver for deontic answer set programming (ASP) — deolingo — as a ba- sis for the construction of a normative narrator, which uses deolingo’s ability to interface with the explainable solver xclingo to construct a module capable of both regulat- ing behaviour through action masking and additional punish- ments, and providing contrastive explanations of why a given action was allowed while others were not, relative to the nor- mative system being enforced. The explanations are mod- elled after the two tiers – internal and external – of expla- nation. We demonstrate this approach’s ability to provide un- derstandable and descriptive explanations in a scenario where a taxi driver agent must act in accordance to a normative sys- tem governing its normal duties and provisions that must be made in case of an emergency.

ABSTRACT. The paper identifies a relational semantics for theory revision for various notions of bases in arbitrary Tarskian logics. We extend the general work by Delgrande, Woltran and Peppas to the case of logics with infinitely many interpretations, as is the case, e.g., in many predicate logics. First, we identify a property of relations, min-retractivity, that allows for capturing AGM revision semantically in this general setting fully. Part of the characterisation presented is a method for encoding change operators and capture the notion of a base elegant. Moreover, we characterise those logics in which belief revision operators can be represented by a total preorder.

ABSTRACT. Recently, epistemic spaces have been introduced to formalize instantiations of iterated belief change operators and their translations from one concrete representation (epistemic space) to another. In this work, we build on these notions to deepen the understanding of iterated belief change and propose a general method for comparing the expressiveness of existing representations. We introduce the notion of canonicity for epistemic spaces as a tool for identifying those that are sufficiently or necessarily expressive to realize some properties of iterated change operators. In particular, we give the canonical epistemic space (up to equivalence) that allows us to instantiate any iterated change operator.

ABSTRACT. We investigate the truth-tracking performance of iterated belief-change operators. In particular, we show that a class of improvement operators is guaranteed to converge to the truth when the input sequence contains sufficiently many correct inputs, and we establish a corresponding convergence theorem. We also report experimental results indicating that this convergence typically occurs with relatively short input sequences.

ABSTRACT. Rational belief revision is commonly viewed as being based on a preference order between possible worlds, with the resulting new belief set being those sentences true in all the most preferred models of the incoming new information. Usually, such a preference order is taken to be a total preorder. Nevertheless, there are other, more general classes of ordering that can also be employed. In this paper, we explore two such classes that have been studied within the theory of rational choice but have seen limited or no application in belief revision. We begin with interval orders, introduced by Fishburn in the ’80s, which associate to each possible world a nonnegative ‘interval’ of plausibility. We then move on to biorders, studied by Aleskerov, Bouyssou, and Monjardet, which generalise interval orders by allowing the intervals to have negative lengths, a feature that can be used to capture a notion of dissonance or instability. We provide axiomatic characterisations of these two resulting families of belief revision operators, as well as of two further families of interest that lie between interval orders and biorders. We show that while biorder-based revisions satisfy the Success postulate, they do not always yield consistent outputs. By modifying their definition to discard inputs that lead to inconsistency as ‘incredible’, we derive new families of so-called nonprioritised revision that satisfy the Consistency postulate, but not the Success one. These families are linked to credibility-limited revision operators of Hansson et al., but for which the set of credible sentences does not satisfy the single-sentence closure condition. We argue that the biorder-based approach is well-suited for scenarios where an agent might initially reject new information, but may accept it when presented with additional explanation.

ABSTRACT. Domain-independent planning algorithms require as input an action model that specifies the preconditions and effects of each action. Constructing such models is often challenging for domain experts, particularly in domains where actions involve both Boolean and numeric state variables. We address the problem of learning such hybrid action models from observations of successful action executions. A central challenge is that observing only successful executions provides no explicit evidence about which conditions are necessary for an action to be applicable. This difficulty is especially pronounced for learning numeric preconditions, for which there exist negative theoretical results concerning efficient learnability. To mitigate this limitation, we propose SAM-SVM, a novel numeric action model learning algorithm that learns numeric preconditions by heuristically simulating negative observations, i.e., possible states where actions are inapplicable. We also implemented NSAM+SVM, a hybrid algorithm that integrates SAM-SVM and NSAM, an existing conservative action model learning algorithm. Empirical evaluation demonstrates that SAM-SVM can learn more accurate action models and achieves improved planning performance compared to existing methods on standard numeric planning benchmarks, and NSAM+SVM provides the most robust behavior across most domains.

ABSTRACT. We study whether next-token prediction can yield world models that truly support planning, in a controlled symbolic setting where propositional STRIPS action models are learned from action traces alone and correctness can be evaluated exactly. We introduce two architectures. The first is the STRIPS Transformer, a symbolically aligned model grounded in theoretical results linking transformers and the formal language structure of STRIPS domains. The second is a standard transformer architecture without explicit symbolic structure built in, for which we study different positional encoding schemes and attention aggregation mechanisms. We evaluate both architectures on five classical planning domains, measuring training accuracy, generalization, and planning performance across domains and problem sizes. Interestingly, both approaches can be used to produce models that support planning with off-the-shelf STRIPS planners over exponentially many unseen initial states and goals. Although the STRIPS Transformer incorporates a strong symbolic inductive bias, it is harder to optimize and requires larger datasets to generalize reliably. In contrast, a standard transformer with stick-breaking attention achieves near-perfect training accuracy and strong generalization. Finally, standard transformers without stick-breaking attention do not generalize to long traces, whereas a symbolic STRIPS model extracted from a transformer trained on shorter traces does.

ABSTRACT. It has been recently shown that lifted STRIPS models can be learned correctly and efficiently from action traces alone; i.e., applicable action sequences from a hidden STRIPS model. The result is remarkable because the states are not assumed to be observable at all, and yet it is not practical enough as STRIPS actions include arguments that are not needed for selecting the actions. This shortcoming has been addressed by assuming that the action traces come instead from a hidden STRIPS+ model where some action arguments are implicit in the hidden action preconditions. A limitation of this approach, however, is that it assumes that the states are fully observable. In this work, we relax these restrictions and consider the problem of learning a STRIPS+ action domains from traces in a more general context, where the traces carry partial information about both actions and states. In particular, we formulate algorithms and completeness results for three general cases, all of which assume full observability of some action arguments. In the first case, no observability of the state is assumed, in the second case, full observability of some state predicates is assumed, and in the third case, local observability of some state predicates is assumed instead. Given a STRIPS+ domain one can then determine the conditions under which an equivalent domain will be learned from traces. Experimental results are also reported.

ABSTRACT. Parameterized distributed systems induce an infinite family of concurrent systems indexed by the number of processes, and their learnability cannot be reduced to learning a language in isolation. We address the problem of semantic reconstruction for fine broadcast protocols (fine BPs) from a finite labeled sample and provide an inference procedure that returns a minimal semantically equivalent fine BP when the sample subsumes a suitable characteristic set. Furthermore, we establish hardness boundaries on the learnability of fine BPs, including (i) characteristic sets of exponential size are unavoidable, (ii) consistency is NP-hard, and (iii) predictability is non-polynomial.

ABSTRACT. We study the problem of checking consistency of qualitative preferences expressed in CP-theory languages, which is PSPACE-complete in general. Building on Wilson’s seminal work on sufficient conditions for consistency based on Complete Search (CS) trees, we characterize a necessary and sufficient condition for the existence of a cs-tree, yielding the weakest sufficient condition for cs-tree–based consistency. We show that consistency testing under this condition is coNP-complete. We also present a polynomial-time computable upper approximation of the dominance relation for cs-tree–consistent CP-theory preferences, and prove that it subsumes all previously proposed approximations. Finally, we introduce set-labeled cs-trees, a generalization of cs-trees, which provides a unifying framework for progressively weakening sufficient conditions and ultimately characterizes necessary and sufficient conditions for consistency checking in CP-theory preferences.

ABSTRACT. Compiling a collection of votes (a profile) consists in compressing the information it contains in a minimal way, while still allowing to compute the winner after more votes are received. These additional votes can be understood temporally (when votes come in an asynchronous way) or spatially (when votes are gathered locally in polling stations, and their results published locally before being aggregated on a global level). Given a voting rule, two profiles are equivalent for this rule if for whichever profile we add to each of them, the winner in the two expanded profiles will be the same. An equivalence relation between profiles corresponds to a set of information structures (called compilation structures) encoding equivalence classes. It is well-known that some information structures, such as pairwise majority matrices are the compilation structure for some voting rules, while some others (such as the majority graph) are not. We fully characterise the equivalence relations (or equivalently the information structures) that correspond to some voting rules, and we review a number of interesting information structures and give known voting rules that correspond to them.

ABSTRACT. We extend the languages of Coalition Logic (CL) and Alternating-time Temporal Logic (ATL) with new modalities for welfare-affecting capabilities, capturing the benefit and harm that a coalition can bring to another coalition through its strategic choices. These languages are interpreted over concurrent games enriched with agents’ preferences. On the conceptual side, we use these languages to formalize the notions of potential benefactor and danger. A potential benefactor corresponds to a coalition having the capability to confer a benefit on another coalition. Danger corresponds to a coalition having the capability to inflict harm on another coalition. On the technical side, we present several results concerning their axiomatization, their relationships with standard CL and ATL, and their computational complexity.

ABSTRACT. Constraint-based causal discovery is notoriously brittle under finite samples: a small number of erroneous conditional-independence (CI) decisions can cascade into substantial structural errors. We argue that causal discovery under noisy CI evidence is fundamentally a problem of defeasible reasoning rather than pure constraint satisfaction. We introduce Quantitative Argumentation for Causal Discovery, a semantics-driven framework that evaluates edge hypotheses by dialectically aggregating uncertain CI evidence. Instead of treating CI test outcomes as hard constraints, Our method models them as defeasible independence arguments whose strengths are derived from statistical tests. Conflicts are resolved through connectivity-mediated structural undercuts, in which short-range graph structure modulates the impact of local CI claims, yielding a fixed-point acceptability labelling over candidate adjacencies. Across standard benchmark Bayesian networks, our method improves skeleton fidelity and interventional reliability compared with classical constraint-based, hybrid and argumentation-based methods. These results illustrate how quantitative argumentation semantics can serve as a computational mechanism for statistical causal discovery under inconsistent CI evidence.

ABSTRACT. Gradual semantics for weighted bipolar argumentation provide a principled framework for modelling argumentative reasoning, yet existing approaches remain mostly scalar, fixed, and weakly grounded in empirical data. We introduce learnable multi-attribute gradual semantics for persuasion prediction in argumentative debates. Our approach builds a dataset of 600 textual debates converted into multi-attribute argumentation graphs enriched with multi-dimensional features on nodes and relations. Building on this representation, we propose learnable aggregation operators that distinguish intrinsic quality from persuasive strategy dimensions. Experiments show that the learned semantics achieve competitive performance with neural and LLM-based baselines while preserving interpretability.

ABSTRACT. Understanding how policy is debated and justified in parliament is a fundamental aspect of the democratic process. However, the volume and complexity of such debates mean that outside audiences struggle to engage. Meanwhile, Large Language Models (LLMs) have been shown to enable automated summarisation at scale. While summaries of debates can make parliamentary procedures more accessible, evaluating whether these summaries faithfully communicate argumentative content remains challenging. Existing automated summarisation metrics have been shown to correlate poorly with human judgements of consistency (i.e., faithfulness or alignment between summary and source). In this work, we propose a formal framework for evaluating parliamentary debate summaries that grounds argument structures in the contested proposals up for debate. Our novel approach, driven by computational argumentation, focuses the evaluation on formal properties concerning the faithful preservation of the reasoning presented to justify or oppose policy outcomes. We demonstrate our methods using a case-study of debates from the European Parliament and associated LLM-driven summaries.

ABSTRACT. Large language models (LLMs) exhibit strong general capabilities, but their deployment in high-stakes domains is hindered by their opacity and unpredictability. Recent work has taken meaningful steps towards addressing these issues by augmenting LLMs with post-hoc reasoning based on computational argumentation, providing faithful explanations and enabling users to contest incorrect decisions. However, this paradigm is limited to pre-defined binary choices and only supports local contestation for specific instances, leaving the underlying decision logic unchanged and prone to repeated mistakes. In this paper, we introduce ArgEval, a framework that shifts from instance-specific reasoning to structured evaluation of general decision options. Rather than mining arguments solely for individual cases, ArgEval systematically maps task-specific decision spaces, builds corresponding option ontologies, and constructs general argumentation frameworks (AFs) for each option. These frameworks can then be instantiated to provide explainable recommendations for specific cases while still supporting global contestability through modification of the shared AFs. We investigate the effectiveness of ArgEval on treatment recommendation for glioblastoma, an aggressive brain tumour, and show that it can produce explainable guidance aligned with clinical practice.

ABSTRACT. ABA Learning is a recent approach for obtaining Assumption-based Argumentation (ABA) frameworks by reasoning with transformation rules from background knowledge and positive/negative examples of concepts of interest. ABA Learning relies on credulous reasoning under a specific semantic notion of extensions for ABA, namely that of stable extensions. In this paper, we newly frame the problem in terms of credulous reasoning under any semantic notion of extensions for ABA. Focusing on admissible, com- plete, grounded, preferred as well as stable extensions, we present X-ABALearn, a novel parametric algorithm (with X any ABA semantics) based on variants of the transformation rules of ABA Learning and an implementation thereof in Answer Set Programming. Finally, we explore the use of (our implementation of) X-ABALearn on several learning problems, including tabular data and beyond.

ABSTRACT. As reinforcement learning (RL) agents are deployed in increasingly complex environments, ensuring that their behavior complies with the user's needs has become a central challenge in eXplainable RL (XRL). An agent's policy may solve a given problem, but some of its choices can seem counter-intuitive or surprising to the user, who may have wished to see the agent accomplish its goal in a different way, and may wonder: what if the agent acted with a different intent in mind? Scenarios that answer this question are called counterfactual policies. In this work, we propose a framework that allows the user to request these alternative policies by formulating preferences about the behavior of the agent. These preferences are expressed in Linear Temporal Logic on finite traces (LTL_f), a formal yet intuitive language that allows reasoning about deterministic sequences of actions. We synthesize the corresponding counterfactual policies using a multi-objective reinforcement learning algorithm, which produces a diverse set of alternative strategies balancing the agent's original policy with the one envisioned by the user. By comparing these strategies and highlighting their key differences, our framework sheds light on the rationale behind the agent's decisions. Experimental trials show that such a set of policies can be synthesized in reasonable time.

ABSTRACT. Time-critical systems must meet stringent real-time constraints, where correctness depends not only on the order of events but also on their timing. Temporal logics provide a well-established formalism for expressing such requirements, ranging from simple deadlines to interval-bounded obligations. Metric Interval Temporal Logic (MITL) has been used successfully, particularly under the signal-based interpretation, where executions are modeled as Boolean signals. In this context, both Boolean and quantitative semantics have been explored. Specifically, time robustness quantifies tolerance to temporal shifts of signals, either synchronously (all signals shifted together) or asynchronously (each shifted independently). These notions have proven valuable for monitoring, verification, and control synthesis of continuous and hybrid systems. In contrast, in the point-based interpretation, where executions are described as timestamped event sequences, the quantitative semantics of MITL have only been marginally investigated, and the notion of time robustness has not been systematically studied. This paper addresses this gap by introducing a new concept of time robustness for MITL over point-based semantics and demonstrating how this measure can serve as a resilience index against timing perturbations. The proposed robustness is implemented and validated through two case studies.

ABSTRACT. Multi-agent systems involve complex, multilevel interactions between autonomous agents. To contain the complexity, but also help a human modeler, hierarchical models can be used to describe the possible courses of action. In that case, the top-level transition system specifies the behavior of the system at a certain level of abstraction, while some nodes are refined via lower-level models. Hierarchical system specifications were originally studied for reactive processes and their temporal properties. In this short paper, we extend the framework to game-like interaction between proactive agents. To this end, we propose \emph{hierarchical concurrent game models} and define their execution semantic by their unfolding to ordinary, flat concurrent game models. We also make the first steps towards verification of strategic abilities, expressed in alternating-time temporal logic ATL, for hierarchical concurrent games.

ABSTRACT. The simple temporal problem (STP) and its generalization allowing disjunctive constraints (DTP) are some of the most influential reasoning formalisms for representing temporal information in AI. We study the problem of resolving inconsistency of data encoded in the DTP, i.e. given a DTP instance, find the minimum number of constraints to remove to make it satisfiable. While this problem is NP-hard in general, it is reasonable to assume that the amount of erroneous data will be small in practical instances. We therefore study the parameterized complexity of this problem parameterized by the number of constraints to be removed to achieve satisfiability. The expressive power of the formalism and the computational complexity of the problem varies depending on the constraint language, i.e. the types of allowed constraints. Dabrowski et al. (AAAI-2022) achieved full P/NP-hard and FPT/W[1]-hard dichotomies for all STP constraint languages. Our main result is an extension of this result to the more expressive binary DTP languages. The starting point is a classification result for discrete temporal CSPs by Bodirsky et al. (JACM, 2018). Using polymorphisms and other tools from logic and algebra, we provide a fine-grained understanding of the complexity of binary DTP languages. Among the tractable cases, we design an FPT algorithm for the language allowing successor constraints and their negations; this generalizes prominent parameterized separation and transversal problems on graphs, such as Edge Multicut and Group Feedback Edge Set (for the additive group of integers) which have previously been solved by disparate tools.

ABSTRACT. Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems. Traditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification’s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement. In this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-—often by thousands-— improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.

ABSTRACT. The expressive power of Graph Neural Networks (GNNs) is often analysed via correspondence to the Weisfeiler-Leman (WL) algorithm and fragments of first-order logic. Standard GNNs are limited to performing aggregation over immediate neighbourhoods or over global read-outs. To increase their expressivity, recent attempts have been made to incorporate substructural information (e.g. cycle counts and subgraph properties). In this paper, we formalize this architectural trend by introducing Template GNNs (T -GNNs), a generalized framework where node features are updated by aggregating over valid template embeddings from a specified set of graph templates. We propose a corresponding logic, Graded template-modal logic (GML(T )), and generalized notions of template-based bisimulation and WL algorithm. We establish an equivalence between the expressive power of T -GNNs and GML(T ), and provide a unifying approach for analysing GNN expressivity: we show how standard AC-GNNs and its recent variants such as AC+-GNNs can be interpreted as instantiations of T -GNNs.

ABSTRACT. We characterize the computational power of recurrent graph neural networks (GNNs) in terms of arithmetic circuits over the real numbers. Our networks are not restricted to aggregate-combine GNNs or other particular types. Generalizing similar notions from the literature, we introduce the model of recurrent arithmetic circuits, which can be seen as arithmetic analogues of sequential or logical circuits. These circuits utilize so-called memory gates which are used to store data between iterations of the recurrent circuit. While (recurrent) GNNs work on labeled graphs, we construct arithmetic circuits that obtain encoded labeled graphs as real valued tuples and then compute the same function. For the other direction we construct recurrent GNNs which are able to simulate the computations of recurrent circuits. These GNNs are given the circuit-input as initial feature vectors and then, after the GNN-computation, have the circuit-output among the feature vectors of its nodes. In this way we establish an exact correspondence between the expressivity of recurrent GNNs and recurrent arithmetic circuits operating over real numbers.

ABSTRACT. The counting power of Message Passing Neural Networks (MPNN) has been the subject of many recent papers, showing that they express logic that can count up to a threshold or more generally satisfy a linear arithmetic constraint. In this paper, we study the counting capability of MPNN beyond linear arithmetic, primarily utilising local and global mean aggregations. In particular, our goal is to tease out conditions required to express the extensions of graded modal logic with polynomial counting constraints. We show that global polynomial counting constraints in node-labelled graphs can be checked using mean MPNN. Allowing local constraints is also possible, if we consider formulas with no nested modalities and additionally either (i) permit either sum/max aggregations, or (ii) only restrict to regular graphs. We also show how formulas with nested modalities can be captured by mean MPNN over graphs with tree-like structures.

ABSTRACT. In recent years, there has been a growing interest in study- ing the expressive power of graph neural networks (GNNs) by linking them to logical languages. This line of study was started by a key finding by Barceló et al. (2020), who proved that graded modal logic (or the guarded part of the logic C2) characterises the logical expressiveness of aggregate-combine GNNs. They left a “challenging open problem” asking if C2 characterises the logical expressive- ness of aggregate-combine-readout GNNs. This question has stayed open for five years. In this paper, we solve this open problem by showing that aggregate-combine-readout GNNs can express logical classifiers beyond C2.

ABSTRACT. We analyse how the choice of the aggregation function in graph neural networks (GNNs) affects their uniform expressiveness. Allowing arbitrary aggregation yields expressiveness of infinitary graded modal logic. Expressiveness strictly decreases when moving from arbitrary aggregation to sum, from sum to mean, and from mean to max. When GNNs are equipped with global readout and arbitrary aggregation, they have the expressiveness of infinitary C2 and, surprisingly, restricting aggregation to sum does not decrease their expressiveness. In the presence of readout GNNs with mean aggregation are strictly less expressive than with sum and those with sum are strictly less expressive than with max. In the case of simple GNNs, where combination functions are linear transformations followed by a non-linearity and the classification function is a threshold function, the landscape differs. In particular GNNs with sum aggregation and readout no longer have the expressiveness of full infinitary C2. These results provide us with new insights on the expressiveness of GNNs, showing that even subtle architectural modifications can significantly influence their expressive power.