1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization

Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.

Download (ext.)

Conference Paper | Published | English

Scopus indexed
Author
Azeem, Muqsit; Chakraborty, Debraj; Kanav, Sudeep; Kretinsky, JanISTA ; Mohagheghi, Mohammadsadegh; Mohr, Stefanie; Weininger, MaximilianISTA
Department
Series Title
LNCS
Abstract
Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.
Publishing Year
Date Published
2025-01-23
Proceedings Title
26th International Conference on Verification, Model Checking, and Abstract Interpretation
Publisher
Springer Nature
Acknowledgement
This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE).
Volume
15530
Page
97-120
Conference
VMCAI: Verification, Model Checking, and Abstract Interpretation
Conference Location
Denver, CO, United States
Conference Date
2025-01-20 – 2025-01-21
ISSN
eISSN
IST-REx-ID

Cite this

Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: 26th International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 15530. Springer Nature; 2025:97-120. doi:10.1007/978-3-031-82703-7_5
Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., & Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In 26th International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. https://doi.org/10.1007/978-3-031-82703-7_5
Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In 26th International Conference on Verification, Model Checking, and Abstract Interpretation, 15530:97–120. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82703-7_5.
M. Azeem et al., “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Denver, CO, United States, 2025, vol. 15530, pp. 97–120.
Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.
Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” 26th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data ISTA Research Explorer

Sources

arXiv 2410.18293

Search this title in

Google Scholar
ISBN Search