CMI Silver Jubilee Lecture

P S Thiagarajan, National University of Singapore

Approximate analysis of hybrid systems

Wednesday, October 8, 2014

Abstract:

Hybrid systems are multi-modal dynamical systems in which the dynamics at each mode is governed by a system of differential equations and switching between modes are discrete events. Such systems arise frequently in domains such as cyber-physical systems and computational systems biology. Since exact analysis of these systems is intractable we develop an approximate approach. The key idea is to view the mode transitions as stochastic events. To secure the required mathematical basis, we also impose (i) a natural continuity assumption on the continuous dynamics, (ii) discretize the time points at which the states of the system are observed and (iii) a non-Zeno restriction relative to this discretization. A rich class of hybrid systems falls in this class. We show that the dynamics of such hybrid systems can be approximated as a Markov chain. Our approximation is such that the hybrid system satisfies a time bounded dynamical property iff its Markov chain approximation almost certainly satisfies the same property. Consequently one can approximately analyze the Markov chain to gain insights into the behavior of the hybrid system. Specifically we develop a statistical model checking procedure for bounded linear time temporal logic specifications in this setting.