42 Search Results for "Haase, Christoph"

Document
DOI: 10.4230/LIPIcs.STACS.2026.60
The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices

Authors: Stefan Kiefer and Andrew Ryzhikov

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

Abstract
We study finite semigroups of n × n matrices with rational entries. Such semigroups provide a rich generalization of transition monoids of unambiguous (and, in particular, deterministic) finite automata. In this paper we determine the maximum size of finite semigroups of rational n × n matrices, with the goal of shedding more light on the structure of such matrix semigroups. While in general such semigroups can be arbitrarily large in terms of n, a classical result of Schützenberger from 1962 implies an upper bound of 2^{𝒪(n² log n)} for irreducible semigroups, i.e., the only subspaces of ℚⁿ that are invariant for all matrices in the semigroup are ℚⁿ and the subspace consisting only of the zero vector. Irreducible matrix semigroups can be viewed as the building blocks of general matrix semigroups, and as such play an important role in mathematics and computer science. From the point of view of automata theory, they generalize strongly connected automata. Using a very different technique from that of Schützenberger, we improve the upper bound on the cardinality to 3^{n²}. This is the main result of the paper. The bound is in some sense tight, as we show that there exists, for every n, a finite irreducible semigroup with 3^{⌊ n²/4 ⌋} rational matrices. Our main result also leads to an improvement of a bound, due to Almeida and Steinberg, on the mortality threshold. The mortality threshold is a number 𝓁 such that if the zero matrix is in the semigroup, then the zero matrix can be written as a product of at most 𝓁 matrices from any subset that generates the semigroup.
Cite as

