Search Results

Documents authored by Kebis, Pavol

Document
DOI: 10.4230/LIPIcs.CONCUR.2026.12
PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance

Authors: Ali Asadi, Krishnendu Chatterjee, and Pavol Kebis

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability.
Cite as

Ali Asadi, Krishnendu Chatterjee, and Pavol Kebis. PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{asadi_et_al:LIPIcs.CONCUR.2026.12,
  author =	{Asadi, Ali and Chatterjee, Krishnendu and Kebis, Pavol},
  title =	{{PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.12},
  URN =		{urn:nbn:de:0030-drops-273432},
  doi =		{10.4230/LIPIcs.CONCUR.2026.12},
  annote =	{Keywords: formal methods, games and logic, logical aspects of AI, model checking}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2026.13
Generalized Bidding Games: Where Bidding and Stochastic Games Meet

Authors: Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, and Kaushik Mallik

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play. In this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP. Finally, we study a repair problem that asks whether bidding vertices can be assigned "owners" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete.
Cite as

Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, and Kaushik Mallik. Generalized Bidding Games: Where Bidding and Stochastic Games Meet. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{asadi_et_al:LIPIcs.CONCUR.2026.13,
  author =	{Asadi, Ali and Henzinger, Thomas A. and Kafshdar Goharshady, Ehsan and Kebis, Pavol and Mallik, Kaushik},
  title =	{{Generalized Bidding Games: Where Bidding and Stochastic Games Meet}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.13},
  URN =		{urn:nbn:de:0030-drops-273440},
  doi =		{10.4230/LIPIcs.CONCUR.2026.13},
  annote =	{Keywords: Bidding Games, Stochastic Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.21
Quantitative Language Automata

Authors: Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç

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

Abstract
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.
Cite as

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2025.21,
  author =	{Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Quantitative Language Automata}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{21:1--21:24},
  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.21},
  URN =		{urn:nbn:de:0030-drops-239718},
  doi =		{10.4230/LIPIcs.CONCUR.2025.21},
  annote =	{Keywords: Quantitative hyperproperties, quantitative automata, automata-based verification}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.144
On Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy Words

Authors: Pavol Kebis, Florian Luca, Joël Ouaknine, Andrew Scoones, and James Worrell

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We consider numbers of the form S_β(u): = ∑_{n=0}^∞ (u_n)/(βⁿ), where u = ⟨u_n⟩_{n=0}^∞ is an infinite word over a finite alphabet and β ∈ ℂ satisfies |β| > 1. Our main contribution is to present a combinatorial criterion on u, called echoing, that implies that S_β(u) is transcendental whenever β is algebraic. We show that every Sturmian word is echoing, as is the Tribonacci word, a leading example of an Arnoux-Rauzy word. We furthermore characterise ̅{ℚ}-linear independence of sets of the form {1, S_β(u₁),…,S_β(u_k)}, where u₁,…,u_k are Sturmian words having the same slope. Finally, we give an application of the above linear independence criterion to the theory of dynamical systems, showing that for a contracted rotation on the unit circle with algebraic slope, its limit set is either finite or consists exclusively of transcendental elements other than its endpoints 0 and 1. This confirms a conjecture of Bugeaud, Kim, Laurent, and Nogueira.
Cite as

Pavol Kebis, Florian Luca, Joël Ouaknine, Andrew Scoones, and James Worrell. On Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy Words. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 144:1-144:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kebis_et_al:LIPIcs.ICALP.2024.144,
  author =	{Kebis, Pavol and Luca, Florian and Ouaknine, Jo\"{e}l and Scoones, Andrew and Worrell, James},
  title =	{{On Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy Words}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{144:1--144:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.144},
  URN =		{urn:nbn:de:0030-drops-202873},
  doi =		{10.4230/LIPIcs.ICALP.2024.144},
  annote =	{Keywords: Transcendence, Subspace Theorem, Fibonacci Word, Tribonacci Word}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.129
Regular Methods for Operator Precedence Languages

Authors: Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç

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

Abstract
The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.
Cite as

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Regular Methods for Operator Precedence Languages. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 129:1-129:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.ICALP.2023.129,
  author =	{Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Regular Methods for Operator Precedence Languages}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{129:1--129:20},
  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.129},
  URN =		{urn:nbn:de:0030-drops-181814},
  doi =		{10.4230/LIPIcs.ICALP.2023.129},
  annote =	{Keywords: operator precedence automata, syntactic congruence, antichain algorithm}
}

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