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 minutes, whereas the naive baseline only covers 3.7% of MDPs in 24 hours.
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Technical University of Munich（慕尼黑工业大学）；Vali-e-Asr University of Rafsanjan（拉夫桑贾德瓦利阿斯尔大学）；Masaryk University（马萨里克大学）；Institute of Science and Technology（科学技术研究院）
Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
Nanyang Technological University, Singapore（新加坡南洋理工大学）；Tata Institute of Fundamental Research, Mumbai, India（印度孟买印度理工学院基础研究所以）；Université Libre de Bruxelles, Brussels, Belgium（比利时布鲁塞尔自由大学）；IITB Trust Lab, Department of CSE, IIT Bombay, Mumbai, India（印度孟买印度理工学院 Bombay 电子与计算机科学系信托实验室）
