1. Symbolic flowpipes for linear continuous systems

Flow* 2.1.0 computes symbolic flowpipes which are independent from the initial set and time-invariant control input for (uncertain) LTI and LTV continuous systems, such that the computed flowpipes can be reused when initial set or control input is changed. After computing the flowpipes for a LTI/LTV system, one may simply change the initial set in the output file (.flow) and let Flow* work on it to generate a new plot file or prove the safety property.

Besides, the performance of reachability computation for LTI hybrid systems can be greatly improved by reusing the symbolic flowpipes.

Examples:

–2-D LTV system.
–SpaceEx helicopter example.
–SpaceEx filtered oscillator example.

2. Symbolic remainder representation

The main source of overapproximation error in Taylor model flowpipe construction is the error accumulation in the Taylor model remainders. Although the Taylor model method can achieve good accuracy on many hard examples, it often requires large approximation orders which lead to high computational costs. To avoid heavy error accumulation, we proposed an algorithm in [1] to keep remainders symbolically for finitely many steps, such that the error accumulation along those steps can be greatly reduced. Some examples of using symbolic remainders are given as below.

Examples:

–Laub-Loomis model.
–p53 model.
–9-D genetic model.

Since the symbolic remainder representation technique is often used in less rigorous computation tasks (with low orders and large cutoff threshold), it usually has a good performance with the integration scheme “poly ode 1” in Flow*. In the future, the decomposition technique described in [1] will be added, and the symbolic remainder technique will also be applied to handling hybrid systems.

3. Safety verification during flowpipe construction

In version 2.1.0, the safety verification on flowpipes is carried out in a more efficient way along with the flowpipe construction.

4. More efficient numerical computation

The time cost of the numerical computation of Flow* is reduced by around 60%.

5. Minor changes in the modeling language

-“unsafe set” -> “unsafe”
-QR preconditioning is disabled since it is better to use the symbolic remainder technique.

References

[1] Xin Chen and Sriram Sankaranarayanan.
Decomposed Reachability Analysis for Nonlinear Systems.
In IEEE Real Time Systems Symposium (RTSS), pp. 13-24, 2016.