Policies Grow on Trees: Model Checking Families of MDPs

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Policies Grow on Trees: Model Checking Families of MDPs

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Policies Grow on Trees: Model Checking Families of MDPs

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

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)<br>S - Specificky vyzkum na vysokych skolach

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

Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis

ISBN

978-3-031-78749-2

ISSN

—

e-ISSN

—

Počet stran výsledku

25

Strana od-do

51-75

Název nakladatele

Springer Verlag

Místo vydání

Cham

Místo konání akce

Kyoto

Datum konání akce

21. 10. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

001456088200003