Reading SpaceEx format:
One can now read SpaceEx models, which have become the quasi-standard for formal verification tools of hybrid systems.
This also has the advantage that one can use the SpaceEx model editor1 for modeling hybrid systems.
Parallel hybrid automata:
It is infeasible to model larger hybrid systems using a single hybrid automaton.
It is now possible to specify parallel hybrid automata so that it is no longer required
to model a system by a single hybrid automaton.
For analysis purposes, we assemble the dynamics of parallel hybrid automata on-the-fly.
New zonotope reduction methods:
New methods for the order reduction of zonotopes are now available in CORA.
Lazy symbolic computations:
CORA performs symbolic computations for nonlinear systems, e.g., to linearize them for various linearization points.
These computations used to be performed for each reachability analysis.
Now these time-consuming computations are only performed if the model files are changed
or options concerning the symbolic computations are modified.
Taylor models:
In our new version, we have realized a class to compute with Taylor models.
Affine arithmetic:
As a byproduct of the Taylor model implementation, we have also implemented an affine arithmetic
when the number of noise terms does not exceed the system dimension.
Constrained zonotope:
This new set representation is as general as polytopes, but makes it possible to use lazy computations.
Discrete time models:
It is now possible to compute reachable sets of discrete time models.
We have not implemented a class for linear discrete time models, since this is too trivial.
More compact implementation:
We have integrated the class linVarSys into the class linParamSys.
Also, we have unified all symbolic computations, which are now inherited from all other classes for continuous dynamics.
Miscellaneous:
There are many other interesting improvements:
Better organization of models, directly changing parameters for nonlinear systems during reachability analysis,
better controlling simplifications of symbolic expressions, more unit tests,
vector and matrix norms for vector and matrix sets,
extending linear systems to affine systems, etc.