22 Search Results for "Kretínský, Jan"

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
DOI: 10.4230/LIPIcs.MFCS.2025.30
Finding Equilibria: Simpler for Pessimists, Simplest for Optimists

Authors: Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini

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

Abstract
We consider equilibria in multiplayer stochastic graph games with terminal-node rewards. In such games, Nash equilibria are defined assuming that each player seeks to maximise their expected payoff, ignoring their aversion or tolerance to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected payoff is replaced by a risk measure. A classical risk measure in the literature is the entropic risk measure, where each player has a real valued parameter capturing their risk-averseness. We introduce the extreme risk measure, which corresponds to extreme cases of entropic risk measure, where players are either extreme optimists or extreme pessimists. Under extreme risk measure, every player is an extremist: an extreme optimist perceives their reward as the maximum payoff that can be achieved with positive probability, while an extreme pessimist expects the minimum payoff achievable with positive probability. We argue that the extreme risk measure, especially in multi-player graph based settings, is particularly relevant as they can model several real life instances such as interactions between secure systems and potential security threats, or distributed controls for safety critical systems. We prove that RSEs defined with the extreme risk measure are guaranteed to exist when all rewards are non-negative. Furthermore, we prove that the problem of deciding whether a given game contains an RSE that generates risk measures within specified intervals is decidable and NP-complete for our extreme risk measure, and even PTIME-complete when all players are extreme optimists, while that same problem is undecidable using the entropic risk measure or even the classical expected payoff. This establishes, to our knowledge, the first decidable fragment for equilibria in simple stochastic games without restrictions on strategy types or number of players.
Cite as

Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini. Finding Equilibria: Simpler for Pessimists, Simplest for Optimists. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.MFCS.2025.30,
  author =	{Brice, L\'{e}onard and Henzinger, Thomas A. and Thejaswini, K. S.},
  title =	{{Finding Equilibria: Simpler for Pessimists, Simplest for Optimists}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-241371},
  doi =		{10.4230/LIPIcs.MFCS.2025.30},
  annote =	{Keywords: Nash equilibria, stochastic games, graph games, risk-sensitive equilibria}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.57
Resolving Nondeterminism with Randomness

Authors: Thomas A. Henzinger, Keya Prakash, and K. S. Thejaswini

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

Abstract
We define and study classes of ω-regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called adversarial resolvability, the input word is constructed letter-by-letter by an adversary, dependent on the resolver’s previous decisions. In the second setting, called stochastic resolvability, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability 1. The class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata. We show that the new automata classes offer interesting trade-offs between succinctness, expressivity, and computational complexity, providing a fine gradation between deterministic automata and nondeterministic automata.
Cite as

Thomas A. Henzinger, Keya Prakash, and K. S. Thejaswini. Resolving Nondeterminism with Randomness. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 57:1-57:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.MFCS.2025.57,
  author =	{Henzinger, Thomas A. and Prakash, Keya and Thejaswini, K. S.},
  title =	{{Resolving Nondeterminism with Randomness}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{57:1--57: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.57},
  URN =		{urn:nbn:de:0030-drops-241645},
  doi =		{10.4230/LIPIcs.MFCS.2025.57},
  annote =	{Keywords: \omega-regular languages, History determinism, Stochastic strategies}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.9
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games

Authors: Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou

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

Abstract
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. This paper introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. Furthermore, we demonstrate that under binary encoding this reduction is polynomial, thereby directly corroborating the known NP ∩ coNP complexity of SPGs and providing new understanding in the relationship between parity and reachability objectives in turn-based stochastic games.
Cite as

Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou. A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.CONCUR.2025.9,
  author =	{Berthon, Rapha\"{e}l and Katoen, Joost-Pieter and Zhou, Zihan},
  title =	{{A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{9:1--9:21},
  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.9},
  URN =		{urn:nbn:de:0030-drops-239595},
  doi =		{10.4230/LIPIcs.CONCUR.2025.9},
  annote =	{Keywords: stochastic games, parity, reduction}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.12
Cancellative Convex Semilattices

Authors: Ana Sokolova and Harald Woracek

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad. A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations). We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).
Cite as

Ana Sokolova and Harald Woracek. Cancellative Convex Semilattices. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sokolova_et_al:LIPIcs.CALCO.2025.12,
  author =	{Sokolova, Ana and Woracek, Harald},
  title =	{{Cancellative Convex Semilattices}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.12},
  URN =		{urn:nbn:de:0030-drops-235714},
  doi =		{10.4230/LIPIcs.CALCO.2025.12},
  annote =	{Keywords: convex semilattice, cancellativity, Riesz space}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.138
Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Authors: Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour

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

Abstract
Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter MDPs (OC-MDPs). They extend finite MDPs via an associated counter taking natural values, thus inducing an infinite MDP over the set of configurations (current state and counter value). We consider two characteristic objectives: reaching a target state (state-reachability), and reaching a target state with counter value zero (selective termination). The synthesis problem for the latter is not known to be decidable and connected to major open problems in number theory. Furthermore, even seemingly simple strategies (e.g., memoryless ones) in OC-MDPs might be impossible to build in practice (due to the underlying infinite configuration space): we need finite, and preferably small, representations. To overcome these obstacles, we introduce two natural classes of concisely represented strategies based on a (possibly infinite) partition of counter values in intervals. For both classes, and both objectives, we study the verification problem (does a given strategy ensure a high enough probability for the objective?), and two synthesis problems (does there exist such a strategy?): one where the interval partition is fixed as input, and one where it is only parameterized. We develop a generic approach based on a compression of the induced infinite MDP that yields decidability in all cases, with all complexities within PSPACE.
Cite as

Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 138:1-138:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.ICALP.2025.138,
  author =	{Ajdar\'{o}w, Michal and Main, James C. A. and Novotn\'{y}, Petr and Randour, Mickael},
  title =	{{Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{138:1--138: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.138},
  URN =		{urn:nbn:de:0030-drops-235157},
  doi =		{10.4230/LIPIcs.ICALP.2025.138},
  annote =	{Keywords: one-counter Markov decision processes, randomised strategies, termination, reachability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.145
Reducing Stochastic Games to Semidefinite Programming

Authors: Manuel Bodirsky, Georg Loho, and Mateusz Skomra

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

Abstract
We present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon’s simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming.
Cite as

Manuel Bodirsky, Georg Loho, and Mateusz Skomra. Reducing Stochastic Games to Semidefinite Programming. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 145:1-145:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.ICALP.2025.145,
  author =	{Bodirsky, Manuel and Loho, Georg and Skomra, Mateusz},
  title =	{{Reducing Stochastic Games to Semidefinite Programming}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{145:1--145:15},
  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.145},
  URN =		{urn:nbn:de:0030-drops-235224},
  doi =		{10.4230/LIPIcs.ICALP.2025.145},
  annote =	{Keywords: Mean-payoff games, stochastic games, semidefinite programming, max-average constraints, max-atom problem}
}
Document
DOI: 10.4230/DagRep.14.9.1
Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy (Dagstuhl Seminar 24361)

Authors: Nils Jansen, Mykel Kochenderfer, Jan Kretinsky, Jana Tumova, and Maris Galesloot

Published in: Dagstuhl Reports, Volume 14, Issue 9 (2025)

Abstract
This report documents the program and outcomes of Dagstuhl Seminar 24361, "Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy." AI is a disruptive force with growing applications in everyday life. Therefore, AI systems require serious safety, correctness, and reliability considerations. Recently, the field of safety in AI has triggered a vast amount of research. This seminar brought together experts from the fields of artificial intelligence, formal methods, and robotics. Via a diverse program with ample space for open yet guided discussion, a common understanding of problems was developed. Consequently, the seminar provided a means to identify key challenges and open problems in the research areas that underpin reliable autonomy.
Cite as

Nils Jansen, Mykel Kochenderfer, Jan Kretinsky, Jana Tumova, and Maris Galesloot. Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy (Dagstuhl Seminar 24361). In Dagstuhl Reports, Volume 14, Issue 9, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{jansen_et_al:DagRep.14.9.1,
  author =	{Jansen, Nils and Kochenderfer, Mykel and Kretinsky, Jan and Tumova, Jana and Galesloot, Maris},
  title =	{{Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy (Dagstuhl Seminar 24361)}},
  pages =	{1--21},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{14},
  number =	{9},
  editor =	{Jansen, Nils and Kochenderfer, Mykel and Kretinsky, Jan and Tumova, Jana and Galesloot, Maris},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.9.1},
  URN =		{urn:nbn:de:0030-drops-226100},
  doi =		{10.4230/DagRep.14.9.1},
  annote =	{Keywords: artificial intelligence, autonomous systems, formal verification, machine learning, robotics}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.8
Enumeration of Minimal Hitting Sets Parameterized by Treewidth

Authors: Batya Kenig and Dan Shlomo Mizrahi

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
Enumerating the minimal hitting sets of a hypergraph is a problem which arises in many data management applications that include constraint mining, discovering unique column combinations, and enumerating database repairs. Previously, Eiter et al. [Thomas Eiter et al., 2003] showed that the minimal hitting sets of an n-vertex hypergraph, with treewidth w, can be enumerated with delay O^*(n^w) (ignoring polynomial factors), with space requirements that scale with the output size. We improve this to fixed-parameter-linear delay, following an FPT preprocessing phase. The memory consumption of our algorithm is exponential with respect to the treewidth of the hypergraph.
Cite as

Batya Kenig and Dan Shlomo Mizrahi. Enumeration of Minimal Hitting Sets Parameterized by Treewidth. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kenig_et_al:LIPIcs.ICDT.2025.8,
  author =	{Kenig, Batya and Mizrahi, Dan Shlomo},
  title =	{{Enumeration of Minimal Hitting Sets Parameterized by Treewidth}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.8},
  URN =		{urn:nbn:de:0030-drops-229498},
  doi =		{10.4230/LIPIcs.ICDT.2025.8},
  annote =	{Keywords: Enumeration, Hitting sets}
}
Document
DOI: 10.4230/DagRep.14.6.1
Stochastic Games (Dagstuhl Seminar 24231)

Authors: Nathanaël Fijalkow, Jan Kretinsky, Ann Nowé, and Gabriel Bathie

Published in: Dagstuhl Reports, Volume 14, Issue 6 (2024)

Abstract
The Dagstuhl Seminar on Stochastic Games brought together leading researchers and practitioners in the field to discuss recent advances, challenges, and future directions. The seminar featured a series of tutorials, invited talks, and contributed talks, which provided a comprehensive overview of the latest developments in Markov decision processes, reinforcement learning, and stochastic game theory. The seminar fostered lively discussions during open problem sessions and working groups, culminating in a collaborative exploration of open questions and potential research directions.
Cite as

Nathanaël Fijalkow, Jan Kretinsky, Ann Nowé, and Gabriel Bathie. Stochastic Games (Dagstuhl Seminar 24231). In Dagstuhl Reports, Volume 14, Issue 6, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fijalkow_et_al:DagRep.14.6.1,
  author =	{Fijalkow, Nathana\"{e}l and Kretinsky, Jan and Now\'{e}, Ann and Bathie, Gabriel},
  title =	{{Stochastic Games (Dagstuhl Seminar 24231)}},
  pages =	{1--18},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{6},
  editor =	{Fijalkow, Nathana\"{e}l and Kretinsky, Jan and Now\'{e}, Ann and Bathie, Gabriel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.6.1},
  URN =		{urn:nbn:de:0030-drops-227344},
  doi =		{10.4230/DagRep.14.6.1},
  annote =	{Keywords: Algorithmic Game Theory, Algorithms, Optimisation, Reinforcement Learning, Stochastic Games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.29
Algorithms and Hardness Results for Computing Cores of Markov Chains

Authors: Ali Ahmadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi, and Ðorđe Žikelić

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Given a Markov chain M = (V, v_0, δ), with state space V and a starting state v_0, and a probability threshold ε, an ε-core is a subset C of states that is left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach (V\C)] ≤ ε. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ε-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ε-core of a given size is NP-complete. This solves an open problem posed in [Jan Kretínský and Tobias Meggendorfer, 2020]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset.
Cite as

Ali Ahmadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi, and Ðorđe Žikelić. Algorithms and Hardness Results for Computing Cores of Markov Chains. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ahmadi_et_al:LIPIcs.FSTTCS.2022.29,
  author =	{Ahmadi, Ali and Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Meggendorfer, Tobias and Safavi, Roodabeh and \v{Z}ikeli\'{c}, Ðor{\d}e},
  title =	{{Algorithms and Hardness Results for Computing Cores of Markov Chains}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.29},
  URN =		{urn:nbn:de:0030-drops-174216},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.29},
  annote =	{Keywords: Markov Chains, Cores, Complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.11
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes

Authors: Kush Grover, Jan Křetínský, Tobias Meggendorfer, and Maximilian Weininger

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation. As this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the "boundary" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations. We present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees.
Cite as

Kush Grover, Jan Křetínský, Tobias Meggendorfer, and Maximilian Weininger. Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{grover_et_al:LIPIcs.CONCUR.2022.11,
  author =	{Grover, Kush and K\v{r}et{\'\i}nsk\'{y}, Jan and Meggendorfer, Tobias and Weininger, Maximilian},
  title =	{{Anytime Guarantees for Reachability in Uncountable Markov Decision Processes}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.11},
  URN =		{urn:nbn:de:0030-drops-170743},
  doi =		{10.4230/LIPIcs.CONCUR.2022.11},
  annote =	{Keywords: Uncountable system, Markov decision process, discrete-time Markov control process, probabilistic verification, anytime guarantee}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.5
Enforcing ω-Regular Properties in Markov Chains by Restarting

Authors: Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts.
Cite as

Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2021.5,
  author =	{Esparza, Javier and Kiefer, Stefan and K\v{r}et{\'\i}nsk\'{y}, Jan and Weininger, Maximilian},
  title =	{{Enforcing \omega-Regular Properties in Markov Chains by Restarting}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.5},
  URN =		{urn:nbn:de:0030-drops-143824},
  doi =		{10.4230/LIPIcs.CONCUR.2021.5},
  annote =	{Keywords: Markov chains, omega-regular properties, runtime enforcement}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.5
Of Cores: A Partial-Exploration Framework for Markov Decision Processes

Authors: Jan Křetínský and Tobias Meggendorfer

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We introduce a framework for approximate analysis of Markov decision processes (MDP) with bounded-, unbounded-, and infinite-horizon properties. The main idea is to identify a "core" of an MDP, i.e., a subsystem where we provably remain with high probability, and to avoid computation on the less relevant rest of the state space. Although we identify the core using simulations and statistical techniques, it allows for rigorous error bounds in the analysis. Consequently, we obtain efficient analysis algorithms based on partial exploration for various settings, including the challenging case of strongly connected systems.
Cite as

Jan Křetínský and Tobias Meggendorfer. Of Cores: A Partial-Exploration Framework for Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2019.5,
  author =	{K\v{r}et{\'\i}nsk\'{y}, Jan and Meggendorfer, Tobias},
  title =	{{Of Cores: A Partial-Exploration Framework for Markov Decision Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.5},
  URN =		{urn:nbn:de:0030-drops-109076},
  doi =		{10.4230/LIPIcs.CONCUR.2019.5},
  annote =	{Keywords: Markov Decision Processes, Reachability, Approximation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.8
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints

Authors: Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in MDPs consisting of a single end component, two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use. (i) For all epsilon and gamma we can construct an online-learning finite-memory strategy that almost-surely satisfies the parity objective and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. (ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. We extend the above results to MDPs consisting of more than one end component in a natural way. Finally, we show that the aforementioned guarantees are tight, i.e. there are MDPs for which stronger combinations of the guarantees cannot be ensured.
Cite as

Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.8,
  author =	{Kret{\'\i}nsk\'{y}, Jan and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.8},
  URN =		{urn:nbn:de:0030-drops-95468},
  doi =		{10.4230/LIPIcs.CONCUR.2018.8},
  annote =	{Keywords: Markov decision processes, Reinforcement learning, Beyond worst case}
}
  • Refine by Type
  • 22 Document/PDF
  • 10 Document/HTML

  • Refine by Publication Year
  • 9 2025
  • 1 2024
  • 2 2022
  • 1 2021
  • 1 2019
  • Show More...

  • Refine by Author
  • 8 Kretinsky, Jan
  • 3 Henzinger, Thomas A.
  • 3 Křetínský, Jan
  • 3 Meggendorfer, Tobias
  • 2 Brazdil, Tomas
  • Show More...

  • Refine by Series/Journal
  • 18 LIPIcs
  • 1 OASIcs
  • 3 DagRep

  • Refine by Classification
  • 4 Theory of computation → Probabilistic computation
  • 3 Theory of computation → Logic and verification
  • 2 Mathematics of computing → Markov processes
  • 2 Theory of computation → Verification by model checking
  • 1 Computing methodologies → Artificial intelligence
  • Show More...

  • Refine by Keyword
  • 4 stochastic games
  • 2 Markov decision process
  • 2 artificial intelligence
  • 2 formal verification
  • 2 machine learning
  • 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