3 Search Results for "Hieronymi, Philipp"

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
DOI: 10.4230/LIPIcs.STACS.2025.37
On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

Authors: Jorge Gallego-Hernández and Alessio Mansutti

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

Abstract
This paper investigates ∃ℝ(ξ^ℤ), that is the extension of the existential theory of the reals by an additional unary predicate ξ^ℤ for the integer powers of a fixed computable real number ξ > 0. If all we have access to is a Turing machine computing ξ, it is not possible to decide whether an input formula from this theory is satisfiable. However, we show an algorithm to decide this problem when - ξ is known to be transcendental, or - ξ is a root of some given integer polynomial (that is, ξ is algebraic). In other words, knowing the algebraicity of ξ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that ξ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ∃ℝ(ξ^ℤ) is - in ExpSpace if ξ is an algebraic number, and - in 3Exp if ξ is a logarithm of an algebraic number, Euler’s e, or the number π, among others. To establish our results, we first observe that the satisfiability problem of ∃ℝ(ξ^ℤ) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over ξ^ℤ. We then prove that these instances have a small witness property: only finitely many integer powers of ξ must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers. As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS, 2023]: when the base of the entropic risk is e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in Exp.
Cite as

Jorge Gallego-Hernández and Alessio Mansutti. On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gallegohernandez_et_al:LIPIcs.STACS.2025.37,
  author =	{Gallego-Hern\'{a}ndez, Jorge and Mansutti, Alessio},
  title =	{{On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{37:1--37:18},
  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.37},
  URN =		{urn:nbn:de:0030-drops-228635},
  doi =		{10.4230/LIPIcs.STACS.2025.37},
  annote =	{Keywords: Theory of the reals with exponentiation, decision procedures, computability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.24
Decidability for Sturmian Words

Authors: Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We show that the first-order theory of Sturmian words over Presburger arithmetic is decidable. Using a general adder recognizing addition in Ostrowski numeration systems by Baranwal, Schaeffer and Shallit, we prove that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly ω-automatic, and then deduce the decidability of the theory of the class of such structures. Using an implementation of this decision algorithm called Pecan, we automatically reprove classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words.
Cite as

Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit. Decidability for Sturmian Words. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hieronymi_et_al:LIPIcs.CSL.2022.24,
  author =	{Hieronymi, Philipp and Ma, Dun and Oei, Reed and Schaeffer, Luke and Schulz, Christian and Shallit, Jeffrey},
  title =	{{Decidability for Sturmian Words}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.24},
  URN =		{urn:nbn:de:0030-drops-157440},
  doi =		{10.4230/LIPIcs.CSL.2022.24},
  annote =	{Keywords: Decidability, Sturmian words, Ostrowski numeration systems, Automated theorem proving}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2022

  • Refine by Author
  • 1 Dong, Ruiwen
  • 1 Gallego-Hernández, Jorge
  • 1 Hieronymi, Philipp
  • 1 Ma, Dun
  • 1 Mansutti, Alessio
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Computing methodologies → Symbolic and algebraic algorithms
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Automated theorem proving
  • 1 Decidability
  • 1 Knapsack in groups
  • 1 Ostrowski numeration systems
  • 1 S-unit equations
  • 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