30 Search Results for "Jecker, Ismaël"

Document
DOI: 10.4230/LIPIcs.STACS.2026.67
Pumping-Like Results for Copyless Cost Register Automata and Polynomially Ambiguous Weighted Automata

Authors: Filip Mazowiecki, Antoni Puch, and Daniel Smertnig

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

Abstract
In this work we consider two rich subclasses of weighted automata over fields: polynomially ambiguous weighted automata and copyless cost register automata. Primarily we are interested in understanding their expressiveness power. Over the field of rationals and 1-letter alphabets, it is known that the two classes coincide; they are equivalent to linear recurrence sequences (LRS) whose exponential bases are roots of rationals. We develop a tool we call Pumping Sequence Families, which, by exploiting the simple single-letter behaviour of the models, yields two pumping-like results over arbitrary fields with unrestricted alphabets, one for each class. As a corollary of these results, we present examples proving that the two classes become incomparable over the field of rationals with unrestricted alphabets. We complement the results by analysing the zeroness and equivalence problems. For weighted automata (even unrestricted) these problems are well understood: there are polynomial time, and even NC² algorithms. For copyless cost register automata we show that the two problems are PSpace-complete, where the difficulty is to show the lower bound.
Cite as

Filip Mazowiecki, Antoni Puch, and Daniel Smertnig. Pumping-Like Results for Copyless Cost Register Automata and Polynomially Ambiguous Weighted Automata. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 67:1-67:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mazowiecki_et_al:LIPIcs.STACS.2026.67,
  author =	{Mazowiecki, Filip and Puch, Antoni and Smertnig, Daniel},
  title =	{{Pumping-Like Results for Copyless Cost Register Automata and Polynomially Ambiguous Weighted Automata}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{67:1--67: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.67},
  URN =		{urn:nbn:de:0030-drops-255568},
  doi =		{10.4230/LIPIcs.STACS.2026.67},
  annote =	{Keywords: weighted automata, cost register automata, ambiguity, linear recurrence sequences, equivalence problem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.44
Minimal DFAs Witnessing Language Inequivalence

Authors: Jan Martens

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

Abstract
We study small witnesses for the inequivalence of two regular languages. A natural witness is a distinguishing word, e.g. a word in exactly one of the two languages. We propose using more succinct witnesses in the form of witnessing DFAs. A witnessing DFA recognizes a subset of one of the languages and contains at least one distinguishing word. In this way the DFA expresses behaviour contained in the first language but not the second. We show witnessing DFAs can be used to present more concise witnesses for the inequivalence of two regular languages. We show that the decision problem for the existence of a witnessing DFA of certain size is NP-complete in general, and in P in the special case of unary DFAs. Besides these computational aspects, we study structural properties of witnessing DFAs. Not all languages can be a minimal witness. It turns out that minimal witnesses are exactly the languages that are not decomposable in the union of languages with smaller state-complexity, the so-called prime languages as studied earlier by Kupferman and Mosheiff.
Cite as

Jan Martens. Minimal DFAs Witnessing Language Inequivalence. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 44:1-44:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{martens:LIPIcs.CSL.2026.44,
  author =	{Martens, Jan},
  title =	{{Minimal DFAs Witnessing Language Inequivalence}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{44:1--44:16},
  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.44},
  URN =		{urn:nbn:de:0030-drops-254691},
  doi =		{10.4230/LIPIcs.CSL.2026.44},
  annote =	{Keywords: Deterministic Finite Automata, Language Inequivalence, DFA decomposition, Prime languages}
}
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
DOI: 10.4230/LIPIcs.FSTTCS.2025.12
Explorability in Pushdown Automata

Authors: Ayaan Bedi and Karoliina Lehtinen

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

Abstract
We study explorability, a measure of nondeterminism in pushdown automata, which generalises history-determinism. An automaton is k-explorable if, while reading the input, it suffices to follow k concurrent runs, built step-by-step based only on the input seen so far, to construct an accepting one, if it exists. We show that the class of explorable PDAs lies strictly between history-deterministic and fully nondeterministic PDAs in terms of both expressiveness and succinctness. In fact increasing explorability induces an infinite hierarchy: each level k defines a strictly more expressive class than level k-1, yet the entire class remains less expressive than general nondeterministic PDAs. We then introduce a parameterized notion of explorability, where the number of runs may depend on input length, and show that exponential explorability precisely captures the context-free languages. Finally, we prove that explorable PDAs can be doubly exponentially more succinct than history-deterministic ones, and that the succinctness gap between deterministic and 2-explorable PDAs is not recursively enumerable. These results position explorability as a robust and operationally meaningful measure of nondeterminism for pushdown systems.
Cite as

Ayaan Bedi and Karoliina Lehtinen. Explorability in Pushdown Automata. 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. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bedi_et_al:LIPIcs.FSTTCS.2025.12,
  author =	{Bedi, Ayaan and Lehtinen, Karoliina},
  title =	{{Explorability in Pushdown Automata}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{12:1--12: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.12},
  URN =		{urn:nbn:de:0030-drops-250921},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.12},
  annote =	{Keywords: Pushdown automata, nondeterminism, explorability, history-determinism}
}
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.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.CONCUR.2025.32
Resolving Nondeterminism by Chance

Authors: Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke, and Di-De Yen

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

Abstract
History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomise and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is λ-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.
Cite as

Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke, and Di-De Yen. Resolving Nondeterminism by Chance. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{paul_et_al:LIPIcs.CONCUR.2025.32,
  author =	{Paul, Soumyajit and Purser, David and Schewe, Sven and Tang, Qiyi and Totzke, Patrick and Yen, Di-De},
  title =	{{Resolving Nondeterminism by Chance}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{32:1--32:22},
  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.32},
  URN =		{urn:nbn:de:0030-drops-239822},
  doi =		{10.4230/LIPIcs.CONCUR.2025.32},
  annote =	{Keywords: History-determinism, finite automata, probabilistic automata}
}
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}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.155
Approximate Problems for Finite Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny

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

