Taming Infinity One Chunk at a Time: Concisely Represented
Strategies in One-Counter MDPs

D 2025

Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

AJDARÓW, Michal; James C A MAIN; Petr NOVOTNÝ a Mickael RANDOUR

Základní údaje

Originální název

Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Autoři

AJDARÓW, Michal; James C A MAIN; Petr NOVOTNÝ a Mickael RANDOUR

Vydání

Neuvedeno, 52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025, od s. "138:1"-"138:19", 19 s. 2025

Nakladatel

Schloss Dagstuhl - Leibniz-Zentrum fur Informatik

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00144668

Organizační jednotka

Fakulta informatiky

ISSN

Klíčová slova anglicky

one-counter Markov decision processes; computational complexity; strategy complexity

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 2. 6. 2026 17:22, Mgr. Petra Trembecká, Ph.D.

Anotace

V originále

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.

Návaznosti

GA23-06963S, projekt VaV

Název: VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty

Investor: Grantová agentura ČR, VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty

Citovat

AJDARÓW, Michal; James C A MAIN; Petr NOVOTNÝ a Mickael RANDOUR. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. Online. In 52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025. Neuvedeno: Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2025, s. "138:1"-"138:19", 19 s. ISSN 1868-8969. Dostupné z: https://doi.org/10.4230/LIPIcs.ICALP.2025.138.

@inproceedings{2562502,
   author = {Ajdarów, Michal and Main, James C A and Novotný, Petr and Randour, Mickael},
   address = {Neuvedeno},
   booktitle = {52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025},
   doi = {https://doi.org/10.4230/LIPIcs.ICALP.2025.138},
   keywords = {one-counter Markov decision processes; computational complexity; strategy complexity},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuvedeno},
   pages = {"138:1"-"138:19"},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fur Informatik},
   title = {Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs},
   year = {2025}
}

TY  - CONF
ID  - 2562502
AU  - Ajdarów, Michal - Main, James C A - Novotný, Petr - Randour, Mickael
PY  - 2025
TI  - Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs
PB  - Schloss Dagstuhl - Leibniz-Zentrum fur Informatik
CY  - Neuvedeno
KW  - one-counter Markov decision processes
KW  - computational complexity
KW  - strategy complexity
N2  - 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.
ER  -

AJDARÓW, Michal; James C A MAIN; Petr NOVOTNÝ a Mickael RANDOUR. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. Online. In \textit{52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025}. Neuvedeno: Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2025, s.~''138:1''-''138:19'', 19 s. ISSN~1868-8969. Dostupné z: https://doi.org/10.4230/LIPIcs.ICALP.2025.138.

Přehled o publikaci