Searcharxiv⌕ Search

arXiv subjects

Jonni Virtema

Publications and source records attributed to Jonni Virtema.

At least 19 recordsLinked to original sources
arXiv2026

Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be formalized together and studied logically. We discover complete characterizations of expressivity for several logics that can express probabilistic statements, conditioning and interventionist counterfactuals. The results characterize the languages in terms of families of linear inequalities and closure conditions that define the corresponding classes of causal multiteams; we find that the strict tensor disjunction, an operator typical of team semantics but absent from the literature on causation, is needed to capture the full class of all linear inequalities. The characterizations yield a strict hierarchy of expressive power and some undefinability results.

cs.LO↗
arXiv2026

Inconsistent Databases and Argumentation Frameworks with Collective Attacks

The connection between subset-maximal repairs for inconsistent databases involving various integrity constraints and acceptable sets of arguments within argumentation frameworks has recently drawn growing interest. In this paper, we contribute to this domain by establishing a new connection when integrity constraints (ICs) include denial constraints and local-as-view tuple-generating dependencies. It turns out that SET-based Argumentation Frameworks (SETAFs), an extension of Dung's argumentation frameworks (AFs) allowing collective attacks, are needed. It is known that subset-maximal repairs under denial constraints correspond to the naive extensions, which also coincide with the preferred and stable extensions in the resulting SETAFs. Our main findings establish that repairs under the considered fragment of tuple-generating dependencies correspond to the preferred extensions. Moreover, for these dependencies, additional preprocessing allows computing a unique extension that is stable and naive. Allowing both types of constraints breaks this relationship, and even the pre-processing does not help as only preferred semantics captures these repairs. Finally, while it is known that functional dependencies do not require set-based attacks, we prove the same regarding inclusion dependencies. Thus, one can translate inconsistent databases under these restricted classes of ICs to plain AFs with attacks only between arguments.

cs.DB↗
arXiv2026

Recurrent Graph Neural Networks and Arithmetic Circuits

We characterise 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. Generalising 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 utilise so-called memory gates which are used to store data between iterations of the recurrent circuit. While (recurrent) GNNs work on labelled graphs, we construct arithmetic circuits that obtain encoded labelled 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. Our results both deepen our understanding of the capabilities of trained neural networks and open new approaches to study recurrent neural networks using the lens of circuit complexity theory.

cs.CC↗
arXiv2026

Locally Consistent K-relations: Entailment and Axioms of Functional Dependence

Local consistency arises in diverse areas, including Bayesian statistics, relational databases, and quantum foundations, and so does the notion of functional dependence. We adopt a general approach to study logical inference in a setting that enables both global inconsistency and local consistency. Our approach builds upon pairwise consistent families of K-relations, i.e, relations with tuples annotated with elements of some positive commutative monoid. The framework covers, e.g., families of probability distributions arising from quantum experiments and their possibilistic counterparts. As a first step, we investigate the entailment problem for functional dependencies (FDs) in this setting. Notably, the transitivity rule for FDs is no longer sound, but can be replaced by two novel axiom schemas. We provide a complete axiomatisation for, and establish NL-completeness of, the entailment problem of unary FDs, and demonstrate that even this restricted case exhibits context-dependent subtleties. In addition, we explore when contextual families over the Booleans have realisations as contextual families over various monoids.

quant-ph↗
arXiv2026

Dichotomy for Axiomatising Inclusion Dependencies on K-Databases

A relation consisting of tuples annotated by an element of a monoid K is called a K-relation. A K-database is a collection of K-relations. In this paper, we study entailment of inclusion dependencies over K-databases, where K is a positive commutative monoid. We establish a dichotomy regarding the axiomatisation of the entailment of inclusion dependencies over K-databases, based on whether the monoid K is weakly absorptive or weakly cancellative. We establish that, if the monoid is weakly cancellative then the standard axioms of inclusion dependencies are sound and complete for the implication problem. If the monoid is not weakly cancellative, it is weakly absorptive and the standard axioms of inclusion dependencies together with the weak symmetry axiom are sound and complete for the implication problem. In addition, we establish that the so-called balance axiom is further required, if one stipulates that the joint weights of each K-relation of a K-database need to be the same; this generalises the notion of a K-relation being a distribution. In conjunction with the balance axiom, weak symmetry axiom boils down to symmetry.

cs.DB↗
arXiv2026

Unifying approach to uniform expressivity of graph neural networks

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 can be interpreted as instantiations of T-GNNs.

cs.LG↗
arXiv2025

Synchronous Team Semantics for Temporal Logics

We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete.

cs.LO↗
arXiv2025

Halting Recurrent GNNs and the Graded $μ$-Calculus

Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN.

cs.LG↗
arXiv2025

Rewriting Consistent Answers on Annotated Data

We embark on a study of the consistent answers of queries over databases annotated with values from a naturally ordered positive semiring. In this setting, the consistent answers of a query are defined as the minimum of the semiring values that the query takes over all repairs of an inconsistent database. The main focus is on self-join free conjunctive queries and key constraints, which is the most extensively studied case of consistent query answering over standard databases. We introduce a variant of first-order logic with a limited form of negation, define suitable semiring semantics, and then establish the main result of the paper: the consistent query answers of a self-join free conjunctive query under key constraints are rewritable in this logic if and only if the attack graph of the query contains no cycles. This result generalizes an analogous result of Koutris and Wijsen for ordinary databases, but also yields new results for a multitude of semirings, including the bag semiring, the tropical semiring, and the fuzzy semiring. Further, for the bag semiring, we show that computing the consistent answers of any self-join free conjunctive query whose attack graph has a strong cycle is not only NP-hard but also it is NP-hard to even approximate the consistent answers with a constant relative approximation guarantee.

