Publication Details

Policies Grow on Trees: Model Checking Families of MDPs

ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; JUNGES, S. Policies Grow on Trees: Model Checking Families of MDPs. Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Cham: Springer Verlag, 2025. p. 51-75. ISBN: 978-3-031-78749-2.
Czech title
Verifikace rodin Markovských rozhodovacích procesů
Type
conference paper
Language
English
Authors
Keywords

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

Abstract

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.

Published
2025
Pages
51–75
Proceedings
Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference
22nd International Symposium on Automated Technology for Verification and Analysis, Kyoto, JP
ISBN
978-3-031-78749-2
Publisher
Springer Verlag
Place
Cham
DOI
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"
}
Back to top