DROPS

Document

DOI: 10.4230/LIPIcs.ICDT.2026.4

Computing Consistent Least Upper Bounds in Aggregate Logic

Authors: Aziz Amezian El Khalfioui and Jef Wijsen

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract

We consider the problem of answering conjunctive queries with aggregation on database instances that may violate primary key constraints. In SQL, these queries follow the SELECT-FROM-WHERE-GROUP BY format, where the WHERE clause involves a conjunction of equalities, and the SELECT clause can incorporate aggregate operators like MAX, MIN, SUM, AVG, or COUNT. Repairs of a database instance are defined as inclusion-maximal subsets that satisfy all primary keys. The range-consistent answer to a numerical query over an inconsistent database is a pair [glb, lub], where glb and lub are, respectively, the smallest and the greatest results returned by the query over all possible repairs. While previous work has focused on the computation of the glb, the current paper studies the computation of the lub for a numerical domain of non-negative rational numbers. We introduce the notion of κ-acyclicity for self-join-free conjunctive queries. We show that if the body of a SUM-query is κ-acyclic, then the lub can be computed through a rewriting in first-order aggregate logic. Moreover, we show that this result extends to all aggregate operators that are monotone and associative. Importantly, we also prove the inverse: if the body of a SUM-query is not κ-acyclic, then the lub cannot be computed in first-order aggregate logic.

Cite as

Aziz Amezian El Khalfioui and Jef Wijsen. Computing Consistent Least Upper Bounds in Aggregate Logic. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{amezianelkhalfioui_et_al:LIPIcs.ICDT.2026.4,
  author =	{Amezian El Khalfioui, Aziz and Wijsen, Jef},
  title =	{{Computing Consistent Least Upper Bounds in Aggregate Logic}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.4},
  URN =		{urn:nbn:de:0030-drops-256180},
  doi =		{10.4230/LIPIcs.ICDT.2026.4},
  annote =	{Keywords: Consistent query answering, primary key, conjunctive query, aggregate logic}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2025.20

Flavors of Quantifiers in Hyperlogics

Authors: Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract

Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results.

Cite as

Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa. Flavors of Quantifiers in Hyperlogics. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chalupa_et_al:LIPIcs.FSTTCS.2025.20,
  author =	{Chalupa, Marek and Henzinger, Thomas A. and Oliveira da Costa, Ana},
  title =	{{Flavors of Quantifiers in Hyperlogics}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.20},
  URN =		{urn:nbn:de:0030-drops-251016},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.20},
  annote =	{Keywords: Hyperproperties, Satisfiability, First-order Logic, S1S}
}

Document

Invited Paper

DOI: 10.4230/OASIcs.RW.2024/2025.5

Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper)

Authors: Camille Bourgaux

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract

Real-world datasets are plagued by data quality issues which may render the data inconsistent w.r.t. a set of constraints, be they given by database integrity constraints or ontologies. A prominent way to handle such inconsistent data is to use inconsistency-tolerant semantics to obtain meaningful answers to queries. Most of these semantics are based on some notion of repairs, which represent ways of restoring the data consistency. The most basic kind of repairs is that of subset repairs, which are maximal consistent subsets of the dataset. However, in many scenarios, one can define preferred repairs based on some preference information. These lecture notes present inconsistency-tolerant semantics, focusing on the repair-based ones, then review different kinds of preferred repairs that have been considered in the literature. We present in particular the relationships between different kinds of preferred repairs and other notions related to inconsistency handling, the computational complexity of reasoning with (preferred) repairs, and some implementations.

Cite as

Camille Bourgaux. Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 5:1-5:67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bourgaux:OASIcs.RW.2024/2025.5,
  author =	{Bourgaux, Camille},
  title =	{{Inconsistency-Tolerant Semantics Based on (Preferred) Repairs}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{5:1--5:67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.5},
  URN =		{urn:nbn:de:0030-drops-250504},
  doi =		{10.4230/OASIcs.RW.2024/2025.5},
  annote =	{Keywords: Knowledge bases, databases, inconsistency handling, repairs, preferences}
}

