6 Search Results for "Chonev, Ventsislav"

Document
DOI: 10.4230/LIPIcs.STACS.2026.8
On the p-adic Skolem Problem

Authors: Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell

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

Abstract
The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many p-adic zeros. In this paper we consider the problem of determining whether a given LRS has a p-adic zero, as well as the corresponding function problem of computing exact representations of all p-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the p-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the p-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the p-adic Schanuel Conjecture.
Cite as

Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell. On the p-adic Skolem Problem. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacik_et_al:LIPIcs.STACS.2026.8,
  author =	{Bacik, Piotr and Ouaknine, Jo\"{e}l and Purser, David and Worrell, James},
  title =	{{On the p-adic Skolem Problem}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{8:1--8: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.8},
  URN =		{urn:nbn:de:0030-drops-254979},
  doi =		{10.4230/LIPIcs.STACS.2026.8},
  annote =	{Keywords: Skolem Problem, p-adic Schanuel Conjecture, Skolem Conjecture, Exponential Local-Global Principle, exponential polynomial}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.92
On Piecewise Affine Reachability with Bellman Operators

Authors: Anton Varonka and Kazuki Watanabe

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

Abstract
A piecewise affine map is one of the simplest mathematical objects exhibiting complex dynamics. The reachability problem of piecewise affine maps is as follows: Given two vectors s, t ∈ ℚ^d and a piecewise affine map f: ℚ^d → ℚ^d, is there n ∈ ℕ such that fⁿ(s) = t? Koiran, Cosnard, and Garzon show that the reachability problem of piecewise affine maps is undecidable even in dimension 2. Most of the recent progress has been focused on decision procedures for one-dimensional piecewise affine maps, where the reachability problem has been shown to be decidable for some subclasses. However, the general undecidability discouraged research into positive results in arbitrary dimension. In this work, we investigate a rich subclass of piecewise affine maps arising as Bellman operators of Markov decision processes (MDPs). We consider the reachability problem restricted to this subclass and examine its decidability in arbitrary dimensions. We establish that the reachability problem for Bellman operators is decidable in any dimension under either of the following conditions: (i) the target vector t is not the fixed point of the operator f; or (ii) the initial and target vectors s and t are comparable with respect to the componentwise order. Furthermore, we show that the reachability problem for two-dimensional Bellman operators is decidable for arbitrary s, t ∈ ℚ^d, in contrast to the known undecidability of reachability for general piecewise affine maps.
Cite as

Anton Varonka and Kazuki Watanabe. On Piecewise Affine Reachability with Bellman Operators. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 92:1-92:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{varonka_et_al:LIPIcs.MFCS.2025.92,
  author =	{Varonka, Anton and Watanabe, Kazuki},
  title =	{{On Piecewise Affine Reachability with Bellman Operators}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{92:1--92: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.92},
  URN =		{urn:nbn:de:0030-drops-241998},
  doi =		{10.4230/LIPIcs.MFCS.2025.92},
  annote =	{Keywords: piecewise affine map, reachability, value iteration, Markov decision process, Bellman operator}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.3
An Updated Survey of Bidding Games on Graphs (Invited Talk)

Authors: Guy Avni and Thomas A. Henzinger

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

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. An Updated Survey of Bidding Games on Graphs (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 3:1-3:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2022.3,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{An Updated Survey of Bidding Games on Graphs}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{3:1--3:6},
  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.3},
  URN =		{urn:nbn:de:0030-drops-168017},
  doi =		{10.4230/LIPIcs.MFCS.2022.3},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.2
A Survey of Bidding Games on Graphs (Invited Paper)

Authors: Guy Avni and Thomas A. Henzinger

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. A Survey of Bidding Games on Graphs (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2020.2,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{A Survey of Bidding Games on Graphs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.2},
  URN =		{urn:nbn:de:0030-drops-128147},
  doi =		{10.4230/LIPIcs.CONCUR.2020.2},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.21
Infinite-Duration Bidding Games

Authors: Guy Avni, Thomas A. Henzinger, and Ventsislav Chonev

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games [Lazarus1999,Lazarus2012]. There, a central question is the existence and computation of threshold budgets; namely, a value t \in [0,1] such that if \PO's budget exceeds t, he can win the game, and if \PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games.
Cite as

Guy Avni, Thomas A. Henzinger, and Ventsislav Chonev. Infinite-Duration Bidding Games. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2017.21,
  author =	{Avni, Guy and Henzinger, Thomas A. and Chonev, Ventsislav},
  title =	{{Infinite-Duration Bidding Games}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.21},
  URN =		{urn:nbn:de:0030-drops-77741},
  doi =		{10.4230/LIPIcs.CONCUR.2017.21},
  annote =	{Keywords: Bidding Games, Parity Games, Mean-Payoff Games, Richman Games}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.100
On the Skolem Problem for Continuous Linear Dynamical Systems

Authors: Ventsislav Chonev, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differential equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuoustime Markov chains. Decidability of the problem is currently open — indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel's Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that decidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.
Cite as

Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the Skolem Problem for Continuous Linear Dynamical Systems. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 100:1-100:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chonev_et_al:LIPIcs.ICALP.2016.100,
  author =	{Chonev, Ventsislav and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{On the Skolem Problem for Continuous Linear Dynamical Systems}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{100:1--100:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.100},
  URN =		{urn:nbn:de:0030-drops-62357},
  doi =		{10.4230/LIPIcs.ICALP.2016.100},
  annote =	{Keywords: differential equations, reachability, Baker’s Theorem, Schanuel’s Conjecture, semi-algebraic sets}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2022
  • 1 2020
  • 1 2017
  • Show More...

  • Refine by Author
  • 3 Avni, Guy
  • 3 Henzinger, Thomas A.
  • 2 Chonev, Ventsislav
  • 2 Ouaknine, Joël
  • 2 Worrell, James
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Solution concepts in game theory
  • 1 Mathematics of computing → Markov processes
  • 1 Theory of computation → Abstract machines
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Bidding games
  • 2 Richman bidding
  • 2 mean-payoff
  • 2 parity
  • 2 poorman bidding
  • 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