Sensitivity analysis for the verification of hybrid systems

One of the fundamental problems in verification and model checking is reachability. Given a system model and a set of ‘bad’ states (indicating an unwanted behaviour), does the system eventually reach these states? The generalisation of this problem for stochastic systems is called probabilistic reachability. Computing probabilistic reachability is an inherently computationally hard problem - integration. It can be shown that the number of parameter combinations to explore in order to accurately compute multi-dimensional integral grows exponentially in the number of parameters.

Computational scientists, engineers and quantitative analysts tend to be interested in sensitivity derivatives with respect to changes in the values and inputs. If very small perturbation in these values cause large changes in output values, then the feasibility of the entire simulation becomes questionable. In this research we are interested in reachability for hybrid systems, a framework widely used for modeling cyber-physical system and biological system (e.g. cancer therapies). In particular we will use Automatic Differentiation techniques for accurate and efficient computation of a derivative of a function, which is important for solving reachability problems through effective space exploration.