Document

DOI: 10.4230/LIPIcs.DISC.2025.30

Team Formation and Applications

Authors: Yuval Emek, Shay Kutten, Ido Rafael, and Gadi Taubenfeld

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract

A novel long-lived distributed problem, called Team Formation (TF), is introduced together with a message- and time-efficient randomized algorithm. The problem is defined over the asynchronous model with a complete communication graph, using bounded size messages, where a certain fraction of the nodes may experience a generalized, strictly stronger, version of initial failures. The goal of a TF algorithm is to assemble tokens injected by the environment, in a distributed manner, into teams of size σ, where σ is a parameter of the problem. The usefulness of TF is demonstrated by using it to derive efficient algorithms for many distributed problems. Specifically, we show that various (one-shot as well as long-lived) distributed problems reduce to TF. This includes well-known (and extensively studied) distributed problems such as several versions of leader election and threshold detection. For example, we are the first to break the linear message complexity bound for asynchronous implicit leader election. We also improve the time complexity of message-optimal algorithms for asynchronous explicit leader election. Other distributed problems that reduce to TF are new ones, including matching players in online gaming platforms, a generalization of gathering, constructing a perfect matching in an induced subgraph of the complete graph, and more. To complement our positive contribution, we establish a tight lower bound on the message complexity of TF algorithms.

Cite as

Yuval Emek, Shay Kutten, Ido Rafael, and Gadi Taubenfeld. Team Formation and Applications. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 30:1-30:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{emek_et_al:LIPIcs.DISC.2025.30,
  author =	{Emek, Yuval and Kutten, Shay and Rafael, Ido and Taubenfeld, Gadi},
  title =	{{Team Formation and Applications}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{30:1--30:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.30},
  URN =		{urn:nbn:de:0030-drops-248474},
  doi =		{10.4230/LIPIcs.DISC.2025.30},
  annote =	{Keywords: asynchronous message-passing, complete communication graph, initial failures, leader election, matching}
}

Document

RANDOM

DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.41

What Is the Minimum Number of Random Bits Required for Computability and Efficiency in Anonymous Networks?

Authors: Dariusz R. Kowalski, Piotr Krysta, and Shay Kutten

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract

Angluin (STOC'80) and Yamashita and Kameda (PODC'88) show that some useful distributed tasks are impossible (for deterministic algorithms) in a general network if nodes do not possess unique identifiers. However, any task decidable in the non-distributed context, can be solved deterministically if the network has a unique leader. Alternatively, much research has been devoted to randomized distributed algorithms in anonymous networks. We present tight upper and lower bounds for the fundamental question: How much randomness is necessary and sufficient to solve Leader Election (LE) in anonymous networks, i.e., to transform an anonymous network into a non-anonymous one? We prove that at least one random bit per node is required in some cases. Surprisingly, a single random bit is also enough, for a total of n bits, where n is the number of nodes. However, the time complexity of our (total of) n random bits algorithm for general networks turned out to be impractically high. Hence, we also developed time-efficient algorithms for the very symmetric graphs of cliques and cycles, paying only an additional cost of o(n) random bits. The primary steps of our algorithms are of independent interest. At first glance, it seems that using one random bit per node, any algorithm can distinguish only two sets of nodes: those with 0 and those with 1. Our algorithms manage to partition the nodes into more than two sets with high probability. In some sense, they perform the task of a "distributed pseudorandom generator", for example, one of our algorithms turns n bits, one per node, into n unique (with high probability) numbers. Even though a complete graph looks very symmetric, the algorithms explore interesting asymmetries inherent in any n permutations (of n values each), if each describes the assignment (by the adversary) of ports in a node to edges leading to neighbors. Finally, we show how to transform any randomized algorithm that generates xn+o(n) random bits in total to one where each node generates at most x+1 bits. Our results apply to both synchronous and asynchronous networks.

Cite as

Dariusz R. Kowalski, Piotr Krysta, and Shay Kutten. What Is the Minimum Number of Random Bits Required for Computability and Efficiency in Anonymous Networks?. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 41:1-41:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kowalski_et_al:LIPIcs.APPROX/RANDOM.2025.41,
  author =	{Kowalski, Dariusz R. and Krysta, Piotr and Kutten, Shay},
  title =	{{What Is the Minimum Number of Random Bits Required for Computability and Efficiency in Anonymous Networks?}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{41:1--41:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.41},
  URN =		{urn:nbn:de:0030-drops-244071},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.41},
  annote =	{Keywords: Distributed computability, Anonymous Networks, Randomness, Leader Election}
}

