Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models
Xin Chen
With the ubiquitous use of computers in controlling physical systems, it
requires to have a new formalism that could model both continuous flows
and discrete jumps. Hybrid systems are introduced to this purpose. A
hybrid system, which is modeled by a hybrid automaton in the thesis, is
equipped with finitely many discrete modes and continuous real-valued
variables. A state of it is then represented by a mode along with
a valuation of the variables. Given that the system is in a mode l,
the variable values are changed continuously according to the Ordinary
Differential Equation (ODE) associated to l, or discretely by a jump
starting from l. The thesis focuses on the techniques to compute all
reachable states over a bounded time horizon and finitely many jumps
for a hybrid system with non-linear dynamics. The results of that can
then be used in safety verification of the system.
Although a great amount of work has been devoted to the reachability
analysis of hybrid systems with linear dynamics, there are few effective
approaches proposed for the non-linear case which is very often in
applications. The difficulty is twofold. Firstly, it is not easy to find
an over-approximation with acceptable accuracy for a set of the solutions
of a non-linear ODE. Secondly, to detect and compute the reachable states
under a jump requires solving non-linear real arithmetic problems which is
also difficult in general. In the thesis, we present our approaches to
deal with the above difficulties. For the first one, we present the use
of Taylor models as the over-approximate representations for non-linear
ODE solutions. Our work can be viewed as a variant of the Taylor model
method proposed by Berz et al., such that we are able to efficiently
deal with some examples with more than $10$ variables. Besides, we also
extend the work of Lin and Stadtherr to handle the ODEs with bounded
time-varying parameters. For the second difficulty, we present two
techniques: (a) domain contraction and (b) range over-approximation
to compute an enclosure for the reachable set from which a jump is
enabled. They can be seen as Satisfiability Modulo Theories (SMT)
solving algorithms which are specialized for the reachability analysis
of hybrid systems. In order to reduce the computational cost, we also
propose different heuristics for aggregating Taylor models. Besides
the above contributions, we describe a method to fast generate Taylor
model over-approximations for linear ODE solutions. Its performance is
demonstrated via a comparison with the tool SpaceEx.
To make our methods accessible by other people, we implement them in a
tool named Flow*. To examine the effectiveness, we thoroughly compare
it with some related tools which are popularly used, according to their
functionalities, over a set of non-trivial benchmarks that are collected
by us from the areas of mechanics, biology, electronic engineering and
medicine. From the experimental results, the advantage of Flow* over the
other tools becomes more apparent when the scale of the system grows. On
the other hand, it also shows that Flow* can be applied to analyzing
realistic systems.