Abstract
Finite (word) state transducers extend finite state automata by defining a binary relation over finite words, called rational relation. If the rational relation is the graph of a function, this function is said to be rational. The class of sequential functions is a strict subclass of rational functions, defined as the functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems and show they are decidable as well. This includes the approximate functionality problem, which asks whether given a rational relation (by a transducer), is it close to a rational function, and the approximate determinisation problem, which asks whether a given rational function is close to a sequential function. We prove decidability results for several classical distances, including Hamming and Levenshtein edit distance. Finally, we investigate the approximate uniformisation problem, which asks, given a rational relation R, whether there exists a sequential function that is close to some function uniformising R. As its exact version, we prove that this problem is undecidable.
Cite as

Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny. Approximate Problems for Finite Transducers. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 155:1-155:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2025.155,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and Madnani, Khushraj and Sunny, Saina},
  title =	{{Approximate Problems for Finite Transducers}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{155:1--155:19},
  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.155},
  URN =		{urn:nbn:de:0030-drops-235329},
  doi =		{10.4230/LIPIcs.ICALP.2025.155},
  annote =	{Keywords: Finite state transducers, Edit distance, Determinisation, Functionality}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.153
Reachability in 3-VASS Is Elementary

Authors: Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, and Łukasz Orlikowski

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