Document

DOI: 10.4230/LIPIcs.SAND.2025.5

Undecidability of the Emptiness Problem for Weak Models of Distributed Computing

Authors: Flavio T. Principato, Javier Esparza, and Philipp Czerner

Published in: LIPIcs, Volume 330, 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)

Abstract

Esparza and Reiter have recently conducted a systematic comparative study of weak asynchronous models of distributed computing, in which a network of identical finite-state machines acts cooperatively to decide properties of the network’s graph. They introduced a distributed automata framework encompassing many different models, and proved that w.r.t. their expressive power (the graph properties they can decide) distributed automata collapse into seven equivalence classes. In this contribution, we turn our attention to the formal verification problem: Given a distributed automaton, does it decide a given graph property? We consider a fundamental instance of this question - the emptiness problem: Given a distributed automaton, does it accept any graph at all? Our main result is negative: the emptiness problem is undecidable for six of the seven equivalence classes, and trivially decidable for the remaining class.

Cite as

Flavio T. Principato, Javier Esparza, and Philipp Czerner. Undecidability of the Emptiness Problem for Weak Models of Distributed Computing. In 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 330, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{principato_et_al:LIPIcs.SAND.2025.5,
  author =	{Principato, Flavio T. and Esparza, Javier and Czerner, Philipp},
  title =	{{Undecidability of the Emptiness Problem for Weak Models of Distributed Computing}},
  booktitle =	{4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)},
  pages =	{5:1--5:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-368-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{330},
  editor =	{Meeks, Kitty and Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2025.5},
  URN =		{urn:nbn:de:0030-drops-230582},
  doi =		{10.4230/LIPIcs.SAND.2025.5},
  annote =	{Keywords: Undecidability, Emptiness Problem, distributed Automata}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.14

Repairing Databases over Metric Spaces with Coincidence Constraints

Authors: Youri Kaminsky, Benny Kimelfeld, Ester Livshits, Felix Naumann, and David Wajc

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Datasets often contain values that naturally reside in a metric space: numbers, strings, geographical locations, machine-learned embeddings in a vector space, and so on. We study the computational complexity of repairing inconsistent databases that violate integrity constraints, where the database values belong to an underlying metric space. The goal is to update the database values to retain consistency while minimizing the total distance between the original values and the repaired ones. We consider what we refer to as coincidence constraints, which include unary key constraints, inclusion constraints, foreign keys, and generally any restriction on the relationship between the numbers of cells of different labels (attributes) coinciding in a single value, for a fixed attribute set. We begin by showing that the problem is APX-hard for general metric spaces. We then present an algorithm solving the problem optimally for tree metrics, which generalize both the line metric (i.e., where repaired values are numbers) and the discrete metric (i.e., where we simply count the number of changed values). Combining our algorithm for tree metrics and a classic result on probabilistic tree embeddings, we design a (high probability) logarithmic-ratio approximation for general metrics. We also study the variant of the problem where we limit the allowed change of each individual value. In this variant, it is already NP-complete to decide the existence of any legal repair for a general metric, and we present a polynomial-time repairing algorithm for the case of a line metric.

Cite as

Youri Kaminsky, Benny Kimelfeld, Ester Livshits, Felix Naumann, and David Wajc. Repairing Databases over Metric Spaces with Coincidence Constraints. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kaminsky_et_al:LIPIcs.ICDT.2025.14,
  author =	{Kaminsky, Youri and Kimelfeld, Benny and Livshits, Ester and Naumann, Felix and Wajc, David},
  title =	{{Repairing Databases over Metric Spaces with Coincidence Constraints}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.14},
  URN =		{urn:nbn:de:0030-drops-229554},
  doi =		{10.4230/LIPIcs.ICDT.2025.14},
  annote =	{Keywords: Database repairs, metric spaces, coincidence constraints, inclusion constraints, foreign-key constraints}
}

