31 Search Results for "Segoufin, Luc"

Document
DOI: 10.4230/LIPIcs.STACS.2026.29
A Pumping-Like Lemma for Languages over Infinite Alphabets

Authors: Yoav Danieli

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We prove a kind of a pumping lemma for languages accepted by one-register alternating finite-memory automata. As a corollary, we obtain that the set of lengths of words in such languages is semi-linear.
Cite as

Yoav Danieli. A Pumping-Like Lemma for Languages over Infinite Alphabets. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{danieli:LIPIcs.STACS.2026.29,
  author =	{Danieli, Yoav},
  title =	{{A Pumping-Like Lemma for Languages over Infinite Alphabets}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle 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.2026.29},
  URN =		{urn:nbn:de:0030-drops-255185},
  doi =		{10.4230/LIPIcs.STACS.2026.29},
  annote =	{Keywords: infinite alphabets, pumping lemma, alternation, semi-linearity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.37
Random Models and Guarded Logic

Authors: Oskar Fiuk

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Building on ideas of Gurevich and Shelah for the Gödel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.
Cite as

Oskar Fiuk. Random Models and Guarded Logic. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.STACS.2026.37,
  author =	{Fiuk, Oskar},
  title =	{{Random Models and Guarded Logic}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{37:1--37:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle 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.2026.37},
  URN =		{urn:nbn:de:0030-drops-255269},
  doi =		{10.4230/LIPIcs.STACS.2026.37},
  annote =	{Keywords: guarded fragment, finite model property, probabilistic method}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.64
One-Clock Synthesis Problems

Authors: Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton, and one of the players can elapse time. We perform a systematic study of synthesis problems in all variants of timed games, depending on which player’s winning condition is specified, and which player’s strategy (or controller, a finite-memory strategy) is sought. As our main result we prove ubiquitous undecidability in all the variants, both for strategy and controller synthesis, already for winning conditions specified by one-clock automata. This strengthens and generalises previously known undecidability results. We also fully characterise those cases where finite memory is sufficient to win, namely existence of a strategy implies existence of a controller. All our results are stated in the timed setting, while analogous results hold in the data setting where one-clock automata are replaced by one-register ones.
Cite as

Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-Clock Synthesis Problems. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 64:1-64:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lasota_et_al:LIPIcs.STACS.2026.64,
  author =	{Lasota, S{\l}awomir and Lehaut, Mathieu and Parreaux, Julie and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{One-Clock Synthesis Problems}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{64:1--64:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle 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.2026.64},
  URN =		{urn:nbn:de:0030-drops-255533},
  doi =		{10.4230/LIPIcs.STACS.2026.64},
  annote =	{Keywords: timed automata, register automata, B\"{u}chi-Landweber games, Church synthesis problem, reactive synthesis problem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.8
Register-Bounded Synthesis from Constraint LTL

Authors: Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables.
Cite as

Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier. Register-Bounded Synthesis from Constraint LTL. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dauvier_et_al:LIPIcs.CSL.2026.8,
  author =	{Dauvier, Nino and Filiot, Emmanuel and Reynier, Pierre-Alain},
  title =	{{Register-Bounded Synthesis from Constraint LTL}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.8},
  URN =		{urn:nbn:de:0030-drops-254322},
  doi =		{10.4230/LIPIcs.CSL.2026.8},
  annote =	{Keywords: Synthesis, Data words, Constraint linear time logic, Register transducer}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.23
Enumeration Kernels for Vertex Cover and Feedback Vertex Set

Authors: Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
Enumerative kernelization is a recent and promising area sitting at the intersection of parameterized complexity and enumeration algorithms. Its study began with the paper of Creignou et al. [Theory Comput. Syst., 2017], and development in the area has started to accelerate with the work of Golovach et al. [J. Comput. Syst. Sci., 2022]. The latter introduced polynomial-delay enumeration kernels and applied them in the study of structural parameterizations of the Matching Cut problem and some variants. Few other results, mostly on Longest Path and some generalizations of Matching Cut, have also been developed. However, little success has been seen in enumeration versions of Vertex Cover and Feedback Vertex Set, some of the most studied problems in kernelization. In this paper, we address this shortcoming. Our first result is a polynomial-delay enumeration kernel with 2k vertices for Enum Vertex Cover, where we wish to list all solutions with at most k vertices. This is obtained by developing a non-trivial lifting algorithm for the classical crown decomposition reduction rule, and directly improves upon the kernel with 𝒪(k²) vertices derived from the work of Creignou et al. Our other result is a polynomial-delay enumeration kernel with 𝒪(k³) vertices and edges for Enum Feedback Vertex Set; the proof is inspired by some ideas of Thomassé [TALG, 2010], but with a weaker bound on the kernel size due to difficulties in applying the q-expansion technique.
Cite as

Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau. Enumeration Kernels for Vertex Cover and Feedback Vertex Set. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bougeret_et_al:LIPIcs.IPEC.2025.23,
  author =	{Bougeret, Marin and C. M. Gomes, Guilherme and dos Santos, Vinicius F. and Sau, Ignasi},
  title =	{{Enumeration Kernels for Vertex Cover and Feedback Vertex Set}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.23},
  URN =		{urn:nbn:de:0030-drops-251552},
  doi =		{10.4230/LIPIcs.IPEC.2025.23},
  annote =	{Keywords: Kernelization, Enumeration, Vertex cover, Crown decomposition, Feedback vertex set}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.96
Counting Small Induced Subgraphs: Scorpions Are Easy but Not Trivial

Authors: Radu Curticapean, Simon Döring, and Daniel Neuen

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
In the parameterized problem #IndSub(Φ) for fixed graph properties Φ, given as input a graph G and an integer k, the task is to compute the number of induced k-vertex subgraphs satisfying Φ. Dörfler et al. [Algorithmica 2022] and Roth et al. [SICOMP 2024] conjectured that #IndSub(Φ) is #W[1]-hard for all non-meager properties Φ, i.e., properties that are nontrivial for infinitely many k. This conjecture has been confirmed for several restricted types of properties, including all hereditary properties [STOC 2022] and all edge-monotone properties [STOC 2024]. We refute this conjecture by showing that induced k-vertex graphs that are scorpions can be counted in time O(n⁴) for all k. Scorpions were introduced more than 50 years ago in the context of the evasiveness conjecture. A simple variant of this construction results in graph properties that achieve arbitrary intermediate complexity assuming ETH. Moreover, we formulate an updated conjecture on the complexity of #IndSub(Φ) that correctly captures the complexity status of scorpions and related constructions.
Cite as

Radu Curticapean, Simon Döring, and Daniel Neuen. Counting Small Induced Subgraphs: Scorpions Are Easy but Not Trivial. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 96:1-96:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{curticapean_et_al:LIPIcs.ESA.2025.96,
  author =	{Curticapean, Radu and D\"{o}ring, Simon and Neuen, Daniel},
  title =	{{Counting Small Induced Subgraphs: Scorpions Are Easy but Not Trivial}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{96:1--96:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.96},
  URN =		{urn:nbn:de:0030-drops-245651},
  doi =		{10.4230/LIPIcs.ESA.2025.96},
  annote =	{Keywords: induced subgraphs, counting complexity, parameterized complexity, scorpions}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.14
Register Automata with Permutations

Authors: Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We propose Permutation Deterministic Register Automata (pDRAs), a deterministic register automaton model where we allow permutations of registers in transitions. The model enables minimal canonical representations and pDRAs can be tested for equivalence in polynomial time. The complexity of minimization is between GI (the complexity of graph isomorphism) and NP. We then introduce a subclass of pDRAs, called register automata with fixed permutation policy, where the register permutation discipline is stipulated globally. This class generalizes the model proposed by Benedikt, Ley and Puppis in 2010, and we show that it also admits minimal and canonical representations, based on a finite-index word equivalence relation. As an application, we show that for any regular data language L, the minimal register automaton with fixed permutation policy recognizing L can be actively learned in polynomial time using oracles for membership, equivalence and data-memorability queries. We show that all the oracles can be implemented in polynomial time, and so this yields a polynomial time minimization algorithm.
Cite as

Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos. Register Automata with Permutations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{balachander_et_al:LIPIcs.MFCS.2025.14,
  author =	{Balachander, Mrudula and Filiot, Emmanuel and Gentilini, Raffaella and Tzevelekos, Nikos},
  title =	{{Register Automata with Permutations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-241219},
  doi =		{10.4230/LIPIcs.MFCS.2025.14},
  annote =	{Keywords: Register automata, data words, equivalence, minimization, active learning}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.22
On the Reachability Problem for Two-Dimensional Branching VASS

Authors: Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem has been known to be decidable for over forty years, and its complexity has recently been precisely characterized. Our work concerns the reachability problem for BVASS, a branching generalization of VASS. In dimension one, the exact complexity of this problem is known. In this paper, we prove that the reachability problem for 2-dimensional BVASS is decidable. In fact, we even show that the reachability set admits a computable semilinear presentation. The decidability status of the reachability problem for BVASS remains open in higher dimensions.
Cite as

Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. On the Reachability Problem for Two-Dimensional Branching VASS. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{biziere_et_al:LIPIcs.MFCS.2025.22,
  author =	{Bizi\`{e}re, Clotilde and Hilaire, Thibault and Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{On the Reachability Problem for Two-Dimensional Branching VASS}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.22},
  URN =		{urn:nbn:de:0030-drops-241294},
  doi =		{10.4230/LIPIcs.MFCS.2025.22},
  annote =	{Keywords: Vector addition systems, Reachability problem, Semilinear sets, Verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.69
FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree

Authors: Markus Lohrey, Sebastian Maneth, and Markus L. Schmid

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Enumerating the result set of a first-order query over a relational structure of bounded degree can be done with linear preprocessing and constant delay. In this work, we extend this result towards the compressed perspective where the structure is given in a potentially highly compressed form by a straight-line program (SLP). Our main result is an algorithm that enumerates the result set of a first-order query over a structure of bounded degree that is represented by an SLP satisfying the so-called apex condition. For a fixed formula, the enumeration algorithm has constant delay and needs a preprocessing time that is linear in the size of the SLP.
Cite as

Markus Lohrey, Sebastian Maneth, and Markus L. Schmid. FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 69:1-69:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lohrey_et_al:LIPIcs.MFCS.2025.69,
  author =	{Lohrey, Markus and Maneth, Sebastian and Schmid, Markus L.},
  title =	{{FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{69:1--69:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.69},
  URN =		{urn:nbn:de:0030-drops-241760},
  doi =		{10.4230/LIPIcs.MFCS.2025.69},
  annote =	{Keywords: Enumeration algorithms, FO-logic, query evaluation over compressed data}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.81
Worst-Case and Average-Case Hardness of Hypercycle and Database Problems

Authors: Cheng-Hao Fu, Andrea Lincoln, and Rene Reyes

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
In this paper we present tight lower-bounds and new upper-bounds for hypergraph and database problems. We give tight lower-bounds for finding minimum hypercycles. We give tight lower-bounds for a substantial regime of unweighted hypercycle. We also give a new faster algorithm for longer unweighted hypercycles. We give a worst-case to average-case reduction from detecting a subgraph of a hypergraph in the worst-case to counting subgraphs of hypergraphs in the average-case. We demonstrate two applications of this worst-case to average-case reduction, which result in average-case lower bounds for counting counting hypercycles in random hypergraphs and queries in average-case databases. Our tight upper and lower bounds for hypercycle detection in the worst-case have immediate implications for the average-case via our worst-case to average-case reductions.
Cite as

Cheng-Hao Fu, Andrea Lincoln, and Rene Reyes. Worst-Case and Average-Case Hardness of Hypercycle and Database Problems. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.ICALP.2025.81,
  author =	{Fu, Cheng-Hao and Lincoln, Andrea and Reyes, Rene},
  title =	{{Worst-Case and Average-Case Hardness of Hypercycle and Database Problems}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{81:1--81:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.81},
  URN =		{urn:nbn:de:0030-drops-234581},
  doi =		{10.4230/LIPIcs.ICALP.2025.81},
  annote =	{Keywords: Hypergraphs, hypercycles, fine-grained complexity, average-case complexity, databases}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.168
Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation

Authors: Olga Martynova and Alexander Okhotin

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
It is proved that the family of tree languages recognized by nondeterministic tree-walking automata is not closed under complementation, solving a problem raised by Bojańczyk and Colcombet (https://doi.org/10.1137/050645427, SIAM J. Comp. 38 (2008) 658-701). In addition, it is shown that nondeterministic tree-walking automata are stronger than unambiguous tree-walking automata.
Cite as

Olga Martynova and Alexander Okhotin. Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 168:1-168:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{martynova_et_al:LIPIcs.ICALP.2025.168,
  author =	{Martynova, Olga and Okhotin, Alexander},
  title =	{{Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{168:1--168:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.168},
  URN =		{urn:nbn:de:0030-drops-235459},
  doi =		{10.4230/LIPIcs.ICALP.2025.168},
  annote =	{Keywords: Finite automata, tree-walking automata, complementation}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICDT.2025.1
The Quest for Faster Join Algorithms (Invited Talk)

Authors: Paraschos Koutris, Shaleen Deep, Austen Fan, and Hangdong Zhao

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

Abstract
Joins are the cornerstone of relational databases. Surprisingly, even after several decades of research in the systems and theory database community, we still lack an understanding of how to design the fastest possible join algorithm. In this talk, we will present the exciting progress the database theory community has achieved in join algorithms over the last two decades. The talk will revolve around five key ideas fundamentally shaping this research area: tree decompositions, data partitioning, leveraging statistical information, enumeration, and algebraic techniques.
Cite as

Paraschos Koutris, Shaleen Deep, Austen Fan, and Hangdong Zhao. The Quest for Faster Join Algorithms (Invited Talk). In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koutris_et_al:LIPIcs.ICDT.2025.1,
  author =	{Koutris, Paraschos and Deep, Shaleen and Fan, Austen and Zhao, Hangdong},
  title =	{{The Quest for Faster Join Algorithms}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{1:1--1:12},
  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.1},
  URN =		{urn:nbn:de:0030-drops-229428},
  doi =		{10.4230/LIPIcs.ICDT.2025.1},
  annote =	{Keywords: Conjunctive Queries, Joins, Tree Decompositions, Enumeration, Semirings}
}
  • Refine by Type
  • 31 Document/PDF
  • 20 Document/HTML

  • Refine by Publication Year
  • 5 2026
  • 15 2025
  • 1 2023
  • 1 2021
  • 2 2020
  • Show More...

  • Refine by Author
  • 9 Segoufin, Luc
  • 2 Figueira, Diego
  • 2 Filiot, Emmanuel
  • 2 Grosshans, Nathan
  • 2 Riveros, Cristian
  • Show More...

  • Refine by Series/Journal
  • 30 LIPIcs
  • 1 DagRep

  • Refine by Classification
  • 6 Theory of computation → Automata over infinite objects
  • 4 Theory of computation → Database theory
  • 3 Theory of computation → Formal languages and automata theory
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • Show More...

  • Refine by Keyword
  • 3 Enumeration
  • 3 register automata
  • 2 Decidability
  • 2 Finite automata
  • 2 Information extraction
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact