Detail publikace

Policies Grow on Trees: Model Checking Families of MDPs

ANDRIUSHCHENKO, R. ČEŠKA, M. MACÁK, F. JUNGES, S.

Originální název

Policies Grow on Trees: Model Checking Families of MDPs

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

Markov decision processes, robust and winning policies, game-based abstraction

Autoři

ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; JUNGES, S.

Vydáno

7. 2. 2025

Nakladatel

Springer Verlag

Místo

Cham

ISBN

978-3-031-78749-2

Kniha

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

Edice

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Strany od

51

Strany do

75

Strany počet

13

BibTex

@inproceedings{BUT193552,
  author="ANDRIUSHCHENKO, R. and ČEŠKA, M. and MACÁK, F. and JUNGES, S.",
  title="Policies Grow on Trees: Model Checking Families of MDPs",
  booktitle="Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis",
  year="2025",
  series="Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
  pages="51--75",
  publisher="Springer Verlag",
  address="Cham",
  doi="10.1007/978-3-031-78750-8\{_}3",
  isbn="978-3-031-78749-2"
}