1-2-3-Go! Policy Synthesis for Parameterized Markov Decision
Processes via Decision-Tree Learning and Generalization

D 2025

1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

AZEEM, Muqsit; Debraj CHAKRABORTY; Sudeep KANAV; Jan KŘETÍNSKÝ; Mohammadsadegh MOHAGHEGHI et al.

Základní údaje

Originální název

1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

Autoři

AZEEM, Muqsit; Debraj CHAKRABORTY; Sudeep KANAV; Jan KŘETÍNSKÝ; Mohammadsadegh MOHAGHEGHI; Stefanie MOHR a Maximilian WEININGER

Vydání

Denver, USA, VMCAI 2025, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, od s. 97-120, 24 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-82702-0

ISSN

DOI

https://doi.org/10.1007/978-3-031-82703-7_5

EID Scopus

2-s2.0-85218471830

Klíčová slova anglicky

model checking; probabilistic verification; Markov decision process; policy synthesis

Štítky

core_B, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 26. 3. 2025 17:04, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

AZEEM, Muqsit; Debraj CHAKRABORTY; Sudeep KANAV; Jan KŘETÍNSKÝ; Mohammadsadegh MOHAGHEGHI; Stefanie MOHR a Maximilian WEININGER. 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization. In VMCAI 2025, 26th International Conference on Verification, Model Checking, and Abstract Interpretation. Denver, USA: Springer, 2025, s. 97-120. ISBN 978-3-031-82702-0. Dostupné z: https://doi.org/10.1007/978-3-031-82703-7_5.

@inproceedings{2484763,
   author = {Azeem, Muqsit and Chakraborty, Debraj and Kanav, Sudeep and Křetínský, Jan and Mohagheghi, Mohammadsadegh and Mohr, Stefanie and Weininger, Maximilian},
   address = {Denver, USA},
   booktitle = {VMCAI 2025, 26th International Conference on Verification, Model Checking, and Abstract Interpretation},
   doi = {https://doi.org/10.1007/978-3-031-82703-7_5},
   keywords = {model checking; probabilistic verification; Markov decision process; policy synthesis},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Denver, USA},
   isbn = {978-3-031-82702-0},
   pages = {97-120},
   publisher = {Springer},
   title = {1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization},
   year = {2025}
}

TY  - CONF
ID  - 2484763
AU  - Azeem, Muqsit - Chakraborty, Debraj - Kanav, Sudeep - Křetínský, Jan - Mohagheghi, Mohammadsadegh - Mohr, Stefanie - Weininger, Maximilian
PY  - 2025
TI  - 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
PB  - Springer
CY  - Denver, USA
SN  - 9783031827020
KW  - model checking
KW  - probabilistic verification
KW  - Markov decision process
KW  - policy synthesis
N2  - 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.
ER  -

AZEEM, Muqsit; Debraj CHAKRABORTY; Sudeep KANAV; Jan KŘETÍNSKÝ; Mohammadsadegh MOHAGHEGHI; Stefanie MOHR a Maximilian WEININGER. 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization. In \textit{VMCAI 2025, 26th International Conference on Verification, Model Checking, and Abstract Interpretation}. Denver, USA: Springer, 2025, s.~97-120. ISBN~978-3-031-82702-0. Dostupné z: https://doi.org/10.1007/978-3-031-82703-7\_{}5.

Přehled o publikaci