Probabilistic Reachability for Stochastic Hybrid Systems
Alessandro Abate, S. Shankar Sastry, Maria Prandini, John Lygeros and Saurabh Amin
An important problem in hybrid systems theory is reachability analysis. In general terms, a reachability problem consists of evaluating whether a given system will reach a certain set during some time horizon, starting from a set of initial conditions. This problem arises, for instance, in connection with those safety verification problems where the unsafe conditions for the system can be characterized in terms of its state entering some unsafe set. In a stochastic setting, the safety verification problem can be formulated as that of estimating the probability that the state of the system remains outside the unsafe set for a given time horizon. If the evolution of the state can be influenced by some control input, the problem becomes that of verifying if it is possible to keep the state of the system outside the unsafe set with sufficiently high probability by selecting a suitable control input.
This project focuses on understanding the theoretical and computational issues associated with a new approach for reachability analysis of controlled stochastic hybrid systems. The technique is based on formulating reachability analysis as a stochastic optimal control problem, solved via dynamic programming. The significance of the problem can be extended from the concepts of reachability and safety to those of viability, controllability, attractivity and the like, thus extending the problem to a rather general "probabilistic verification" one.
A further focus of the project is the application of hybrid models in biology. In particular, a model for the production of an antibiotic as part of the stress response network for the bacterium Bacillus Subtilis will be described. The new model allows one to reinterpret and study the survival analysis for the single B-Subtilis cell as a probabilistic safety specification problem.