StocHy: automated verification and synthesis of stochastic processes

TL;DR

Stochastic hybrid systems ($SHS$) enable rich modelling of systems with both discrete and continuous dynamics, but verification and synthesis are challenging due to undecidability and high dimensionality. StocHy provides a modular, high-performance toolchain that automates SHS modelling, simulation, and abstraction-based analysis by converting SHS into finite $MDP$ or $IMDP$ representations, using adaptive grid refinement and sparse-matrix techniques. The approach delivers formal verification and policy synthesis, with experiments demonstrating improved abstraction precision and scalability up to at least 12 continuous dimensions, as well as effective Monte Carlo simulations for statistical insight. These capabilities promote the practical adoption of SHS methods by non-experts and support engineers to verify, synthesize, and simulate complex stochastic systems at scale.

Abstract

StocHy is a software tool for the quantitative analysis of discrete-time stochastic hybrid systems (SHS). StocHy accepts a high-level description of stochastic models and constructs an equivalent SHS model. The tool allows to (i) simulate the SHS evolution over a given time horizon; and to automatically construct formal abstractions of the SHS. Abstractions are then employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy allows for modular modelling, and has separate simulation, verification and synthesis engines, which are implemented as independent libraries. This allows for libraries to be easily used and for extensions to be easily built. The tool is implemented in C++ and employs manipulations based on vector calculus, the use of sparse matrices, the symbolic construction of probabilistic kernels, and multi-threading. Experiments show StocHy's markedly improved performance when compared to existing abstraction-based approaches: in particular, StocHy beats state-of-the-art tools in terms of precision (abstraction error) and computational effort, and finally attains scalability to large-sized models (12 continuous dimensions). StocHy is available at www.gitlab.com/natchi92/StocHy.

Figures (6)

• Figure 1: Case study 1: Comparison of verification results for $\varphi_1$ when using faust$^2$ vs imdp.
• Figure 2: Case study 2: (a) Gridded domain together with a superimposed simulation of trajectory initialised at $(-0.5,-1)$ within $q_0$, under the synthesised optimal switching strategy $\pi^*$. Lower probabilities of satisfying $\varphi_2$ for mode $q_0$ (b) and for mode $q_1$ (c), as computed by $\mathsf{StocHy}$.
• Figure 3: Case study 4: (a) mc for the discrete modes of the $CO_2$ model and (b) input control signal.
• Figure 4: Case study 4: Simulation single traces for continuous variables (a) $x_1$, (b) $x_2$ and discrete modes (c) $q$. Histogram plots with respect to time step for (d) $x_1$, (e) $x_2$ and discrete modes (f) $q$.
• Figure :

Theorems & Definitions (6)

• definition thmcounterdefinition
• remark thmcounterremark
• remark thmcounterremark: Special instance
• remark thmcounterremark: Special instance
• definition thmcounterdefinition
• definition thmcounterdefinition