Learning Algorithms for Verification of Markov Decision Processes

Kód výsledku v IS VaVaI

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

Výsledek na webu

<a href="https://theoretics.episciences.org/14694" target="_blank" >https://theoretics.episciences.org/14694</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.46298/theoretics.25.10" target="_blank" >10.46298/theoretics.25.10</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Learning Algorithms for Verification of Markov Decision Processes

Popis výsledku v původním jazyce

We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.

Název v anglickém jazyce

Learning Algorithms for Verification of Markov Decision Processes

Popis výsledku anglicky

We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.

Druh

J_SC - Článek v periodiku v databázi SCOPUS

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

V - Vyzkumna aktivita podporovana z jinych verejnych zdroju

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 periodika

TheoretiCS

ISSN

2751-4838

e-ISSN

2751-4838

Svazek periodika

4

Číslo periodika v rámci svazku

13268

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

82

Strana od-do

1-82

Kód UT WoS článku

—

EID výsledku v databázi Scopus

2-s2.0-105031089413