Project Description:

An important problem in hybrid systems theory is reachability analysis. In general terms, a reachability problem consists in evaluating if 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: if the state of the system cannot enter the unsafe set, then the system is declared to be safe. 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 (both continuous and discrete) 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.
The study has been directed towards gaining a deeper understanding of the theoretical and computational issues associated with the reachability analysis of controlled stochastic hybrid systems. The approach is based on formulating reachability analysis as a stochastic optimal control problem. The maximal probability of remaining in a safe set for a certain time horizon can then be computed by 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. From a more practical standpoint, research has been directed toward embedding some ``performance specifications'' into the problem definition, in order to address some ``probabilistic regulation'' tasks and other control-oriented objectives. The computational aspects of the proposed approach have been constantly under focus, leveraging on the flexibility of the dynamic programming approach (and approximate, distributed, convex versions thereof).

An updated list of publications:

A. Abate, M. Prandini, J. Lygeros, and S. Sastry,
"Probabilistic Reachability and Safety for Controlled Discrete Time Stochastic Hybrid Systems," accepted in Automatica, 2008.
[pdf][BibTeX]

A. Abate,
"Probabilistic Reachability for Stochastic Hybrid Systems: Theory, Computations, and Applications," PhD Thesis, Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, 2007.
[pdf][BibTeX]

A. Abate, S. Amin, M. Prandini, J. Lygeros, and S. Sastry,
"Computational Approaches to Reachability Analysis of Stochastic Hybrid Systems", In A. Bemporad, A. Bicchi, and G. Buttazzo, eds.: Hybrid Systems: Computation and Control. Lecture Notes in Computer Science 4416, pp. 4-17, Springer Verlag.
Presented at the 10th International Workshop on Hybrid Systems, Pisa (IT), April 2007.
[pdf][BibTeX]

A. Abate, S. Amin, M. Prandini, J. Lygeros, and S. Sastry,
"Probabilistic Reachability for Safety and Regulation of Controlled Discrete-Time Stochastic Hybrid Systems", in the Proceedings of the 45th the Decision and Control Conference, San Diego, CA, Dec. 2006.
[pdf][BibTeX]

S. Amin, A. Abate, M. Prandini, J. Lygeros, S. Sastry,
"Reachability Analysis of Controlled Discrete-Time Stochastic Hybrid Systems", In J. Hespanha and A. Tiwari, eds.: Hybrid Systems: Computation and Control. Lecture Notes in Computer Science 3927, pp. 49 - 63, Springer Verlag.
Presented at the 9th International Workshop on Hybrid Systems, S.ta Barbara, CA, March 2006.
[pdf][BibTeX]