RealySt: A C++ Tool for Optimizing Reachability Probabilities in Stochastic Hybrid Systems

Abstract

This paper presents the open-source C++ tool RealySt for effectively computing optimal time-bounded reachability probabilities for subclasses of hybrid automata extended with random clocks. The tool explicitly resolves the underlying nondeterminism and computes reachable state sets exactly. The error of the computed results solely stems from the multi-dimensional integration. The architecture of RealySt is extensible and allows to easily integrate other classes of hybrid automata extended by random clocks. RealySt relies on the HyPro library to perform flowpipe construction, and on GSL for multi-dimensional integration.

Supported by DFG project 471367371.

Appendices

Appendix A

Figure 1 illustrates an exemplary RAR with three locations that has two variables: random clock r and continuous variable x. The model contains initial nondeterminism in the valuation of x, which can be chosen from the interval [1, 3]. According to the syntax as presented in [11], the random clock r behaves as a stopwatch and has to be 0 initially.

The evolution of r is always either 1 or 0, since it can be active or $inactive$. In the given model, r is only active in location $\ell _0$. Hence, it evolves with rate 1 in $\ell _0$ and there is a stochastic transition from $\ell _0$ to $\ell _2$ modelling the expiration of the random delay. The continuous variable x, however, can evolve with a rate $\in [1,2]$ in $\ell _0$, which again models nondeterministic behavior. If it reaches a valuation of 4, location $\ell _0$ has to be left, either with the stochastic transition or with the transition from $\ell _0$ to $\ell _1$. In $\ell _1$, x is evolving with rate 1 and r is inactive and hence cannot expire anymore.

Appendix B

For completeness, we have included Fig. 3 illustrating the RAR model of the case study evaluated in Sect. 4. Note that the figure is taken from [11].

Fig. 3.

Car model with detours. Random clock c is active ($\dot{c}=1$) in the charging locations, d is active in locations driving and detour and r is active in location driving. The state of charge x is restricted to [0, 10] in all locations unless stated otherwise. No time is spent in location charge due to invariants not shown.

Appendix C

Figure 4 shows the computation times of the different model variants, where rectangular model variants are indicated with R and singular model variants with S. The computation times are separated for flowpipe construction (step 1), refinement (step 2 and 3), extraction of the sample domain (step 4) and the multi-dimensional integration (step 5). As the figure illustrates, RealySt is considerably quicker for all model variants in comparison to the computations from [11], and especially the flowpipe construction and integration perform much better.

Note that due for to the absence of peaks in the uniform distribution, VEGAS is unable to perform importance sampling. This particularly occurred during the variant singular AB for 2 detours, hence a larger number of integration samples had to be used in the computation. This resulted in a probability of 0.425 528 with $e_{\textit{stat}}$ = $1.203 \cdot 10^{-05}$.

Fig. 4.

Computation times for different models and number of detours with RealySt.