Home

About the Expressive Power and Complexity of Order-Invariance with Two Variables


Order-invariant first-order logic is an extension of first-order logic FO where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. We suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. By contrast, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO.


Published on March 28, 2025
Unbalanced Triangle Detection and Enumeration Hardness for Unions of Conjunctive Queries


We study the enumeration of answers to Unions of Conjunctive Queries (UCQs) with optimal time guarantees. More precisely, we wish to identify the queries that can be solved with linear preprocessing time and constant delay. Despite the basic nature of this problem, it was shown only recently that UCQs can be solved within these time bounds if they admit free-connex union extensions, even if all individual CQs in the union are intractable with respect to the same complexity measure. Our goal is to understand whether there exist additional tractable UCQs, not covered by the currently known algorithms. As a first step, we show that some previously unclassified UCQs are hard using the classic 3SUM hypothesis, via a known reduction from 3SUM to triangle listing in graphs. As a second step, we identify a question about a variant of this graph task that is unavoidable if we want to classify all self-join-free UCQs: is it possible to decide the existence of a triangle in a vertex-unbalanced tripartite graph in linear time? We prove that this task is equivalent in hardness to some family of UCQs. Finally, we show a dichotomy for unions of two self-join-free CQs if we assume the answer to this question is negative. In conclusion, this paper pinpoints a computational barrier in the form of a single decision problem that is key to advancing our understanding of the enumeration complexity of many UCQs. Without a breakthrough for unbalanced triangle detection, we have no hope of finding an […]


Published on March 27, 2025
Characterising memory in infinite games


This paper is concerned with games of infinite duration played over potentially infinite graphs. Recently, Ohlmann (LICS 2022) presented a characterisation of objectives admitting optimal positional strategies, by means of universal graphs: an objective is positional if and only if it admits well-ordered monotone universal graphs. We extend Ohlmann's characterisation to encompass (finite or infinite) memory upper bounds. We prove that objectives admitting optimal strategies with ε-memory less than m (a memory that cannot be updated when reading an ε-edge) are exactly those which admit well-founded monotone universal graphs whose antichains have size bounded by m. We also give a characterisation of chromatic memory by means of appropriate universal structures. Our results apply to finite as well as infinite memory bounds (for instance, to objectives with finite but unbounded memory, or with countable memory strategies). We illustrate the applicability of our framework by carrying out a few case studies, we provide examples witnessing limitations of our approach, and we discuss general closure properties which follow from our results.


Published on March 24, 2025
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable


We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASS) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASS, thus to get decidability we investigate restricted subclasses. On the one hand, we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand, we prove that the language equivalence problem is already Ackermann-hard for deterministic VASS. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.


Published on March 20, 2025
With a little help from your friends: semi-cooperative games via Joker moves


This paper coins the notion of Joker games, a variant of concurrent games where the players are not strictly adversarial. Instead, Player 1 can get help from Player 2 by playing a Joker move. We formalize these games as cost games and develop strategies that minimize the use of Jokers - viewed as costs - to secure a win with the least possible help. Our investigation studies the theoretical underpinnings of these games and their associated Joker strategies. In particular, when comparing our cost-minimal strategies with admissible strategies, we find out that they differ. Moreover, while randomization can be beneficial in conventional concurrent games, it does not aid in winning Joker games, although it can help reduce the number of needed Jokers. We also enhance our framework by introducing a secondary objective, namely by minimizing the number of moves executed by a Joker strategy. Finally, we demonstrate the practical advantages of our approach by applying it to test generation in model-based testing.


Published on March 18, 2025

Managing Editors

 

Stefan Milius
Editor-in-Chief

Brigitte Pientka
Fabio Zanasi
Executive Editors


Editorial Board
Executive Board
Publisher

eISSN: 1860-5974


Logical Methods in Computer Science is an open-access journal, covered by SCOPUS, DBLPWeb of Science, Mathematical Reviews and Zentralblatt. The journal is a member of the Free Journal Network. All journal content is licensed under a Creative Commons license.