Arrow Research search

Author name cluster

Jonni Virtema

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

25 papers
2 author rows

Possible papers

25

KR Conference 2025 Conference Paper

A Logic-Based Framework for Database Repairs

  • Nicolas Fröhlich
  • Arne Meier
  • Nina Pardal
  • Jonni Virtema

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 repair notions from the literature can be modelled in our framework. The framework generalises both set-based and cardinality based repairs to semiring annotated databases. Finally, we initiate a complexity-theoretic analysis of consistent query answering and checking existence of a repair in our setting.

PDF Details DOI

KR Conference 2025 Conference Paper

Halting Recurrent GNNs and the Graded mu-Calculus

  • Jeroen Bollen
  • Jan Van den Bussche
  • Stijn Vansummeren
  • Jonni Virtema

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.

PDF Details DOI

I&C Journal 2025 Journal Article

Set semantics for asynchronous TeamLTL: Expressivity and complexity

  • Juha Kontinen
  • Max Sandström
  • Jonni Virtema

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 relate the new semantics with the original semantics based on multisets and establish 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.

Details DOI

AAAI Conference 2024 Conference Paper

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

  • Teemu Hankala
  • Miika Hannula
  • Juha Kontinen
  • Jonni Virtema

The training problem of neural networks (NNs) is known to be ER-complete with respect to ReLU and linear activation functions. We show that the training problem for NNs equipped with arbitrary activation functions is polynomial-time bireducible to the existential theory of the reals extended with the corresponding activation functions. For effectively continuous activation functions (e.g., the sigmoid function), we obtain an inclusion to low levels of the arithmetical hierarchy. Consequently, the sigmoid activation function leads to the existential theory of the reals with the exponential function, and hence the decidability of training NNs using the sigmoid activation function is equivalent to the decidability of the existential theory of the reals with the exponential function, a long-standing open problem. In contrast, we obtain that the training problem is undecidable if sinusoidal activation functions are considered.

PDF Details DOI

CSL Conference 2024 Conference Paper

Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

  • Fausto Barbero
  • Jonni Virtema

Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be together formalized 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 equations and closure conditions that define the corresponding classes of causal multiteams. The characterizations yield a strict hierarchy of expressive power. Finally, we present some undefinability results based on the characterizations.

Details

NeurIPS Conference 2024 Conference Paper

Graph Neural Networks and Arithmetic Circuits

  • Timon Barlag
  • Vivian Holzapfel
  • Laura Strieker
  • Jonni Virtema
  • Heribert Vollmer

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.

PDF Details DOI

JELIA Conference 2023 Conference Paper

Logics with Probabilistic Team Semantics and the Boolean Negation

  • Miika Hannula
  • Minna Hirvonen
  • Juha Kontinen
  • Yasir Mahmood 0002
  • Arne Meier
  • Jonni Virtema

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

Details

MFCS Conference 2023 Conference Paper

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

  • Juha Kontinen
  • Max Sandström
  • Jonni Virtema

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 relate the new semantics with the original semantics based on multisets and establish 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.

Details

JELIA Conference 2023 Conference Paper

Strongly Complete Axiomatization for a Logic with Probabilistic Interventionist Counterfactuals

  • Fausto Barbero
  • Jonni Virtema

Abstract Causal multiteam semantics is a framework where probabilistic notions and causal inference can be studied in a unified setting. We study a logic ( \(\mathcal {PCO}\) ) that features marginal probabilities, observations and interventionist counterfactuals, and allows expressing conditional probability statements, do expressions and other mixtures of causal and probabilistic reasoning. Our main contribution is a strongly complete infinitary axiomatisation for \(\mathcal {PCO}\).

Details

KR Conference 2023 Conference Paper

Unified Foundations of Team Semantics via Semirings

  • Timon Barlag
  • Miika Hannula
  • Juha Kontinen
  • Nina Pardal
  • Jonni Virtema

Semiring semantics for first-order logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula. Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending first-order logic with atoms that describe dependencies between variables. Combining these two, we propose a unifying approach for analysing the concepts of dependence and independence via a novel semiring team semantics, which subsumes all the previously considered variants for first-order team semantics. In particular, we study the preservation of satisfaction of dependencies and formulae between different semirings. In addition we create links to reasoning tasks such as provenance, counting, and repairs.

PDF Details DOI

Highlights Conference 2022 Conference Abstract

Temporal Team Semantics Revisited

  • Jonni Virtema

We introduce a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We define three new logics: TeamLTL, TeamCTL and TeamCTL∗, which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We study the complexity of model checking of different fragments of the new logics, and map their undecidability boundier. We show that the model checking problem for already the existential fragment of TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. On the positive side, we present a translation from TeamCTL∗ to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems. Finally, we identify a restrictive setting in which model checking can be done in polynomial time. This is joint work with Jens Oliver Gutsfeld, Arne Meier, and Christoph Ohrem.

Details

CSL Conference 2021 Conference Paper

On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

  • Miika Hannula
  • Juha Kontinen
  • Martin Lück
  • Jonni Virtema

Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k = 1 and both restrictions of the first sort are in effect.

Details

