Learning Algorithms for Verification of Markov Decision
Processes

J 2025

Learning Algorithms for Verification of Markov Decision Processes

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ et al.

Základní údaje

Originální název

Learning Algorithms for Verification of Markov Decision Processes

Autoři

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ; Marta KWIATKOWSKA; Tobias MEGGENDORFER; David PARKER a Mateusz UJMA

Vydání

TheoretiCS, 2025, 2751-4838

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

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í

Odkazy

URL

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00142513

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.46298/theoretics.25.10

EID Scopus

2-s2.0-105031089413

Klíčová slova anglicky

Electrical Engineering and Systems Sciences-Systems and Control; Computer Science-Artificial Intelligence; Computer Science-Logic in Computer Science

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 4. 2026 11:13, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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ávaznosti

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ; Marta KWIATKOWSKA; Tobias MEGGENDORFER; David PARKER a Mateusz UJMA. Learning Algorithms for Verification of Markov Decision Processes. TheoretiCS. 2025, roč. 4, č. 13268, s. 1-82. ISSN 2751-4838. Dostupné z: https://doi.org/10.46298/theoretics.25.10.

@article{2531337,
   author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelík, Martin and Forejt, Vojtěch and Křetínský, Jan and Kwiatkowska, Marta and Meggendorfer, Tobias and Parker, David and Ujma, Mateusz},
   article_number = {13268},
   doi = {https://doi.org/10.46298/theoretics.25.10},
   keywords = {Electrical Engineering and Systems Sciences-Systems and Control; Computer Science-Artificial Intelligence; Computer Science-Logic in Computer Science},
   language = {eng},
   issn = {2751-4838},
   journal = {TheoretiCS},
   title = {Learning Algorithms for Verification of Markov Decision Processes},
   url = {https://theoretics.episciences.org/14694},
   volume = {4},
   year = {2025}
}

TY  - JOUR
ID  - 2531337
AU  - Brázdil, Tomáš - Chatterjee, Krishnendu - Chmelík, Martin - Forejt, Vojtěch - Křetínský, Jan - Kwiatkowska, Marta - Meggendorfer, Tobias - Parker, David - Ujma, Mateusz
PY  - 2025
TI  - Learning Algorithms for Verification of Markov Decision Processes
JF  - TheoretiCS
VL  - 4
IS  - 13268
SP  - 1-82
EP  - 1-82
SN  - 27514838
KW  - Electrical Engineering and Systems Sciences-Systems and Control
KW  - Computer Science-Artificial Intelligence
KW  - Computer Science-Logic in Computer Science
UR  - https://theoretics.episciences.org/14694
N2  - 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.
ER  -

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ; Marta KWIATKOWSKA; Tobias MEGGENDORFER; David PARKER a Mateusz UJMA. Learning Algorithms for Verification of Markov Decision Processes. \textit{TheoretiCS}. 2025, roč.~4, č.~13268, s.~1-82. ISSN~2751-4838. Dostupné z: https://doi.org/10.46298/theoretics.25.10.

Přehled o publikaci