CODECHECK Certificate 2025-018
Paper details
Title: Scalable control synthesis for stochastic systems via structural IMDP abstractions
Authors: Frederik B. Mathiesen, Sofie Haesaert, Luca Laurenti
Abstract: Obtained from OpenAlex
This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.
CODECHECK details
Certificate identifier: 2025-018
Codechecker name: Niket Agrawal
Time of check: 2025-05-28 10:00:00
Repository: https://github.com/codecheckers/certificate-2025-018
Full certificate: https://doi.org/10.5281/zenodo.15630442
Summary:
Tables 2, 3, and 4, as well as Figures 4 and 5 from the manuscript, were successfully reproduced by following the instructions provided in the README file. Instructions were only available for reproducing these specific tables and figures. To avoid the lengthy execution time required to run the full experiments, the pre-computed results provided in the repository were used to generate the tables and figures, as recommended in the README.
https://codecheck.org.uk/ | codecheckers
© team@cdchck.science | Published under CC BY-SA 4.0
CODECHECK is a process for independent execution of computations underlying scholarly research articles.