Stefan Kiefer and Andrew Ryzhikov. The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 60:1-60:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.STACS.2026.60,
  author =	{Kiefer, Stefan and Ryzhikov, Andrew},
  title =	{{The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{60:1--60:20},
  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.60},
  URN =		{urn:nbn:de:0030-drops-255496},
  doi =		{10.4230/LIPIcs.STACS.2026.60},
  annote =	{Keywords: finite matrix semigroups, irreducible matrix semigroups, matrix mortality, aperiodic semigroups, unambiguous automata, transition monoids}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.16
On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Authors: Nicolas Peltier

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

Abstract
Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.
Cite as

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{peltier:LIPIcs.CSL.2026.16,
  author =	{Peltier, Nicolas},
  title =	{{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{16:1--16:20},
  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.16},
  URN =		{urn:nbn:de:0030-drops-254402},
  doi =		{10.4230/LIPIcs.CSL.2026.16},
  annote =	{Keywords: Separation logic, Dynamic logic, Entailment problem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.27
Analysis of Logics with Arithmetic

Authors: Michael Benedikt, Chia-Hsuan Lu, and Tony Tan

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

Abstract
We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional "global cardinality constraints": restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.
Cite as

Michael Benedikt, Chia-Hsuan Lu, and Tony Tan. Analysis of Logics with Arithmetic. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.CSL.2026.27,
  author =	{Benedikt, Michael and Lu, Chia-Hsuan and Tan, Tony},
  title =	{{Analysis of Logics with Arithmetic}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{27:1--27: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.27},
  URN =		{urn:nbn:de:0030-drops-254510},
  doi =		{10.4230/LIPIcs.CSL.2026.27},
  annote =	{Keywords: Presburger quantifiers, Spectrum, Guarded logics}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.24
A Note on the Parameterised Complexity of Coverability in Vector Addition Systems

Authors: Michał Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks

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

Abstract
We investigate the parameterised complexity of the classic coverability problem for vector addition systems (VAS): V ⊆ ℤ^d, an initial configuration s ∈ ℕ^d, and a target configuration t ∈ ℕ^d, decide whether starting from s, one can iteratively add vectors from V to ultimately arrive at a configuration that is larger than or equal to t on every coordinate, while not observing any negative value on any coordinate along the way. We consider two natural parameters for the problem: the dimension d and the size of V, defined as the total bitsize of its encoding. We present several results charting the complexity of those two parameterisations, among which the highlight is that coverability for VAS parameterised by the dimension and with all the numbers in the input encoded in unary is complete for the class XNL under PL-reductions. We also discuss open problems in the topic, most notably the question about fixed-parameter tractability for the parameterisation by the size of V.
Cite as

Michał Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks. A Note on the Parameterised Complexity of Coverability in Vector Addition Systems. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pilipczuk_et_al:LIPIcs.IPEC.2025.24,
  author =	{Pilipczuk, Micha{\l} and Schmitz, Sylvain and Sinclair-Banks, Henry},
  title =	{{A Note on the Parameterised Complexity of Coverability in Vector Addition Systems}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{24:1--24:19},
  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.24},
  URN =		{urn:nbn:de:0030-drops-251563},
  doi =		{10.4230/LIPIcs.IPEC.2025.24},
  annote =	{Keywords: vector addition system, Petri net, parameterised complexity, coverability}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.9
Reasoning About Time in DatalogMTL: Course Notes (Invited Paper)

Authors: Przemysław Andrzej Wałęga

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

Abstract
Many real-world applications, such as those in healthcare, finance, and logistics, require reasoning over temporal data. Standard rule-based languages like Datalog, however, lack explicit mechanisms for handling time and temporal dependencies. In this chapter, we discussDatalogMTL, an extension of Datalog with operators frommetric temporal logic that allow to express complex temporal properties. We focus on reasoning algorithms for DatalogMTL, discussing bothmaterialisation, based on fixpoint applications of the immediate consequence operator, and anovel saturation-based extensionthat detects and halts infinite derivations, ensuring both completeness and termination of reasoning.
Cite as

Przemysław Andrzej Wałęga. Reasoning About Time in DatalogMTL: Course Notes (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. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{walega:OASIcs.RW.2024/2025.9,
  author =	{Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  title =	{{Reasoning About Time in DatalogMTL: Course Notes}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{9:1--9:23},
  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.9},
  URN =		{urn:nbn:de:0030-drops-250546},
  doi =		{10.4230/OASIcs.RW.2024/2025.9},
  annote =	{Keywords: DatalogMTL, Logic Programming, Temporal Reasoning}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.60
Reachability in Symmetric VASS

Authors: Łukasz Kamiński and Sławomir Lasota

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

Abstract
We investigate the reachability problem in symmetric vector addition systems with states (vass), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general vass. In another extremal case, the symmetric groups, we show that the reachability problem can be solved in PSpace, regardless of the dimension of input vass (to be contrasted with Ackermannian complexity in general vass). We also consider other groups, in particular alternating and cyclic ones. Furthermore, motivated by the open status of the reachability problem in data vass, we estimate the gain in complexity when the group arises as a combination of the trivial and symmetric groups.
Cite as

Łukasz Kamiński and Sławomir Lasota. Reachability in Symmetric VASS. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 60:1-60:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kaminski_et_al:LIPIcs.MFCS.2025.60,
  author =	{Kami\'{n}ski, {\L}ukasz and Lasota, S{\l}awomir},
  title =	{{Reachability in Symmetric VASS}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{60:1--60:17},
  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.60},
  URN =		{urn:nbn:de:0030-drops-241678},
  doi =		{10.4230/LIPIcs.MFCS.2025.60},
  annote =	{Keywords: vector addition systems, Petri nets, reachability problem, symmetry, permutation group}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.45
Regular Model Checking for Systems with Effectively Regular Reachability Relation

Authors: Javier Esparza and Valentin Krasotin

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

Abstract
Regular model checking is a well-established technique for the verification of regular transition systems (RTS): transition systems whose initial configurations and transition relation can be effectively encoded as regular languages. In 2008, To and Libkin studied RTSs in which the reachability relation (the reflexive and transitive closure of the transition relation) is also effectively regular, and showed that the recurrent reachability problem (whether a regular set L of configurations is reached infinitely often) is polynomial in the size of RTS and the transducer for the reachability relation. We extend the work of To and Libkin by studying the decidability and complexity of verifying almost-sure reachability and recurrent reachability - that is, whether L is reachable or recurrently reachable with probability 1. We then apply our results to the more common case in which only a regular overapproximation of the reachability relation is available. In particular, we extend recent complexity results on verifying safety using regular abstraction frameworks - a technique recently introduced by Czerner, the authors, and Welzel-Mohr - to liveness and almost-sure properties.
Cite as

Javier Esparza and Valentin Krasotin. Regular Model Checking for Systems with Effectively Regular Reachability Relation. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.MFCS.2025.45,
  author =	{Esparza, Javier and Krasotin, Valentin},
  title =	{{Regular Model Checking for Systems with Effectively Regular Reachability Relation}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{45:1--45: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.45},
  URN =		{urn:nbn:de:0030-drops-241525},
  doi =		{10.4230/LIPIcs.MFCS.2025.45},
  annote =	{Keywords: Regular model checking, abstraction, inductive invariants}
}
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.30
Finding Equilibria: Simpler for Pessimists, Simplest for Optimists

Authors: Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini

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

Abstract
We consider equilibria in multiplayer stochastic graph games with terminal-node rewards. In such games, Nash equilibria are defined assuming that each player seeks to maximise their expected payoff, ignoring their aversion or tolerance to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected payoff is replaced by a risk measure. A classical risk measure in the literature is the entropic risk measure, where each player has a real valued parameter capturing their risk-averseness. We introduce the extreme risk measure, which corresponds to extreme cases of entropic risk measure, where players are either extreme optimists or extreme pessimists. Under extreme risk measure, every player is an extremist: an extreme optimist perceives their reward as the maximum payoff that can be achieved with positive probability, while an extreme pessimist expects the minimum payoff achievable with positive probability. We argue that the extreme risk measure, especially in multi-player graph based settings, is particularly relevant as they can model several real life instances such as interactions between secure systems and potential security threats, or distributed controls for safety critical systems. We prove that RSEs defined with the extreme risk measure are guaranteed to exist when all rewards are non-negative. Furthermore, we prove that the problem of deciding whether a given game contains an RSE that generates risk measures within specified intervals is decidable and NP-complete for our extreme risk measure, and even PTIME-complete when all players are extreme optimists, while that same problem is undecidable using the entropic risk measure or even the classical expected payoff. This establishes, to our knowledge, the first decidable fragment for equilibria in simple stochastic games without restrictions on strategy types or number of players.
Cite as

Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini. Finding Equilibria: Simpler for Pessimists, Simplest for Optimists. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.MFCS.2025.30,
  author =	{Brice, L\'{e}onard and Henzinger, Thomas A. and Thejaswini, K. S.},
  title =	{{Finding Equilibria: Simpler for Pessimists, Simplest for Optimists}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-241371},
  doi =		{10.4230/LIPIcs.MFCS.2025.30},
  annote =	{Keywords: Nash equilibria, stochastic games, graph games, risk-sensitive equilibria}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.25
Polynomial-Time Tractable Problems over the p-Adic Numbers

Authors: Manuel Bodirsky and Arno Fehm

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

Abstract
We study the computational complexity of fundamental problems over the p-adic numbers {ℚ}_p and the p-adic integers {ℤ}_p. Guépin, Haase, and Worrell [Florent Guépin et al., 2019] proved that checking satisfiability of systems of linear equations combined with valuation constraints of the form v_p(x) = c for p ≥ 5 is NP-complete (both over {ℤ}_p and over {ℚ}_p), and left the cases p = 2 and p = 3 open. We solve their problem by showing that the problem is NP-complete for {ℤ}₃ and for {ℚ}₃, but that it is in P for {ℤ}₂ and for {ℚ}₂. We also present different polynomial-time algorithms for solvability of systems of linear equations in {ℚ}_p with either constraints of the form v_p(x) ≤ c or of the form v_p(x) ≥ c for c ∈ {ℤ}. Finally, we show how our algorithms can be used to decide in polynomial time the satisfiability of systems of (strict and non-strict) linear inequalities over {ℚ} together with valuation constraints v_p(x) ≥ c for several different prime numbers p simultaneously.
Cite as

Manuel Bodirsky and Arno Fehm. Polynomial-Time Tractable Problems over the p-Adic Numbers. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.MFCS.2025.25,
  author =	{Bodirsky, Manuel and Fehm, Arno},
  title =	{{Polynomial-Time Tractable Problems over the p-Adic Numbers}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{25:1--25:17},
  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.25},
  URN =		{urn:nbn:de:0030-drops-241325},
  doi =		{10.4230/LIPIcs.MFCS.2025.25},
  annote =	{Keywords: p-adic numbers, existential theory, linear theory, constraint satisfaction, linear program feasibility, NP-hardness, polynomial-time algorithm}
}
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.70
Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width

Authors: Aliaume Lopez

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

Abstract
We construct an algorithm that inputs an MSO-interpretation from finite words to graphs, and decides if there exists a k ∈ ℕ such that the class of graphs induced by the interpretation is not well-quasi-ordered by the induced subgraph relation when vertices are freely labelled using {1, …, k}. In case no such k exists, we also prove that the class of graphs is not well-quasi-ordered by the induced subgraph relation when vertices are freely labelled using any well-quasi-ordered set of labels. As a byproduct of our analysis, we prove that for classes of bounded linear clique-width, a weak version of a conjecture by Pouzet holds.
Cite as

Aliaume Lopez. Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 70:1-70:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lopez:LIPIcs.MFCS.2025.70,
  author =	{Lopez, Aliaume},
  title =	{{Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{70:1--70:17},
  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.70},
  URN =		{urn:nbn:de:0030-drops-241773},
  doi =		{10.4230/LIPIcs.MFCS.2025.70},
  annote =	{Keywords: well-quasi-ordering, linear clique-width, MSO transduction, automata theory}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.72
One-Parametric Presburger Arithmetic Has Quantifier Elimination

Authors: Alessio Mansutti and Mikhail R. Starchak

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

Abstract
We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function x ↦ t ⋅ x, where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions x ↦ ⌊x/(f(t))⌋, one for each integer polynomial f. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring ℤ[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.
Cite as

Alessio Mansutti and Mikhail R. Starchak. One-Parametric Presburger Arithmetic Has Quantifier Elimination. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 72:1-72:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mansutti_et_al:LIPIcs.MFCS.2025.72,
  author =	{Mansutti, Alessio and Starchak, Mikhail R.},
  title =	{{One-Parametric Presburger Arithmetic Has Quantifier Elimination}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{72:1--72: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.72},
  URN =		{urn:nbn:de:0030-drops-241794},
  doi =		{10.4230/LIPIcs.MFCS.2025.72},
  annote =	{Keywords: decision procedures, quantifier elimination, non-linear integer arithmetic}
}
Document
DOI: 10.4230/LIPIcs.DNA.31.3
Reachability in Deletion-Only Chemical Reaction Networks

Authors: Bin Fu, Timothy Gomez, Ryan Knobel, Austin Luchsinger, Aiden Massie, Marco Rodriguez, Adrian Salinas, Robert Schweller, and Tim Wylie

Published in: LIPIcs, Volume 347, 31st International Conference on DNA Computing and Molecular Programming (DNA 31) (2025)

Abstract
For general discrete Chemical Reaction Networks (CRNs), the fundamental problem of reachability - the question of whether a target configuration can be produced from a given initial configuration - was recently shown to be Ackermann-complete. However, many open questions remain about which features of the CRN model drive this complexity. We study a restricted class of CRNs with void rules, reactions that only decrease species counts. We further examine this regime in the motivated model of step CRNs, which allow additional species to be introduced in discrete stages. With and without steps, we characterize the complexity of the reachability problem for CRNs with void rules. We show that, without steps, reachability remains polynomial-time solvable for bimolecular systems but becomes NP-complete for larger reactions. Conversely, with just a single step, reachability becomes NP-complete even for bimolecular systems. Our results provide a nearly complete classification of void-rule reachability problems into tractable and intractable cases, with only a single exception.
Cite as

Bin Fu, Timothy Gomez, Ryan Knobel, Austin Luchsinger, Aiden Massie, Marco Rodriguez, Adrian Salinas, Robert Schweller, and Tim Wylie. Reachability in Deletion-Only Chemical Reaction Networks. In 31st International Conference on DNA Computing and Molecular Programming (DNA 31). Leibniz International Proceedings in Informatics (LIPIcs), Volume 347, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.DNA.31.3,
  author =	{Fu, Bin and Gomez, Timothy and Knobel, Ryan and Luchsinger, Austin and Massie, Aiden and Rodriguez, Marco and Salinas, Adrian and Schweller, Robert and Wylie, Tim},
  title =	{{Reachability in Deletion-Only Chemical Reaction Networks}},
  booktitle =	{31st International Conference on DNA Computing and Molecular Programming (DNA 31)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-399-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{347},
  editor =	{Schaeffer, Josie and Zhang, Fei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.31.3},
  URN =		{urn:nbn:de:0030-drops-238521},
  doi =		{10.4230/LIPIcs.DNA.31.3},
  annote =	{Keywords: CRN, Chemical Reaction Network, Reachability, Void Reactions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.38
Reachability in Vector Addition System with States Parameterized by Geometric Dimension

Authors: Yangluo Zheng

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

Abstract
The geometric dimension of a vector addition system with states (VASS), emerged in Leroux and Schmitz (2019) and formalized by Fu, Yang, and Zheng (2024), quantifies the dimension of the vector space spanned by cycle effects in the system. This paper examines the VASS reachability problem through the lens of geometric dimension, revealing key differences from the traditional dimensional parameterization. Notably, we establish that the reachability problem for both geometrically 1-dimensional and 2-dimensional VASS is PSPACE-complete, achieved by extending the pumping technique initially proposed by Czerwiński et al. (2019).
Cite as

Yangluo Zheng. Reachability in Vector Addition System with States Parameterized by Geometric Dimension. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zheng:LIPIcs.CONCUR.2025.38,
  author =	{Zheng, Yangluo},
  title =	{{Reachability in Vector Addition System with States Parameterized by Geometric Dimension}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{38:1--38:18},
  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.38},
  URN =		{urn:nbn:de:0030-drops-239888},
  doi =		{10.4230/LIPIcs.CONCUR.2025.38},
  annote =	{Keywords: Petri net, vector addition system, reachability, geometric dimension, pumping}
}
  • Refine by Type
  • 42 Document/PDF
  • 26 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 19 2025
  • 5 2024
  • 4 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 14 Haase, Christoph
  • 5 Chistikov, Dmitry
  • 4 Kiefer, Stefan
  • 4 Mansutti, Alessio
  • 3 Ryzhikov, Andrew
  • Show More...

  • Refine by Series/Journal
  • 37 LIPIcs
  • 1 OASIcs
  • 4 TGDK

  • Refine by Classification
  • 7 Theory of computation → Logic
  • 6 Theory of computation → Logic and verification
  • 5 Theory of computation → Models of computation
  • 3 Mathematics of computing → Discrete mathematics
  • 3 Theory of computation → Formal languages and automata theory
  • Show More...

  • Refine by Keyword
  • 4 vector addition systems
  • 3 Petri nets
  • 3 Presburger arithmetic
  • 3 quantifier elimination
  • 3 reachability
  • 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