7 Search Results for "Nieuwveld, Joris"

Document
DOI: 10.4230/LIPIcs.MFCS.2025.50
Lexicographic Transductions of Finite Words

Authors: Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier

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

Abstract
Regular transductions over finite words have linear input-to-output growth. This class of transductions enjoys many characterizations, such as transductions computable by two-way transducers as well as transductions definable in MSO (in the sense of Courcelle). Recently, regular transductions have been extended by Bojańczyk to polyregular transductions, which have polynomial growth, and are characterized by pebble transducers and MSO interpretations. Another class of interest is that of transductions defined by streaming string transducers or marble transducers, which have exponential growth and are incomparable with polyregular transductions. In this paper, we consider MSO set interpretations (MSOSI) over finite words, that were introduced by Colcombet and Loeding. MSOSI are a natural candidate for the class of "regular transductions with exponential growth", and are rather well behaved. However, MSOSI for now lacks two desirable properties that regular and polyregular transductions have. The first property is to have an automata description. This property is closely related to a second property, that of being regularity preserving, meaning preserving regular languages under inverse image. We first show that if MSOSI are (effectively) regularity preserving then any automatic ω-word has a decidable MSO theory, an almost 20 years old conjecture of Bárány. Our main contribution is the introduction of a class of transductions of exponential growth, which we call lexicographic transductions. We provide three different presentations for this class: first, as the closure of simple transductions (recognizable transductions) under a single operator called maplex; second, as a syntactic fragment of MSOSI (but the regular languages are given by automata instead of formulas); and third, we give an automaton based model called nested marble transducers, which generalize both marble transducers and pebble transducers. We show that this class enjoys many nice properties including being regularity preserving.
Cite as

Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier. Lexicographic Transductions of Finite Words. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.MFCS.2025.50,
  author =	{Filiot, Emmanuel and Lhote, Nathan and Reynier, Pierre-Alain},
  title =	{{Lexicographic Transductions of Finite Words}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{50:1--50: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.50},
  URN =		{urn:nbn:de:0030-drops-241572},
  doi =		{10.4230/LIPIcs.MFCS.2025.50},
  annote =	{Keywords: Transducers, Automata, MSO, Logical interpretations, Automatic structures}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.80
On Expansions of Monadic Second-Order Logic with Dynamical Predicates

Authors: Joris Nieuwveld and Joël Ouaknine

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

Abstract
Expansions of the monadic second-order (MSO) theory of the structure ⟨ℕ;<⟩ have been a fertile and active area of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ⟨ℕ;<,P⟩, where P ranges over a large class of unary "dynamical" predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.
Cite as

Joris Nieuwveld and Joël Ouaknine. On Expansions of Monadic Second-Order Logic with Dynamical Predicates. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 80:1-80:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nieuwveld_et_al:LIPIcs.MFCS.2025.80,
  author =	{Nieuwveld, Joris and Ouaknine, Jo\"{e}l},
  title =	{{On Expansions of Monadic Second-Order Logic with Dynamical Predicates}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{80:1--80: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.80},
  URN =		{urn:nbn:de:0030-drops-241879},
  doi =		{10.4230/LIPIcs.MFCS.2025.80},
  annote =	{Keywords: Monadic second-order logic, linear recurrence sequences, decidability, Baker’s theorem}
}
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.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
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.154
Submonoid Membership in n-Dimensional Lamplighter Groups and S-Unit Equations

Authors: Ruiwen Dong

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

Abstract
We show that Submonoid Membership is decidable in n-dimensional lamplighter groups (ℤ/pℤ) ≀ ℤⁿ for any prime p and integer n. More generally, we show decidability of Submonoid Membership in semidirect products of the form 𝒴 ⋊ ℤⁿ, where 𝒴 is any finitely presented module over the Laurent polynomial ring 𝔽_p[X₁^{±}, …, X_n^{±}]. Combined with a result of Shafrir (2024), this gives the first example of a group G and a finite index subgroup G̃ ≤ G, such that Submonoid Membership is decidable in G̃ but undecidable in G. To obtain our decidability result, we reduce Submonoid Membership in 𝒴 ⋊ ℤⁿ to solving S-unit equations over 𝔽_p[X₁^{±}, …, X_n^{±}]-modules. We show that the solution set of such equations is effectively p-automatic, extending a result of Adamczewski and Bell (2012). As an intermediate result, we also obtain that the solution set of the Knapsack Problem in 𝒴 ⋊ ℤⁿ is effectively p-automatic.
Cite as

Ruiwen Dong. Submonoid Membership in n-Dimensional Lamplighter Groups and S-Unit Equations. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 154:1-154:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dong:LIPIcs.ICALP.2025.154,
  author =	{Dong, Ruiwen},
  title =	{{Submonoid Membership in n-Dimensional Lamplighter Groups and S-Unit Equations}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{154:1--154: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.154},
  URN =		{urn:nbn:de:0030-drops-235316},
  doi =		{10.4230/LIPIcs.ICALP.2025.154},
  annote =	{Keywords: Submonoid Membership, lamplighter groups, S-unit equations, p-automatic sets, Knapsack in groups}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.130
Positivity Problems for Reversible Linear Recurrence Sequences

Authors: George Kenison, Joris Nieuwveld, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
It is a longstanding open problem whether there is an algorithm to decide the Positivity Problem for linear recurrence sequences (LRS) over the integers, namely whether given such a sequence, all its terms are non-negative. Decidability is known for LRS of order 5 or less, i.e., for those sequences in which every new term depends linearly on the previous five (or fewer) terms. For simple LRS (i.e., those sequences whose characteristic polynomials have no repeated roots), decidability of Positivity is known up to order 9. In this paper, we focus on the important subclass of reversible LRS, i.e., those integer LRS ⟨u_n⟩_{n=0}^∞ whose bi-infinite completion ⟨u_n⟩_{n=-∞}^∞ also takes exclusively integer values; a typical example is the classical Fibonacci (bi-)sequence ⟨ … , 5, -3, 2, -1, 1, 0, 1, 1, 2, 3, 5, … ⟩. Our main results are that Positivity is decidable for reversible LRS of order 11 or less, and for simple reversible LRS of order 17 or less.
Cite as

George Kenison, Joris Nieuwveld, Joël Ouaknine, and James Worrell. Positivity Problems for Reversible Linear Recurrence Sequences. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 130:1-130:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kenison_et_al:LIPIcs.ICALP.2023.130,
  author =	{Kenison, George and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Positivity Problems for Reversible Linear Recurrence Sequences}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{130:1--130:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.130},
  URN =		{urn:nbn:de:0030-drops-181821},
  doi =		{10.4230/LIPIcs.ICALP.2023.130},
  annote =	{Keywords: The Positivity Problem, Linear Recurrence Sequences, Verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.20
Skolem Meets Schanuel

Authors: Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the Skolem Problem remains open. The main contribution of this paper is an algorithm to solve the Skolem Problem for simple linear recurrence sequences (those with simple characteristic roots). Whenever the algorithm terminates, it produces a stand-alone certificate that its output is correct - a set of zeros together with a collection of witnesses that no further zeros exist. We give a proof that the algorithm always terminates assuming two classical number-theoretic conjectures: the Skolem Conjecture (also known as the Exponential Local-Global Principle) and the p-adic Schanuel Conjecture. Preliminary experiments with an implementation of this algorithm within the tool Skolem point to the practical applicability of this method.
Cite as

Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell. Skolem Meets Schanuel. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bilu_et_al:LIPIcs.MFCS.2022.20,
  author =	{Bilu, Yuri and Luca, Florian and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Purser, David and Worrell, James},
  title =	{{Skolem Meets Schanuel}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{20:1--20:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.20},
  URN =		{urn:nbn:de:0030-drops-168180},
  doi =		{10.4230/LIPIcs.MFCS.2022.20},
  annote =	{Keywords: Skolem Problem, Skolem Conjecture, Exponential Local-Global Principle, p-adic Schanuel Conjecture}
}
  • Refine by Type
  • 7 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 1 2023
  • 1 2022

  • Refine by Author
  • 3 Nieuwveld, Joris
  • 3 Ouaknine, Joël
  • 2 Purser, David
  • 2 Worrell, James
  • 1 Bilu, Yuri
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 2 Mathematics of computing → Discrete mathematics
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Logic and verification
  • 1 Computing methodologies → Algebraic algorithms
  • 1 Computing methodologies → Symbolic and algebraic algorithms
  • Show More...

  • Refine by Keyword
  • 1 Automata
  • 1 Automatic structures
  • 1 Baker’s theorem
  • 1 Exponential Local-Global Principle
  • 1 History-determinism
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact