analiza aiqbench
This research advances formal verification methods for parametric Markov decision processes by introducing supermartingale certificates that handle general measurable state and action spaces. By transforming parametric models into non-parametric equivalents, the authors enable polynomial arithmetic algorithms for the first time in this continuous setting. The work provides a foundational step toward robust synthesis and verification techniques essential for complex AI systems operating under uncertainty.
Supermartingale Certificates for Parametric MDPs
arXiv:2609.12715v1 Announce Type: cross Abstract: We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.
Abstract:We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.
Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Systems and Control (eess.SY)
arXiv:2609.12715 [cs.LO]
(or arXiv:2609.12715v1 [cs.LO] for this version)
https://doi.org/10.48550/arXiv.2609.12715 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 224 cuvinte
Subiecte conexe
Certifying Almost-Sure Reachability in Unknown MDPs
arXiv · 15 oct. 2026
Runtime Monitoring of Supermartingale Certificates
arXiv · 15 oct. 2026
Rigorous characterization of continuous-variable quantum states via optical parametric amplifiers
arXiv · 21 iul. 2026
Consistent Model Chasing Is Minimax Optimal: The Exact Value of Scalar Adversarial Adaptive Control under Large Parametric Uncertainty
arXiv · 17 aug. 2026