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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00144668" target="_blank" >RIV/00216224:14330/25:00144668 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2025.138" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.ICALP.2025.138</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2025.138" target="_blank" >10.4230/LIPIcs.ICALP.2025.138</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GA23-06963S" target="_blank" >GA23-06963S: VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

52nd International Colloquium on Automata, Languages, and Programming, ICALP 2025

ISBN

—

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

19

Strana od-do

„138:1“-„138:19“

Název nakladatele

Schloss Dagstuhl - Leibniz-Zentrum fur Informatik

Místo vydání

Neuvedeno

Místo konání akce

Aarhus, Dánsko

Datum konání akce

1. 1. 2025

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001740139600138