Abstract
The reachability problem in 3-dimensional vector addition systems with states (3-VASS) is known to be PSpace-hard, and to belong to Tower. We significantly narrow down the complexity gap by proving the problem to be solvable in doubly-exponential space. The result follows from a new upper bound on the length of the shortest path: if there is a path between two configurations of a 3-VASS then there is also one of at most triply-exponential length. We show it by introducing a novel technique of approximating the reachability sets of 2-VASS by small semi-linear sets.
Cite as

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, and Łukasz Orlikowski. Reachability in 3-VASS Is Elementary. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 153:1-153:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2025.153,
  author =	{Czerwi\'{n}ski, Wojciech and Jecker, Isma\"{e}l and Lasota, S{\l}awomir and Orlikowski, {\L}ukasz},
  title =	{{Reachability in 3-VASS Is Elementary}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{153:1--153: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.153},
  URN =		{urn:nbn:de:0030-drops-235307},
  doi =		{10.4230/LIPIcs.ICALP.2025.153},
  annote =	{Keywords: vector addition systems, Petri nets, reachability problem, dimension three, doubly exponential space, length of shortest path}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.68
Slightly Non-Linear Higher-Order Tree Transducers

Authors: Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni

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

Abstract
We investigate the tree-to-tree functions computed by "affine λ-transducers": tree automata whose memory consists of an affine λ-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati’s Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine (à la Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of Nguyễn and Pradic on "implicit automata" in an affine λ-calculus. We also prove that a more powerful variant, extended with preprocessing by an MSO relabeling and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet, Hoogeboom and Samwel’s invisible pebble tree transducers. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of Girard’s geometry of interaction, a semantics of linear logic. We work with ad-hoc specializations to λ-terms of low exponential depth of a tree-generating version of the IAM.
Cite as

Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni. Slightly Non-Linear Higher-Order Tree Transducers. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 68:1-68:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.STACS.2025.68,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Vanoni, Gabriele},
  title =	{{Slightly Non-Linear Higher-Order Tree Transducers}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{68:1--68:20},
  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.68},
  URN =		{urn:nbn:de:0030-drops-228934},
  doi =		{10.4230/LIPIcs.STACS.2025.68},
  annote =	{Keywords: Almost affine lambda-calculus, geometry of interaction, reversibility, tree transducers, tree-walking automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.35
New Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be F_d-hard for VASS of dimension 3d+2 (the complexity class F_d corresponds to the kth level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: F_d-hardness in dimension 2d+3. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: F_d-hardness in dimension d/2 + 6. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).
Cite as

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.35,
  author =	{Czerwi\'{n}ski, Wojciech and Jecker, Isma\"{e}l and Lasota, S{\l}awomir and Leroux, J\'{e}r\^{o}me and Orlikowski, {\L}ukasz},
  title =	{{New Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.35},
  URN =		{urn:nbn:de:0030-drops-194088},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.35},
  annote =	{Keywords: vector addition systems, reachability problem, pushdown vector addition system, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.18
History-Deterministic Vector Addition Systems

Authors: Sougata Bose, David Purser, and Patrick Totzke

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We consider history-determinism, a restricted form of non-determinism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words. History-determinism requires that the non-deterministic choices can be resolved on-the-fly; based on the past and without jeopardising acceptance of any possible continuation of the input word. Our results show that the history-deterministic (HD) VASS sit strictly between deterministic and non-deterministic VASS regardless of the number of counters. We compare the relative expressiveness of HD systems, and closure-properties of the induced language classes, with coverability and reachability semantics, and with and without ε-labelled transitions. Whereas in dimension 1, inclusion and regularity remain decidable, from dimension two onwards, HD-VASS with suitable resolver strategies, are essentially able to simulate 2-counter Minsky machines, leading to several undecidability results: It is undecidable whether a VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable.
Cite as

Sougata Bose, David Purser, and Patrick Totzke. History-Deterministic Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2023.18,
  author =	{Bose, Sougata and Purser, David and Totzke, Patrick},
  title =	{{History-Deterministic Vector Addition Systems}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.18},
  URN =		{urn:nbn:de:0030-drops-190120},
  doi =		{10.4230/LIPIcs.CONCUR.2023.18},
  annote =	{Keywords: Vector Addition Systems, History-determinism, Good-for Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.31
History-Deterministic Parikh Automata

Authors: Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure properties of deterministic automata.
Cite as

Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-Deterministic Parikh Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{erlich_et_al:LIPIcs.CONCUR.2023.31,
  author =	{Erlich, Enzo and Guha, Shibashis and Jecker, Isma\"{e}l and Lehtinen, Karoliina and Zimmermann, Martin},
  title =	{{History-Deterministic Parikh Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.31},
  URN =		{urn:nbn:de:0030-drops-190250},
  doi =		{10.4230/LIPIcs.CONCUR.2023.31},
  annote =	{Keywords: Parikh automata, History-determinism, Reversal-bounded Counter Machines}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.32
A Regular and Complete Notion of Delay for Streaming String Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.
Cite as

Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter. A Regular and Complete Notion of Delay for Streaming String Transducers. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.STACS.2023.32,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and L\"{o}ding, Christof and Winter, Sarah},
  title =	{{A Regular and Complete Notion of Delay for Streaming String Transducers}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{32:1--32:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.32},
  URN =		{urn:nbn:de:0030-drops-176843},
  doi =		{10.4230/LIPIcs.STACS.2023.32},
  annote =	{Keywords: Streaming string transducers, Delay, Origin}
}
  • Refine by Type
  • 30 Document/PDF
  • 11 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 9 2025
  • 4 2023
  • 4 2022
  • 4 2021
  • Show More...

  • Refine by Author
  • 17 Jecker, Ismaël
  • 4 Filiot, Emmanuel
  • 4 Lehtinen, Karoliina
  • 3 Guha, Shibashis
  • 3 Lasota, Sławomir
  • Show More...

  • Refine by Series/Journal
  • 30 LIPIcs

  • Refine by Classification
  • 9 Theory of computation → Formal languages and automata theory
  • 5 Theory of computation → Regular languages
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Solution concepts in game theory
  • 3 Theory of computation → Transducers
  • Show More...

  • Refine by Keyword
  • 3 History-determinism
  • 3 Transducers
  • 3 reachability problem
  • 3 vector addition systems
  • 2 Bidding games
  • 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