ReachabilityAnalysis.jl
ReachabilityAnalysis.jl copied to clipboard
Computing reachable states of dynamical systems in Julia
discretization: - https://github.com/JuliaReach/Reachability.jl/blob/master/src/ReachSets/discretize.jl#L690
[Rohou, S., Jaulin, L., Mihaylova, L., Le Bars, F., & Veres, S. M. (2017). Guaranteed computation of robot trajectories. Robotics and Autonomous Systems, 93, 76-84.](https://hal.archives-ouvertes.fr/hal-01516228/document). CC: @dpsanders
Instead of computing `ΦᵏX(0)` and checking whether the intersection with `B` is empty, one can backpropagate `B` using `(Φᵏ)⁻¹B`. In other words, `ΦᵏX(0) ∩ B = ∅ ⟺ X(0) ∩...
See [Chutinan, Krogh - Computational techniques for hybrid system verification](http://users.ece.cmu.edu/~krogh/papers/ChK03.pdf). The algorithm can be made arbitrarily precise based on partitioning the time step and initial states. This is probably not...
https://link.springer.com/chapter/10.1007/978-3-319-89963-3_17
[Serry, M., & Reissig, G. (2018, December). Hyper-Rectangular Over-Approximations of Reachable Sets for Linear Uncertain Systems. In 2018 IEEE Conference on Decision and Control (CDC) (pp. 6275-6282). IEEE.](https://ieeexplore.ieee.org/document/8619276).
[Singh, K. R., Shen, Q., & Yong, S. Z. (2018, December). Mesh-Based Affine Abstraction of Nonlinear Systems with Tighter Bounds. In 2018 IEEE Conference on Decision and Control (CDC) (pp....
Currently only handles `HACLD1` hybrid system types. This can be applied in the Platoon benchmark, for example.
https://www.sciencedirect.com/science/article/pii/S0005109818300839