JELIA Conference 2021 Conference Paper

Tractability Frontiers in Probabilistic Team Semantics and Existential Second-Order Logic over the Reals

  • Miika Hannula
  • Jonni Virtema

Abstract Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the complexity and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additive real arithmetic can only express NP properties.

Details

JELIA Conference 2019 Conference Paper

Facets of Distribution Identities in Probabilistic Team Semantics

  • Miika Hannula
  • Åsa Hirvonen
  • Juha Kontinen
  • Vadim Kulikov
  • Jonni Virtema

Abstract We study probabilistic team semantics which is a semantical framework allowing the study of logical and probabilistic dependencies simultaneously. We examine and classify the expressive power of logical formalisms arising by different probabilistic atoms such as conditional independence and different variants of marginal distribution equivalences. We also relate the framework to the first-order theory of the reals and apply our methods to the open question on the complexity of the implication problem of conditional independence.

Details

CSL Conference 2018 Conference Paper

Expressivity Within Second-Order Transitive-Closure Logic

  • Flavio Ferrarotti
  • Jan Van den Bussche
  • Jonni Virtema

Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(exists); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(exists) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.

Details

MFCS Conference 2018 Conference Paper

Team Semantics for the Specification and Verification of Hyperproperties

  • Andreas Krebs
  • Arne Meier
  • Jonni Virtema
  • Martin Zimmermann 0002

We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.

Details

I&C Journal 2017 Journal Article

Complexity of validity for propositional dependence logics

  • Jonni Virtema

We study the complexity of the validity problems of propositional dependence logic, modal dependence logic, and extended modal dependence logic. We show that the validity problem for propositional dependence logic is NEXPTIME -complete. In addition, we establish that the corresponding problems for modal dependence logic and extended modal dependence logic coincide. We show containment in NEXPTIME NP, whereas NEXPTIME -hardness follows from the propositional case.

Details DOI

MFCS Conference 2017 Conference Paper

Model Checking and Validity in Propositional and Modal Inclusion Logics

  • Lauri Hella
  • Antti Kuusisto
  • Arne Meier
  • Jonni Virtema

Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.

Details

MFCS Conference 2016 Conference Paper

Decidability of Predicate Logics with Team Semantics

  • Juha Kontinen
  • Antti Kuusisto
  • Jonni Virtema

We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of dependence logic.

Details

GandALF Workshop 2016 Workshop Paper

On Quantified Propositional Logics and the Exponential Time Hierarchy

  • Miika Hannula
  • Juha Kontinen
  • Martin Lück
  • Jonni Virtema

We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the exponential hierarchy. Second we study propositional team-based logics. We show that DQBF formulae correspond naturally to quantified propositional dependence logic and present a general NEXPTIME upper bound for quantified propositional logic with a large class of generalized dependence atoms. Moreover we show AEXPTIME(poly)-completeness for extensions of propositional team logic with generalized dependence atoms.

PDF Details DOI

TIME Conference 2015 Conference Paper

A Team Based Variant of CTL

  • Andreas Krebs
  • Arne Meier
  • Jonni Virtema

We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeess for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.

Details

CSL Conference 2015 Conference Paper

Axiomatizing Propositional Dependence Logics

  • Katsuhiko Sano
  • Jonni Virtema

We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.

Details

I&C Journal 2014 Journal Article

Complexity of two-variable dependence logic and IF-logic

  • Juha Kontinen
  • Antti Kuusisto
  • Peter Lohmann
  • Jonni Virtema

We study the two-variable fragments D 2 and IF 2 of dependence logic and independence-friendly logic. We consider the satisfiability and finite satisfiability problems of these logics and show that for D 2, both problems are NEXPTIME-complete, whereas for IF 2, the problems are Π 1 0 and Σ 1 0 -complete, respectively. We also show that D 2 is strictly less expressive than IF 2 and that already in D 2, equicardinality of two unary predicates and infinity can be expressed (the latter in the presence of a constant symbol). This is an extended version of a publication in the proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011).

Details DOI

GandALF Workshop 2014 Workshop Paper

Complexity of validity for propositional dependence logics

  • Jonni Virtema

We study the validity problem for propositional dependence logic, modal dependence logic and extended modal dependence logic. We show that the validity problem for propositional dependence logic is NEXPTIME-complete. In addition, we establish that the corresponding problem for modal dependence logic and extended modal dependence logic is NEXPTIME-hard and in NEXPTIME^NP.

PDF Details DOI

CSL Conference 2012 Conference Paper

Undecidable First-Order Theories of Affine Geometries

  • Antti Kuusisto
  • Jeremy Meyers
  • Jonni Virtema

Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2, \beta, \equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2, \beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FO-theory of monadic expansions of (R^n, \beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T, \beta), where T is a subset of R^n, and show that for each structure (T, \beta) in C, the FO-theory of the class of monadic expansions of (T, \beta) is undecidable. We then consider classes of expansions of structures (T, \beta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n, \beta). While the logics are incomparable in general, over expansions of (R^n, \beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. An extended version of this article can be found on the ArXiv (arXiv: 1208. 4930v1).

Details
v2026.09.13