Policies Grow on Trees: Model Checking Families of MDPs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0193552" target="_blank" >RIV/00216305:26230/26:0193552 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-031-78750-8_3" target="_blank" >http://dx.doi.org/10.1007/978-3-031-78750-8_3</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-78750-8_3" target="_blank" >10.1007/978-3-031-78750-8_3</a>
Alternative languages
Result language
angličtina
Original language name
Policies Grow on Trees: Model Checking Families of MDPs
Original language description
Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a winning policy that achieves a desired specification. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. For a given family, we study synthesising (1) the subset of MDPs where a winning policy exists and (2) a preferably small number of winning policies that together cover this subset. We introduce policy trees that concisely capture the synthesis result. The key ingredient for synthesising policy trees is a recursive application of a game-based abstraction. We combine this abstraction with an efficient refinement procedure and a post-processing step. An extensive empirical evaluation demonstrates superior scalability of our approach compared to naive baselines. For one of the benchmarks, we find 246 winning policies covering 94 million MDPs. Our algorithm requires less than 30 min, whereas the naive baseline only covers 3.7% of MDPs in 24 h.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA23-06963S" target="_blank" >GA23-06963S: VESCAA: Verifiable and Efficient Synthesis of Controllers for Autonomous Agents</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis
ISBN
978-3-031-78749-2
ISSN
—
e-ISSN
—
Number of pages
25
Pages from-to
51-75
Publisher name
Springer Verlag
Place of publication
Cham
Event location
Kyoto
Event date
Oct 21, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001456088200003