This dataset is a repeatability evaluation package for the paper "Scalable control synthesis for stochastic systems via structural IMDP abstractions", Frederik Baymler Mathiesen, Sofie Haesaert, Luca Laurenti, 2024. The core idea is to verify properties about stochastic dynamical systems by finding a finite-state representation, called an abstraction, which may more easily be verified. The repeatability package includes experiments of abstracting different types of stochastic systems (additive linear/affine, polynomial, neural network dynamic models, Gaussian processes, and stochastically switched systems) to Interval Markov Decision Processes (IMDPs), orthogonally decoupled IMDPs (odIMDPs), and mixtures of odIMDPs. odIMDPs are a new abstract model proposed in the paper, where the ambiguity sets of transition probabilities are specified as products of (marginal) interval ambiguity sets.
The dataset includes all benchmark instances, a Docker-based command-line interface, plotting and table generating code, code for comparison against baseline tools IMPaCT and SySCoRe. For instructions on how to run the package, please consult the README.md file of the dataset.
ER -