New reachability algorithms:
We have added a novel set-based reachability algorithm for computing inner approximations of nonlinear systems.
Furthermore, we have integrated recently proposed backward reachability algorithms for linear continuous-time systems.
New spectrahedral shadow class:
We added a new set representation \(\texttt{spectraShadow}\) to CORA (Sec. 2.2.1.10):
Spectrahedral shadows can be seen as the semidefinite generalization of polytopes,
and can represent a large variety of convex sets.
In particular, every convex set representation implemented in CORA can be represented as a spectrahedral shadow.
Improved neural network verification and new set-based training:
We improved the code to verify neural networks and harmonized it with all other CORA modules.
Additionally, we added a novel approach to train verifiably robust networks both in the supervised and in the reinforcement learning setting.
Please visit Sec. 6 for more information.
Reachset-conformance identification:
We added several new functionalities to the reachset-conformance identification in CORA.
Please visit Sec. 4.1.10 for details.
Verification of dynamic systems using signal temporal logic:
Improvements have been made how signal temporal logic can be used to verify dynamic systems,
in particular using a new incremental algorithm to verify hybrid systems.
Overhaul of dynamic systems:
We overhauled all dynamics system classes to ensure the correctness of our implementation and improve maintainability.
This also comes with an updated syntax for hybrid systems as described in Sec. 4.3,
in particular how reset functions are constructed.
Polytopes:
Our \(\texttt{polytope}\) class got a massive overhaul with several new functionalities.
Vertex representation and halfspace representation can now also be instantiated independently from another,
making the usage more flexible. Visit Sec. 2.2.1.4 for details.
Matrix sets:
We improved the performance of matrix sets by restructuring their properties as multi-dimensional matrices instead of cell arrays.
Please visit Sec. 3 for the new syntax.
Miscellaneous:
Minor improvements have been made in various parts of the code:
Some basic functionality runs more efficiently,
standardized input argument validation and more accurate error messages enhance the responsiveness,
and more unit tests ensure greater reliability.
Please also have a look at Appendix A.12 for deprecated functionality and their replacements.