cs.DB↗
arXiv2025

A logic-based framework for database repairs

We introduce a general abstract framework for database repairs, where the repair notions are defined using formal logic. We distinguish between integrity constraints and so-called query constraints. The former are used to model consistency and desirable properties of the data (such as functional dependencies and independencies), while the latter relate two database instances according to their answers to the query constraints. The framework allows for a distinction between hard and soft queries, allowing the answers to a core set of queries to be preserved, as well as defining a distance between instances based on query answers. We illustrate how different notions of repairs from the literature can be modelled within our unifying framework. The framework generalises both set-based and cardinality based repairs to semiring annotated databases. Furthermore, we initiate a complexity-theoretic analysis of consistent query answering and checking existence of a repair within the framework.

cs.DB↗
arXiv2024

Graph Neural Networks and Arithmetic Circuits

We characterize the computational power of neural networks that follow the graph neural network (GNN) architecture, not restricted to aggregate-combine GNNs or other particular types. We establish an exact correspondence between the expressivity of GNNs using diverse activation functions and arithmetic circuits over real numbers. In our results the activation function of the network becomes a gate type in the circuit. Our result holds for families of constant depth circuits and networks, both uniformly and non-uniformly, for all common activation functions.

cs.LG↗
arXiv2024

A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL

Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the Until-operator or within the Global-operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the left-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier.

cs.LO↗
arXiv2024

Logics with probabilistic team semantics and the Boolean negation

We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic FOPT. We give a comprehensive picture of the relative expressivity of these logics together with the most studied logics in probabilistic team semantics setting, as well as relating their expressivity to a numerical variant of second-order logic. In addition, we introduce novel entropy atoms and show that the extension of first-order logic by entropy atoms subsumes probabilistic independence logic. Finally, we obtain some results on the complexity of model checking, validity, and satisfiability of our logics.

cs.LO↗
arXiv2024

Temporal Team Semantics Revisited

Temporal logics have been studied as an approach to the specification of hyperproperties, resulting in the conception of "hyperlogics". With a few recent exceptions, the hyperlogics thus far developed can only relate different traces of a transition system synchronously. However, important information is contained in the relation between different points in their asynchronous interaction. To specify such "asynchronous hyperproperties", new trace quantifier based hyperlogics have been developed. Yet, hyperlogics with trace quantification cannot express certain requirements that describe the relationships between all executions of a system. Also, these logics induce model checking problems (MC) with prohibitively high complexity costs in the number of quantifier alternations. We study an alternative approach to asynchronous hyperproperties by introducing a novel foundation of temporal team semantics. Team semantics is a logical framework that specifies properties of sets of traces of unbounded size directly, and thus does not have the same limitation as the quantifier based logics mentioned above. We consider temporal team logics which employ quantification over so-called "time evaluation functions" (TEFs) controlling the asynchronous progress of traces instead of quantification over traces. TEFs constitute a novel approach to defining expressive logics for hyperproperties where diverse asynchronous interactions between computations can be formalised and enforced. We show embeddings of synchronous TeamLTL into our new logics. We show that MC for some TeamCTL fragment is highly undecidable. We present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata, and obtain decidability results for the path checking problem and restrictions of MC and SAT. Our translation constitutes the first approach to team semantics based on automata-theoretic methods.

cs.LO↗
arXiv2023

Computing Repairs Under Functional and Inclusion Dependencies via Argumentation

We discover a connection between finding subset-maximal repairs for sets of functional and inclusion dependencies, and computing extensions within argumentation frameworks (AFs). We study the complexity of the existence of a repair and deciding whether a given tuple belongs to some (or every) repair, by simulating the instances of these problems via AFs. We prove that subset-maximal repairs under functional dependencies correspond to the naive extensions, which also coincide with the preferred and stable extensions in the resulting AFs. For inclusion dependencies, one needs a pre-processing step on the resulting AFs in order for the extensions to coincide. Allowing both types of dependencies breaks this relationship between extensions, and only preferred semantics captures the repairs. Finally, we establish that the complexities of the above decision problems are NP-complete and Pi_2^P-complete, when both functional and inclusion dependencies are allowed.

cs.CC↗
arXiv2023

Complexity of Neural Network Training and ETR: Extensions with Effectively Continuous Functions

We study the complexity of the problem of training neural networks defined via various activation functions. The training problem is known to be existsR-complete with respect to linear activation functions and the ReLU activation function. We consider the complexity of the problem with respect to the sigmoid activation function and other effectively continuous functions. We show that these training problems are polynomial-time many-one bireducible to the existential theory of the reals extended with the corresponding activation functions. In particular, we establish that the sigmoid activation function leads to the existential theory of the reals with the exponential function. It is thus open, and equivalent with the decidability of the existential theory of the reals with the exponential function, whether training neural networks using the sigmoid activation function is algorithmically solvable. In contrast, we obtain that the training problem is undecidable if sinusoidal activation functions are considered. Finally, we obtain general upper bounds for the complexity of the training problem in the form of low levels of the arithmetical hierarchy.

cs.LO↗
arXiv2023

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We establish fascinating connections between the original semantics based on multisets and the new set-based semantics as well as show one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics. We also relate and apply our results to recently defined logics whose asynchronicity is formalized via time evaluation functions.

cs.LO↗