Document

DOI: 10.4230/LIPIcs.STACS.2025.37

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

Authors: Jorge Gallego-Hernández and Alessio Mansutti

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract

This paper investigates ∃ℝ(ξ^ℤ), that is the extension of the existential theory of the reals by an additional unary predicate ξ^ℤ for the integer powers of a fixed computable real number ξ > 0. If all we have access to is a Turing machine computing ξ, it is not possible to decide whether an input formula from this theory is satisfiable. However, we show an algorithm to decide this problem when - ξ is known to be transcendental, or - ξ is a root of some given integer polynomial (that is, ξ is algebraic). In other words, knowing the algebraicity of ξ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that ξ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ∃ℝ(ξ^ℤ) is - in ExpSpace if ξ is an algebraic number, and - in 3Exp if ξ is a logarithm of an algebraic number, Euler’s e, or the number π, among others. To establish our results, we first observe that the satisfiability problem of ∃ℝ(ξ^ℤ) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over ξ^ℤ. We then prove that these instances have a small witness property: only finitely many integer powers of ξ must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers. As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS, 2023]: when the base of the entropic risk is e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in Exp.

Cite as

Jorge Gallego-Hernández and Alessio Mansutti. On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gallegohernandez_et_al:LIPIcs.STACS.2025.37,
  author =	{Gallego-Hern\'{a}ndez, Jorge and Mansutti, Alessio},
  title =	{{On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{37:1--37:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.37},
  URN =		{urn:nbn:de:0030-drops-228635},
  doi =		{10.4230/LIPIcs.STACS.2025.37},
  annote =	{Keywords: Theory of the reals with exponentiation, decision procedures, computability}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.10

The Complexity of Second-Order HyperLTL

Authors: Hadar Frenkel and Martin Zimmermann

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.

Cite as

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
  author =	{Frenkel, Hadar and Zimmermann, Martin},
  title =	{{The Complexity of Second-Order HyperLTL}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.10},
  URN =		{urn:nbn:de:0030-drops-227679},
  doi =		{10.4230/LIPIcs.CSL.2025.10},
  annote =	{Keywords: HyperLTL, Satisfiability, Model-checking}
}

Document

DOI: 10.4230/DagRep.14.3.31

Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111)

Authors: Juha Kontinen, Jonni Virtema, Heribert Vollmer, Fan Yang, and Nicolas Fröhlich

Published in: Dagstuhl Reports, Volume 14, Issue 3 (2024)

Abstract

This report documents the programme and outcomes of Dagstuhl Seminar "Logics for Dependence and Independence: Expressivity and Complexity" (24111). This seminar served as a follow-up seminar to the highly successful seminars "Dependence Logic: Theory and Applications" (13071), "Logics for Dependence and Independence" (15261) and "Logics for Dependence and Independence" (19031). A key objective of the seminar was to bring together researchers working in dependence logic and in application areas (for this edition with a particular emphasis on the areas of hyperproperties and formal linguistics), so that they can communicate state-of-the-art advances and embark on a systematic interaction. The goal was especially to reach those researchers who have recently started working in this thriving area, as well as researchers working on several aspects of complexity studies of team-based logics as well as expressivity issues, in particular in the just mentioned application areas. In particular, bringing together researchers from areas of theoretical studies with the application areas aimed at enhancing the synergy between the different communities working on dependence logic.

Cite as

Juha Kontinen, Jonni Virtema, Heribert Vollmer, Fan Yang, and Nicolas Fröhlich. Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111). In Dagstuhl Reports, Volume 14, Issue 3, pp. 31-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{kontinen_et_al:DagRep.14.3.31,
  author =	{Kontinen, Juha and Virtema, Jonni and Vollmer, Heribert and Yang, Fan and Fr\"{o}hlich, Nicolas},
  title =	{{Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111)}},
  pages =	{31--51},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{3},
  editor =	{Kontinen, Juha and Virtema, Jonni and Vollmer, Heribert and Yang, Fan and Fr\"{o}hlich, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.3.31},
  URN =		{urn:nbn:de:0030-drops-211827},
  doi =		{10.4230/DagRep.14.3.31},
  annote =	{Keywords: finite model theory, formal linguistics, hyperproperties, information theory, team semantics}
}

Document

DOI: 10.4230/LIPIcs.CSL.2024.15

Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

Authors: Fausto Barbero and Jonni Virtema

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

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.

Cite as

Fausto Barbero and Jonni Virtema. Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{barbero_et_al:LIPIcs.CSL.2024.15,
  author =	{Barbero, Fausto and Virtema, Jonni},
  title =	{{Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.15},
  URN =		{urn:nbn:de:0030-drops-196583},
  doi =		{10.4230/LIPIcs.CSL.2024.15},
  annote =	{Keywords: Interventionist counterfactuals, Multiteam semantics, Causation, Probability logic, Linear inequalities, Expressive power}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2023.60

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

Authors: Juha Kontinen, Max Sandström, and Jonni Virtema

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract

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.

Cite as

Juha Kontinen, Max Sandström, and Jonni Virtema. Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.MFCS.2023.60,
  author =	{Kontinen, Juha and Sandstr\"{o}m, Max and Virtema, Jonni},
  title =	{{Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.60},
  URN =		{urn:nbn:de:0030-drops-185949},
  doi =		{10.4230/LIPIcs.MFCS.2023.60},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, Team Semantics}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2021.52

Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity

Authors: Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract

We study the expressivity and complexity of model checking of linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL -extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.

Cite as

Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 52:1-52:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{virtema_et_al:LIPIcs.FSTTCS.2021.52,
  author =	{Virtema, Jonni and Hofmann, Jana and Finkbeiner, Bernd and Kontinen, Juha and Yang, Fan},
  title =	{{Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{52:1--52:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.52},
  URN =		{urn:nbn:de:0030-drops-155634},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.52},
  annote =	{Keywords: Linear temporal logic, Hyperproperties, Model Checking, Expressivity}
}

Document

DOI: 10.4230/LIPIcs.CSL.2021.27

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

Authors: Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

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.

Cite as

Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hannula_et_al:LIPIcs.CSL.2021.27,
  author =	{Hannula, Miika and Kontinen, Juha and L\"{u}ck, Martin and Virtema, Jonni},
  title =	{{On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{27:1--27:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.27},
  URN =		{urn:nbn:de:0030-drops-134610},
  doi =		{10.4230/LIPIcs.CSL.2021.27},
  annote =	{Keywords: quantified Boolean formulae, computational complexity, second-order logic, Horn and Krom fragment}
}

Document

DOI: 10.4230/LIPIcs.CSL.2018.22

Expressivity Within Second-Order Transitive-Closure Logic

Authors: Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

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.

Cite as

Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema. Expressivity Within Second-Order Transitive-Closure Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ferrarotti_et_al:LIPIcs.CSL.2018.22,
  author =	{Ferrarotti, Flavio and Van den Bussche, Jan and Virtema, Jonni},
  title =	{{Expressivity Within Second-Order Transitive-Closure Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.22},
  URN =		{urn:nbn:de:0030-drops-96896},
  doi =		{10.4230/LIPIcs.CSL.2018.22},
  annote =	{Keywords: Expressive power, Higher order logics, Descriptive complexity}
}

20 Search Results for "Virtema, Jonni"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message