Flow* over-approximates the reachable set over a bounded time horizon and finitely many jumps in a flowpipe construction manner. Given a bounded time interval and a natural number , Flow* computes a finite number of Taylor models containing all states which are reachable in the time  via at most  jumps.

 

Continuous dynamics

The continuous dynamics in a mode is defined by an ODE. Then we use the technique of Taylor model integration which is originally proposed by Berz and Makino to compute over-approximations for the solutions. In order to accelerate the computation, we additionally propose new techniques and heuristics to handle ODEs in different situations. For example, in the version 2.0.0, Flow* uses different schemes to generate Taylor models for linear, polynomial and non-polynomial ODEs. Besides, our tool also deals with bounded time-varying parameters in an ODE.

The flowpipe computation is polynomial-time in the system dimension (number of state variables) as well as the Taylor model order when the dynamics is a linear time-invariant or time-varying ODE. When the ODE is non-linear in the state variables, the complexity could be exponential in the system dimension. However, by specifying a relatively large cutoff threshold, our techniques can still efficiently handle non-stiff ODEs of more than 10 variables with comparatively large initial sets.

 

Discrete jumps

Given a jump, in order to compute the state set from which the jump is enabled, we need to intersect the computed reachable set in the starting mode with the jump guard. It is not easy to compute Taylor model/guard intersections. We propose two techniques: domain contraction and range over-approximation to produce an over-approximation for such an intersection. To further relieve the computation burden, the tool also aggregates the intersection over-approximations for a jump.