Combining analytical technique and randomized algorithm in safety verification of stochastic hybrid systems

In recent papers we have focused on the task of safety controller synthesis, that is, designing a controller that will take the system from any point within a compact set of initial states to a point inside a set of acceptable goal states, while never entering any state that is deemed unsafe. This method first finds a feedback controller that causes the system to be imbued with trajectory robustness, then finds open-loop reference signals that each safely drive the system from a subset of initial states to the goal state. In this paper we use piece wise affine system identification techniques to generate a feedback control law to replace the open-loop signals. This provides additional robustness to unexpected disturbances, in addition to reducing the memory required in the resulting controller, from storing many signals to a set of piece wise affine control laws.

We consider the problem of probabilistic safety verification for stochastic hybrid systems. In particular, we propose a method that combines two existing approaches, namely, analytical techniques and randomized algorithms. Analytical techniques, such as using stochastic approximate bisimulation, are able to handle non-deterministic initial states. However, their practical applicability is limited to relatively simple stochastic dynamics. On the other hand, randomized algorithms are able to handle more complex dynamics. However, it typically requires running a large number of simulations, and cannot be used for non-deterministic initial states. Our combined approach basically uses an analytical technique when the stochastic dynamics is simple, and switches to a randomized algorithm when the dynamics is nonlinear. The main idea is that by using the analytical technique, we can bound the gaps between the probability density functions corresponding to the family of non-deterministic initial states. This, in turn, enables randomized algorithms that provide upperand lower-bounds on the safety and unsafety probabilities. We illustrate our approach with an example from air traffic management. © 2014 American Automatic Control Council.