Verification of Stochastic Hybrid Systems

John Lygeros

Over the past decade, stochastic hybrid systems have emerged as a framework for modeling systems that involve the interaction of discrete and continuous dynamics, as well as probabilistic uncertainty. Research in this area has been motivated by applications of stochastic hybrid systems to areas as diverse as systems biology, transportation, telecommunications and electrical power networks. The talk will begin with an introduction to the modeling issues that arise when treating systems with stochastic and hybrid dynamics. We will then provide a brief overview of analysis and control problems for stochastic hybrid systems, before focusing our attention to questions related to reachability. In this context, we will concentrate primarily on stochastic hybrid systems that evolve in discrete time and whose evolution at each step may be influenced by external inputs. We will show how reachability problems for this class of systems can be addressed based on methods from stochastic optimal control and discuss extensions to more general properties encoded in probabilistic temporal logics.

The latter part of the talk will be based on joint research with Sean Summers and Federico Ramponi.