Verification and Simulation of Stochastic Hybrid Systems: Exploring Parametric Design Spaces

Natasha Neogi
Assistant Professor
Department of Aeronautics and Astronautics
University of Illinois at Urbana-Champaign

Verification and simulation of stochastic hybrid systems is of increasing interest to fields which encompass the notion of continuous actions intermeshed with discrete logical switches or modal behaviour; such as the chemical process engineering, biological engineering and aerospace engineering domains. At the present, our main focus outside the field of controls and computer science centers on the modeling of biological systems.

We identify several key issues that complicate the verification of safety and liveness properties of complex, interconnected systems via deterministic and stochastic methods. Techniques employing Hidden Markov Models, Stochastic Hybrid Simulation and Analytic Ellipsoidal Reachability Sets will be illustrated in the attempt to address these issues in the context of a biological example; and their strengths and weaknesses will be discussed. The conservatism and computational complexity of calculating ellipsoidal overapproximations to non-linear systems will be addressed, and the use of fast hybrid simulation in designing and exploring quality-driven tradeoffs for systems in which analytic closed form solutions are either impossible or intractable will be explored. Through guided simulation, it becomes possible to investigate the reachable state space of these models, and then find counter-example behaviour traces to properties that may be violated. Investigation of these path properties, via hidden markov modeling proves invaluable in exploring the parametric design spaces of these stochastic hybrid models.