diff --git a/docs/src/index.md b/docs/src/index.md index 6190f8ae04..6f051f7061 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -57,8 +57,7 @@ where ``CH`` is the convex hull operator, ``⊕`` denotes Minkowski sum, ``\math is a ball in the infinity norm centered at zero and radius ``1.2``, and ``B`` is a linear map of the appropriate dimensions. This equation typically arises in the study of discrete approximation models for -reachability of continuous systems, see for example -[SpaceEx: Scalable verification of hybrid systems](https://github.com/JuliaReach/Reachability.jl/wiki/References#frehse2011spaceex). +reachability of continuous systems, see for example [FrehseGDCRLRGDM11](@citet). For concreteness, we take ``A`` to be a random matrix with probability ``1\%`` of any entry being nonzero. @@ -135,9 +134,8 @@ We can visualize the result using `plot`, as shown below (left-most plot). In the second and third plots, we have used a refined method that allows to specify a prescribed accuracy for the projection (in terms of the [Hausdorff distance](https://en.wikipedia.org/wiki/Hausdorff_distance)). -For the theoretical background, see -[this reference](https://github.com/JuliaReach/Reachability.jl/wiki/References#polyhedral-approximations). It can be passed as a second argument to `overapproximate`. +For the theoretical background, see the section on [Polyhedral Approximations](@ref). |Error tol.|time (s)|memory (MB)| |------|------|------| diff --git a/docs/src/refs.bib b/docs/src/refs.bib index 0540f06c49..63fdc10bb1 100644 --- a/docs/src/refs.bib +++ b/docs/src/refs.bib @@ -1,3 +1,53 @@ +@article{Muller59, + author = {Mervin E. Muller}, + title = {A Note on a Method for Generating Points Uniformly on N-Dimensional + Spheres}, + journal = {Communications of the {ACM}}, + volume = {2}, + number = {4}, + pages = {19--20}, + year = {1959}, + url = {https://doi.org/10.1145/377939.377946}, + doi = {10.1145/377939.377946} +} + +@article{Rubin81, + title={The {B}ayesian bootstrap}, + author={Rubin, Donald B}, + journal={The annals of statistics}, + pages={130--134}, + year={1981}, + publisher={JSTOR} +} + +@incollection{Goldman90, + author = {Ronald Goldman}, + title = {Intersection of Two Lines in Three-Space}, + booktitle = {Graphics Gems}, + editor = {Andrew S. Glassner}, + publisher = {Academic Press}, + year = {1990}, + pages = {304--304} +} + +@book{Mangasarian94, + title={Nonlinear programming}, + author={Mangasarian, Olvi L}, + year={1994}, + publisher={SIAM} +} + +@article{Valtr95, + author = {Pavel Valtr}, + title = {Probability that n Random Points are in Convex Position}, + journal = {Discrete & Computational Geometry}, + volume = {13}, + pages = {637--643}, + year = {1995}, + url = {https://doi.org/10.1007/BF02574070}, + doi = {10.1007/BF02574070} +} + @article{Kamenev96, title={An algorithm for approximating polyhedra}, author={Kamenev, George K}, @@ -9,6 +59,62 @@ @article{Kamenev96 publisher={Pergamon Press} } +@article{KolmanovskyG98, + title={Theory and computation of disturbance invariant sets for discrete-time linear systems}, + author={Kolmanovsky, Ilya and Gilbert, Elmer G}, + journal={Mathematical Problems in Engineering}, + volume={4}, + number={4}, + pages={317--367}, + year={1998}, + publisher={Wiley Online Library}, + url={https://doi.org/10.1155/S1024123X98000866}, + doi={10.1155/S1024123X98000866} +} + +@book{RockafellarW98, + author = {R. Tyrrell Rockafellar and + Roger J.{-}B. Wets}, + title = {Variational Analysis}, + series = {Grundlehren der mathematischen Wissenschaften}, + volume = {317}, + publisher = {Springer}, + year = {1998}, + url = {https://doi.org/10.1007/978-3-642-02431-3}, + doi = {10.1007/978-3-642-02431-3}, + isbn = {978-3-540-62772-2} +} + +@book{ORourke98, + title={Computational geometry in {C}}, + author={O’Rourke, Joseph}, + year={1998}, + publisher={Cambridge University Press} +} + +@inproceedings{Combastel03, + author = {Christophe Combastel}, + title = {A state bounding observer based on zonotopes}, + booktitle = {European Control Conference ({ECC})}, + pages = {2589--2594}, + publisher = {{IEEE}}, + year = {2003}, + url = {https://doi.org/10.23919/ECC.2003.7085991}, + doi = {10.23919/ECC.2003.7085991} +} + +@inproceedings{GuibasNZ03, + author = {Leonidas J. Guibas and + An Thanh Nguyen and + Li Zhang}, + title = {Zonotopes as bounding volumes}, + booktitle = {Symposium on Discrete Algorithms ({SODA})}, + pages = {803--812}, + publisher = {{ACM/SIAM}}, + year = {2003}, + url = {http://dl.acm.org/citation.cfm?id=644108.644241} +} + @inproceedings{Girard05, author = {Antoine Girard}, editor = {Manfred Morari and @@ -24,6 +130,40 @@ @inproceedings{Girard05 doi = {10.1007/978-3-540-31954-2_19} } +@misc{Kvasnica05, + title={Minkowski addition of convex polytopes}, + author={Kvasnica, Michal}, + year={2005} +} + +@inproceedings{AlthoffSB07, + author = {Matthias Althoff and + Olaf Stursberg and + Martin Buss}, + title = {Reachability analysis of linear systems with uncertain parameters + and inputs}, + booktitle = {Conference on Decision and Control ({CDC})}, + pages = {726--732}, + publisher = {{IEEE}}, + year = {2007}, + url = {https://doi.org/10.1109/CDC.2007.4434084}, + doi = {10.1109/CDC.2007.4434084} +} + +@inproceedings{AlthoffSB08, + author = {Matthias Althoff and + Olaf Stursberg and + Martin Buss}, + title = {Reachability analysis of nonlinear systems with uncertain parameters + using conservative linearization}, + booktitle = {Conference on Decision and Control ({CDC})}, + pages = {4042--4048}, + publisher = {{IEEE}}, + year = {2008}, + url = {https://doi.org/10.1109/CDC.2008.4738704}, + doi = {10.1109/CDC.2008.4738704} +} + @article{LotovP08, title={The modified method of refined bounds for polyhedral approximation of convex polytopes}, author={Lotov, Alexander Vladimirovich and Pospelov, Alexis I}, @@ -36,3 +176,337 @@ @article{LotovP08 url={https://doi.org/10.1134/S0965542508060055}, doi={10.1134/S0965542508060055} } + +@inproceedings{GhorbalGP09, + author = {Khalil Ghorbal and + Eric Goubault and + Sylvie Putot}, + editor = {Ahmed Bouajjani and + Oded Maler}, + title = {The Zonotope Abstract Domain {T}aylor1+}, + booktitle = {Computer Aided Verification ({CAV})}, + series = {LNCS}, + volume = {5643}, + pages = {627--633}, + publisher = {Springer}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-02658-4_47}, + doi = {10.1007/978-3-642-02658-4_47} +} + +@phdthesis{LeGuernic09, + author = {Colas Le Guernic}, + title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.}, + school = {Joseph Fourier University, Grenoble, France}, + year = {2009}, + url = {https://tel.archives-ouvertes.fr/tel-00422569} +} + +@article{AlthoffSB10, + title={Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes}, + author={Althoff, Matthias and Stursberg, Olaf and Buss, Martin}, + journal={Nonlinear Analysis: Hybrid Systems}, + volume={4}, + number={2}, + pages={233--249}, + year={2010}, + publisher={Elsevier}, + url={https://doi.org/10.1016/j.nahs.2009.03.009}, + doi={10.1016/j.nahs.2009.03.009} +} + +@inproceedings{FrehseGDCRLRGDM11, + author = {Goran Frehse and + Colas Le Guernic and + Alexandre Donz{\'{e}} and + Scott Cotton and + Rajarshi Ray and + Olivier Lebeltel and + Rodolfo Ripado and + Antoine Girard and + Thao Dang and + Oded Maler}, + editor = {Ganesh Gopalakrishnan and + Shaz Qadeer}, + title = {{SpaceEx}: Scalable Verification of Hybrid Systems}, + booktitle = {Computer Aided Verification ({CAV})}, + series = {LNCS}, + volume = {6806}, + pages = {379--395}, + publisher = {Springer}, + year = {2011}, + url = {https://doi.org/10.1007/978-3-642-22110-1_30}, + doi = {10.1007/978-3-642-22110-1_30} +} + +@inproceedings{AlthoffK12, + author = {Matthias Althoff and + Bruce H. Krogh}, + editor = {Thao Dang and + Ian M. Mitchell}, + title = {Avoiding geometric intersection operations in reachability analysis + of hybrid systems}, + booktitle = {Hybrid Systems: Computation and Control ({HSCC})}, + pages = {45--54}, + publisher = {{ACM}}, + year = {2012}, + url = {https://doi.org/10.1145/2185632.2185643}, + doi = {10.1145/2185632.2185643} +} + +@inproceedings{Frehse012, + author = {Goran Frehse and + Rajarshi Ray}, + editor = {Maurice Heemels and + Bart De Schutter}, + title = {Flowpipe-Guard Intersection for Reachability Computations with Support + Functions}, + booktitle = {Analysis and Design of Hybrid Systems ({ADHS})}, + series = {{IFAC} Proceedings Volumes}, + volume = {45}, + number = {9}, + pages = {94--101}, + publisher = {Elsevier}, + year = {2012}, + url = {https://doi.org/10.3182/20120606-3-NL-3011.00053}, + doi = {10.3182/20120606-3-NL-3011.00053} +} + +@inproceedings{Althoff13, + author = {Matthias Althoff}, + editor = {Calin Belta and + Franjo Ivancic}, + title = {Reachability analysis of nonlinear systems using conservative polynomialization + and non-convex sets}, + booktitle = {Hybrid Systems: Computation and Control ({HSCC})}, + pages = {173--182}, + publisher = {{ACM}}, + year = {2013}, + url = {https://doi.org/10.1145/2461328.2461358}, + doi = {10.1145/2461328.2461358} +} + +@article{MaigaRTC14, + author = {Moussa Ma{\"{\i}}ga and + Nacim Ramdani and + Louise Trav{\'{e}}{-}Massuy{\`{e}}s and + Christophe Combastel}, + title = {A {CSP} Versus a Zonotope-Based Method for Solving Guard Set Intersection + in Nonlinear Hybrid Reachability}, + journal = {Mathematics in Computer Science}, + volume = {8}, + number = {3-4}, + pages = {407--423}, + year = {2014}, + url = {https://doi.org/10.1007/s11786-014-0204-y}, + doi = {10.1007/S11786-014-0204-Y} +} + +@article{Althoff15, + author = {Matthias Althoff}, + title = {On Computing the {M}inkowski Difference of Zonotopes}, + journal = {CoRR}, + volume = {abs/1512.02794}, + year = {2015}, + url = {http://arxiv.org/abs/1512.02794}, + eprinttype = {arXiv}, + eprint = {1512.02794} +} +@inproceedings{DreossiDP16, + author = {Tommaso Dreossi and + Thao Dang and + Carla Piazza}, + editor = {Alessandro Abate and + Georgios Fainekos}, + title = {Parallelotope Bundles for Polynomial Reachability}, + booktitle = {Hybrid Systems: Computation and Control ({HSCC})}, + pages = {297--306}, + publisher = {{ACM}}, + year = {2016}, + url = {https://doi.org/10.1145/2883817.2883838}, + doi = {10.1145/2883817.2883838} +} + +@inproceedings{DuggiralaV16, + author = {Parasara Sridhar Duggirala and + Mahesh Viswanathan}, + editor = {Swarat Chaudhuri and + Azadeh Farzan}, + title = {Parsimonious, Simulation Based Verification of Linear Systems}, + booktitle = {Computer Aided Verification ({CAV})}, + series = {LNCS}, + volume = {9779}, + pages = {477--494}, + publisher = {Springer}, + year = {2016}, + url = {https://doi.org/10.1007/978-3-319-41528-4_26}, + doi = {10.1007/978-3-319-41528-4_26} +} + +@inproceedings{BakD17, + author = {Stanley Bak and + Parasara Sridhar Duggirala}, + editor = {Rupak Majumdar and + Viktor Kuncak}, + title = {Simulation-Equivalent Reachability of Large Linear Systems with Inputs}, + booktitle = {Computer Aided Verification ({CAV})}, + series = {LNCS}, + volume = {10426}, + pages = {401--420}, + publisher = {Springer}, + year = {2017}, + url = {https://doi.org/10.1007/978-3-319-63387-9_20}, + doi = {10.1007/978-3-319-63387-9_20} +} + +@inproceedings{KopetzkiSA17, + author = {Anna{-}Kathrin Kopetzki and + Bastian Sch{\"{u}}rmann and + Matthias Althoff}, + title = {Methods for order reduction of zonotopes}, + booktitle = {Conference on Decision and Control ({CDC})}, + pages = {5626--5633}, + publisher = {{IEEE}}, + year = {2017}, + url = {https://doi.org/10.1109/CDC.2017.8264508}, + doi = {10.1109/CDC.2017.8264508} +} + +@article{DreossiDP17, + author = {Tommaso Dreossi and + Thao Dang and + Carla Piazza}, + title = {Reachability computation for polynomial dynamical systems}, + journal = {Formal Methods in System Design}, + volume = {50}, + number = {1}, + pages = {1--38}, + year = {2017}, + url = {https://doi.org/10.1007/s10703-016-0266-3}, + doi = {10.1007/S10703-016-0266-3} +} + +@inproceedings{SinghGMPV18, + author = {Gagandeep Singh and + Timon Gehr and + Matthew Mirman and + Markus P{\"{u}}schel and + Martin T. Vechev}, + editor = {Samy Bengio and + Hanna M. Wallach and + Hugo Larochelle and + Kristen Grauman and + Nicol{\`{o}} Cesa{-}Bianchi and + Roman Garnett}, + title = {Fast and Effective Robustness Certification}, + booktitle = {Advances in Neural Information Processing Systems ({NeurIPS})}, + pages = {10825--10836}, + year = {2018}, + url = {https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html} +} + +@article{YangS18, + author = {Xuejiao Yang and + Joseph K. Scott}, + title = {A comparison of zonotope order reduction techniques}, + journal = {Automatica}, + volume = {95}, + pages = {378--384}, + year = {2018}, + url = {https://doi.org/10.1016/j.automatica.2018.06.006}, + doi = {10.1016/J.AUTOMATICA.2018.06.006} +} + +@article{Behroozi19, + author = {Mehdi Behroozi}, + title = {Largest Inscribed Rectangles in Geometric Convex Sets}, + journal = {CoRR}, + volume = {abs/1905.13246}, + year = {2019}, + url = {http://arxiv.org/abs/1905.13246}, + eprinttype = {arXiv}, + eprint = {1905.13246} +} + +@inproceedings{MitchellBB19, + author = {Ian M. Mitchell and + Jacob Budzis and + Andriy Bolyachevets}, + editor = {Necmiye Ozay and + Pavithra Prabhakar}, + title = {Invariant, viability and discriminating kernel under-approximation + via zonotope scaling: poster abstract}, + booktitle = {Hybrid Systems: Computation and Control ({HSCC})}, + pages = {268--269}, + publisher = {{ACM}}, + year = {2019}, + url = {https://doi.org/10.1145/3302504.3313354}, + doi = {10.1145/3302504.3313354} +} + +@article{KochdumperA21, + author = {Niklas Kochdumper and + Matthias Althoff}, + title = {Sparse Polynomial Zonotopes: {A} Novel Set Representation for Reachability + Analysis}, + journal = {Transactions on Automatic Control}, + volume = {66}, + number = {9}, + pages = {4043--4058}, + year = {2021}, + publisher = {{IEEE}}, + url = {https://doi.org/10.1109/TAC.2020.3024348}, + doi = {10.1109/TAC.2020.3024348} +} + +@phdthesis{Kochdumper21a, + author = {Niklas Kochdumper}, + title = {Extensions of Polynomial Zonotopes and their Application to Verification + of Cyber-Physical Systems}, + school = {Technical University of Munich, Germany}, + year = {2022}, + url = {https://mediatum.ub.tum.de/1620128} +} + +@misc{Kochdumper21b, + author = {Niklas Kochdumper}, + title = {Challenge Problem 5: Polynomial Zonotopes in {J}ulia}, + year = {2021}, + note = {JuliaReach and JuliaIntervals Days 3} +} + +@inproceedings{KochdumperSAB23, + author = {Niklas Kochdumper and + Christian Schilling and + Matthias Althoff and + Stanley Bak}, + editor = {Kristin Yvonne Rozier and + Swarat Chaudhuri}, + title = {Open- and Closed-Loop Neural Network Verification Using Polynomial + Zonotopes}, + booktitle = {{NASA} Formal Methods ({NFM})}, + series = {LNCS}, + volume = {13903}, + pages = {16--36}, + publisher = {Springer}, + year = {2023}, + url = {https://doi.org/10.1007/978-3-031-33170-1_2}, + doi = {10.1007/978-3-031-33170-1_2} +} + +@article{WetzlingerKBA23, + author = {Mark Wetzlinger and + Niklas Kochdumper and + Stanley Bak and + Matthias Althoff}, + title = {Fully Automated Verification of Linear Systems Using Inner and Outer + Approximations of Reachable Sets}, + journal = {Transactions on Automatic Control}, + volume = {68}, + number = {12}, + pages = {7771--7786}, + year = {2023}, + publisher = {{IEEE}}, + url = {https://doi.org/10.1109/TAC.2023.3292008}, + doi = {10.1109/TAC.2023.3292008} +} diff --git a/src/Approximations/box_approximation.jl b/src/Approximations/box_approximation.jl index 480dc83ce3..63eb291f58 100644 --- a/src/Approximations/box_approximation.jl +++ b/src/Approximations/box_approximation.jl @@ -213,15 +213,11 @@ A hyperrectangle. ### Algorithm -This function implements the method in [Section 5.1.2, 1]. A zonotope +This function implements the method in [AlthoffSB10; Section 5.1.2](@citet). A zonotope ``Z = ⟨c, G⟩`` can be tightly overapproximated by an axis-aligned hyperrectangle such that its center is ``c`` and the radius along dimension ``i`` is the column-sum of the absolute values of the ``i``-th row of ``G`` for ``i = 1,…, p``, where ``p`` is the number of generators of ``Z``. - -[1] Althoff, M., Stursberg, O., & Buss, M. (2010). *Computing reachable sets of -hybrid systems using a combination of zonotopes and polytopes.* Nonlinear -analysis: hybrid systems, 4(2), 233-249. """ function box_approximation(Z::AbstractZonotope) r = sum(abs, genmat(Z); dims=2)[:] diff --git a/src/Approximations/overapproximate.jl b/src/Approximations/overapproximate.jl index a7ef2fadce..fc20d5cb13 100644 --- a/src/Approximations/overapproximate.jl +++ b/src/Approximations/overapproximate.jl @@ -319,7 +319,7 @@ The idea is to solve the univariate optimization problem `ρ(di, X ∩ Hi)` for each half-space of the set `P` and then take the minimum. This gives an overapproximation of the exact support function. -This algorithm is inspired from [1]. +This algorithm is inspired from [Frehse012](@citet). ### Notes @@ -327,9 +327,6 @@ This method relies on having available the `constraints_list` of the polyhedron `P`. This method may return a non-empty set even if the original set is empty. - -[1] G. Frehse, R. Ray. *Flowpipe-Guard Intersection for Reachability -Computations with Support Functions*. ADHS 2012. """ function overapproximate(cap::Intersection{N, # TODO use better mechanism to detect polyhedral set <:LazySet, @@ -463,11 +460,7 @@ An overapproximation of the given zonotopic set using a parallelotope. ### Algorithm -The algorithm is based on Proposition 8 discussed in Section 5 of [1]. - -[1] Althoff, M., Stursberg, O., & Buss, M. (2010). *Computing reachable sets of -hybrid systems using a combination of zonotopes and polytopes*. Nonlinear -analysis: hybrid systems, 4(2), 233-249. +The algorithm is based on Proposition 8 discussed in [AlthoffSB10; Section 5](@citet). """ function overapproximate(Z::AbstractZonotope, ::Type{<:HParallelotope}, indices=1:dim(Z)) @@ -513,10 +506,7 @@ otherwise the result is an `HPolyhedron`. ### Algorithm -This function implements [Algorithm 8.1, 1]. - -[1] Colas Le Guernic. *Reachability Analysis of Hybrid Systems with Linear -continuous dynamics* (Doctoral dissertation). 2009. +This function implements [LeGuernic09; Algorithm 8.1](@citet). """ function overapproximate(X::Intersection{N,<:AbstractZonotope,<:Hyperplane}, dirs::AbstractDirections) where {N} @@ -582,11 +572,7 @@ polynomial zonotope. ### Algorithm -This method implements Proposition 13 of [1]. - -[1] N. Kochdumper and M. Althoff. *Sparse Polynomial Zonotopes: A Novel Set -Representation for Reachability Analysis*. Transactions on Automatic Control -2021. +This method implements [KochdumperA21; Proposition 13](@citet). """ function overapproximate(QM::QuadraticMap{N,<:SparsePolynomialZonotope}, ::Type{<:SparsePolynomialZonotope}) where {N} diff --git a/src/Approximations/overapproximate_zonotope.jl b/src/Approximations/overapproximate_zonotope.jl index ee2486e39d..eecc94f0f4 100644 --- a/src/Approximations/overapproximate_zonotope.jl +++ b/src/Approximations/overapproximate_zonotope.jl @@ -46,7 +46,7 @@ incomparable. ##### 'mean' method -If `algorithm == "mean"`, we choose the method proposed in [1]. +If `algorithm == "mean"`, we choose the method proposed in [Girard05](@citet). The convex hull of two zonotopic sets ``Z₁`` and ``Z₂`` of the same order, which we write @@ -65,11 +65,11 @@ If the zonotope order is not the same, this algorithm calls It should be noted that the output zonotope is not necessarily the minimal enclosing zonotope, which is in general expensive to obtain in high dimensions. -This is further investigated in [2]. +This is further investigated in [GuibasNZ03](@citet). ##### 'join' method -If `algorithm == "join"`, we choose the method proposed in [3, Definition 1]. +If `algorithm == "join"`, we choose the method proposed in [GhorbalGP09; Definition 1](@citet). The convex hull ``X`` of two zonotopic sets ``Z₁`` and ``Z₂`` is overapproximated by a zonotope ``Z₃`` such that the box approximation of ``X`` is identical with the box approximation of ``Z₃``. @@ -98,17 +98,6 @@ The following formula defines the sum of all those generators. where ``c`` is the center of the new zonotope and the ``g``s are the generators constructed in the first phase. - -##### References - -[1] *Reachability of Uncertain Linear Systems Using Zonotopes*. A. Girard. - HSCC 2005. - -[2] *Zonotopes as bounding volumes*. L. J. Guibas, A. T. Nguyen, L. Zhang. - SODA 2003. - -[3] *The zonotope abstract domain Taylor1+*. K. Ghorbal, E. Goubault, S. Putot. - CAV 2009. """ function overapproximate(X::ConvexHull{N,<:AbstractZonotope,<:AbstractZonotope}, ::Type{<:Zonotope}; algorithm="mean") where {N} @@ -327,11 +316,7 @@ A zonotope. ### Algorithm -This method implements Proposition 1 in [1]. - -[1] M. Althoff in *Reachability analysis of nonlinear systems using conservative - polynomialization and non-convex sets*, Hybrid Systems: Computation and - Control, 2013, pp. 173-182. +This method implements [Althoff13; Proposition 1](@citet). """ function overapproximate(P::DensePolynomialZonotope, ::Type{<:Zonotope}) η = polynomial_order(P) @@ -697,7 +682,7 @@ function load_intervalmatrices_overapproximation() ### Algorithm - This implementation uses the method proposed in [1]. + This implementation uses the method proposed in [AlthoffSB07](@citet). Given an interval matrix ``M = \\tilde{M} + ⟨-\\hat{M},\\hat{M}⟩`` (split into a conventional matrix and a symmetric interval matrix) and a zonotope @@ -709,9 +694,6 @@ function load_intervalmatrices_overapproximation() v_j = \\begin{cases} 0 & i ≠ j \\\\ \\hat{M}_j (|c| + ∑_{k=1}^m |g_k|) & i = j. \\end{cases} ``` - - [1] Althoff, Stursberg, Buss. *Reachability analysis of linear systems with - uncertain parameters and inputs*. CDC 2007. """ function overapproximate(lm::LinearMap{N,<:AbstractZonotope,NM, <:AbstractIntervalMatrix{NM}}, @@ -826,8 +808,8 @@ We preprocess the directions in that respect. ### Algorithm We solve a linear program parametric in the vertices ``v_j`` of `X` and the -directions ``d_k`` in `dir` presented in Section 4.2 in [1], adapting the -notation to the one used in this library. +directions ``d_k`` in `dir` presented in Section 4.2 in [GuibasNZ03](@citet), +adapting the notation to the one used in this library. ```math \\min ∑_{k=1}^l α_k \\ @@ -840,10 +822,7 @@ notation to the one used in this library. The resulting zonotope has center `c` and generators `α_k · d_k`. Note that the first type of side constraints is vector-based and that the -nonnegativity constraints (last type) are not stated explicitly in [1]. - -[1] *Zonotopes as bounding volumes*. L. J. Guibas, A. T. Nguyen, L. Zhang. - SODA 2003. +nonnegativity constraints (last type) are not stated explicitly in [GuibasNZ03](@cite). """ function _overapproximate_zonotope_vrep(X::LazySet{N}, dir::AbstractDirections; @@ -949,10 +928,7 @@ zonotopes, and finally converts the Cartesian product of the sets to a zonotope. ### Algorithm -The implementation is based on Section 8.2.4 in [1]. - -[1] Le Guernic, C. *Reachability analysis of hybrid systems with linear -continuous dynamics* (Doctoral dissertation). 2009. +The implementation is based on [LeGuernic09; Section 8.2.4](@citet). """ function _overapproximate_zonotope_cpa(X::LazySet, dir::AbstractDirections) n = dim(X) @@ -1005,10 +981,7 @@ A zonotope overapproximation of the set obtained by rectifying `Z`. ### Algorithm -This method implements [Theorem 3.1, 1]. - -[1] Singh, G., Gehr, T., Mirman, M., Püschel, M., & Vechev, M. *Fast and -effective robustness certification*. NeurIPS 2018. +This method implements [SinghGMPV18; Theorem 3.1](@citet). """ function overapproximate(r::Rectification{N,<:AbstractZonotope}, ::Type{<:Zonotope}) where {N} @@ -1123,10 +1096,7 @@ Mathematically, a quadratic map of a zonotope with matrices ``Q`` is defined as: ### Algorithm -This method implements [Lemma 1, 1]. - -[1] Matthias Althoff and Bruce H. Krogh. *Avoiding geometric intersection -operations in reachability analysis of hybrid systems*. HSCC 2012. +This method implements [AlthoffK12; Lemma 1](@citet). """ function overapproximate(QM::QuadraticMap{N,<:AbstractZonotope}, ::Type{<:Zonotope}) where {N} @@ -1179,11 +1149,7 @@ A zonotope overapproximating the intersection. ### Algorithm -This method implements Algorithm 3 in [1]. - -[1] Moussa Maïga, Nacim Ramdani, Louise Travé-Massuyès, Christophe Combastel: -*A CSP versus a zonotope-based method for solving guard set intersection in -nonlinear hybrid reachability*. Mathematics in Computer Science (8) 2014. +This method implements [MaigaRTC14; Algorithm 3](@citet). """ function overapproximate(X::Intersection{N,<:AbstractZonotope,<:Hyperplane}, ::Type{<:Zonotope}) where {N} diff --git a/src/Approximations/underapproximate.jl b/src/Approximations/underapproximate.jl index 8c39f74bd6..e9a6b0225d 100644 --- a/src/Approximations/underapproximate.jl +++ b/src/Approximations/underapproximate.jl @@ -75,12 +75,9 @@ Due to numerical issues, the result may be slightly outside the set. ### Algorithm -The algorithm is taken from [1, Theorem 17] and solves a convex program (in fact +The algorithm is taken from [Behroozi19; Theorem 17](@citet) and solves a convex program (in fact a linear program with nonlinear objective). (The objective is modified to an equivalent version due to solver issues.) - -[1] Mehdi Behroozi - *Largest inscribed rectangles in geometric convex sets.* -arXiv:1905.13246. """ function underapproximate(X::LazySet{N}, ::Type{<:Hyperrectangle}; solver=nothing) where {N} diff --git a/src/ConcreteOperations/cartesian_product.jl b/src/ConcreteOperations/cartesian_product.jl index ad0a0df120..34fad7b328 100644 --- a/src/ConcreteOperations/cartesian_product.jl +++ b/src/ConcreteOperations/cartesian_product.jl @@ -163,11 +163,7 @@ end ### Algorithm -This method implements Proposition 3.1.22 in [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application - to verification of cyber-physical systems.* PhD diss., Technische Universität - München, 2022. +This method implements [Kochdumper21a; Proposition 3.1.22](@citet). """ @commutative function cartesian_product(SPZ::SparsePolynomialZonotope, Z::AbstractZonotope) c = vcat(center(SPZ), center(Z)) diff --git a/src/ConcreteOperations/intersection.jl b/src/ConcreteOperations/intersection.jl index 8733f6565e..bd96a458d1 100644 --- a/src/ConcreteOperations/intersection.jl +++ b/src/ConcreteOperations/intersection.jl @@ -945,11 +945,7 @@ between the given sets is not empty. ### Algorithm -This function implements [Algorithm 8.2, 1]. - -[1] *Colas Le Guernic. Reachability Analysis of Hybrid Systems with Linear -Continuous Dynamics. Computer Science [cs]. Université Joseph-Fourier - Grenoble -I, 2009. English. fftel-00422569v2f* +This function implements [LeGuernic09; Algorithm 8.2](@citet). """ function _bound_intersect_2D(Z::Zonotope, L::Line2D) c = center(Z) diff --git a/src/ConcreteOperations/isdisjoint.jl b/src/ConcreteOperations/isdisjoint.jl index a8772aae85..4d1d21cf56 100644 --- a/src/ConcreteOperations/isdisjoint.jl +++ b/src/ConcreteOperations/isdisjoint.jl @@ -197,14 +197,11 @@ end ### Algorithm -The algorithm is taken from [1]. +The algorithm is taken from [GuibasNZ03](@citet). ``Z1 ∩ Z2 = ∅`` iff ``c_1 - c_2 ∉ Z(0, (g_1, g_2))`` where ``c_i`` and ``g_i`` are the center and generators of zonotope `Zi` and ``Z(c, g)`` represents the zonotope with center ``c`` and generators ``g``. - -[1] L. J. Guibas, A. T. Nguyen, L. Zhang: *Zonotopes as bounding volumes*. SODA -2003. """ function isdisjoint(Z1::AbstractZonotope, Z2::AbstractZonotope, witness::Bool=false; solver=nothing) @@ -672,9 +669,7 @@ for ST in [:AbstractZonotope, :AbstractSingleton] end end -# see Proposition 8 in Wetzlinger, Kochdumper, Bak, Althoff: * Fully-automated -# verification of linear systems using inner- and outer-approximations of -# reachable sets*. 2022. +# See [WetzlingerKBA23; Proposition 8](@citet). @commutative function isdisjoint(Z::AbstractZonotope, P::AbstractPolyhedron, witness::Bool=false; solver=nothing) n = dim(Z) diff --git a/src/ConcreteOperations/issubset.jl b/src/ConcreteOperations/issubset.jl index 74fc12b83b..72043ccda8 100644 --- a/src/ConcreteOperations/issubset.jl +++ b/src/ConcreteOperations/issubset.jl @@ -202,6 +202,8 @@ each direction of the constraints of ``P``. For witness generation, we use a support vector in the first direction where the above check fails. + +See [WetzlingerKBA23; Proposition 7](@citet). """ function ⊆(X::LazySet, P::AbstractPolyhedron, witness::Bool=false) if !isconvextype(typeof(X)) @@ -210,10 +212,8 @@ function ⊆(X::LazySet, P::AbstractPolyhedron, witness::Bool=false) return _issubset_constraints_list(X, P, witness) end -# S ⊆ P where P = ⟨Cx ≤ d⟩ iff y ≤ d where y is the upper corner of box(C*S) -# -# see Proposition 7 in Wetzlinger, Kochdumper, Bak, Althoff: *Fully-automated verification -# of linear systems using inner- and outer-approximations of reachable sets*. 2022. +# S ⊆ P where P = ⟨Cx ≤ d⟩ iff y ≤ d where y is the upper corner of box(C*S). +# See [WetzlingerKBA23; Proposition 7](@citet). function _issubset_in_polyhedron_high(S::LazySet, P::LazySet, witness::Bool=false) @assert dim(S) == dim(P) @@ -233,8 +233,7 @@ function ⊆(Z::AbstractZonotope, P::AbstractPolyhedron, witness::Bool=false) return _issubset_zonotope_in_polyhedron(Z, P, witness) end -# implements Proposition 7 in Wetzlinger, Kochdumper, Bak, Althoff: *Fully-automated verification -# of linear systems using inner- and outer-approximations of reachable sets*. 2022. +# See [WetzlingerKBA23; Proposition 7](@citet). function _issubset_zonotope_in_polyhedron(Z::AbstractZonotope, P::LazySet, witness::Bool=false) @assert dim(Z) == dim(P) @@ -887,10 +886,7 @@ end ### Algorithm -The algorithm is based on Lemma 3.1 in [1]. - -[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. *Invariant, viability and -discriminating kernel under-approximation via zonotope scaling*. HSCC 2019. +The algorithm is based on [MitchellBB19; Lemma 3.1](@citet). """ function ⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, witness::Bool=false) c = center(Z) diff --git a/src/ConcreteOperations/minkowski_difference.jl b/src/ConcreteOperations/minkowski_difference.jl index 7dedd1bfa2..90b9ede1c4 100644 --- a/src/ConcreteOperations/minkowski_difference.jl +++ b/src/ConcreteOperations/minkowski_difference.jl @@ -21,7 +21,7 @@ is bounded. ### Algorithm -This method implements Theorem 2.3 in [1]: +This method implements [KolmanovskyG98; Theorem 2.3](@citet): Suppose ``P`` is a polyhedron ```math @@ -34,11 +34,6 @@ Then the Minkowski difference is ```math \\{z ∈ ℝ^n: sᵢᵀz ≤ rᵢ - ρ(sᵢ,Q),~i = 1, …, N\\}. ``` - -[1] Ilya Kolmanovsky and Elmer G. Gilbert (1997). *Theory and computation -of disturbance invariant sets for discrete-time linear systems.* -[Mathematical Problems in Engineering Volume 4, Issue 4, Pages -317-367.](http://dx.doi.org/10.1155/S1024123X98000866) """ function minkowski_difference(P::LazySet, Q::LazySet) @assert ispolyhedral(P) "this implementation requires that the first argument " * @@ -100,10 +95,8 @@ An `HPolytope`. ### Algorithm For one-dimensional sets, this method implements a simple algorithm for intervals. -For two-dimensional sets, this method implements Proposition 6 in [1]. -For higher-dimensional sets, this method implements Theorem 3 in [1]. - -[1] M. Althoff: *On computing the Minkowski difference of zonotopes*. 2022. +For two-dimensional sets, this method implements [Althoff15; Proposition 6](@citet). +For higher-dimensional sets, this method implements [Althoff15; Theorem 3](@citet). """ function minkowski_difference(Z1::AbstractZonotope, Z2::AbstractZonotope) n = dim(Z1) @@ -129,8 +122,7 @@ function _minkowski_difference_1d(Z1::AbstractZonotope, Z2::AbstractZonotope) return Zonotope([c], hcat([(c - l) / 2])) end -# implements Proposition 6 in [1] -# [1] M. Althoff: *On computing the Minkowski difference of zonotopes*. 2022. +# See [Althoff15; Proposition 6](@citet). function _minkowski_difference_2d(Zm::AbstractZonotope, Zs::AbstractZonotope) N = promote_type(eltype(Zm), eltype(Zs)) Gm = genmat(Zm) @@ -169,6 +161,7 @@ function _minkowski_difference_2d(Zm::AbstractZonotope, Zs::AbstractZonotope) return Zonotope(c, G) end +# See [Althoff15; Theorem 3](@citet). function _minkowski_difference_nd(Z1::AbstractZonotope, Z2::AbstractZonotope) Gm = genmat(Z1) n, p = size(Gm) diff --git a/src/ConcreteOperations/minkowski_sum.jl b/src/ConcreteOperations/minkowski_sum.jl index 226479aa2a..97c5123f63 100644 --- a/src/ConcreteOperations/minkowski_sum.jl +++ b/src/ConcreteOperations/minkowski_sum.jl @@ -76,7 +76,7 @@ and `Q`. ### Algorithm This function implements the concrete Minkowski sum by projection and variable -elimination as detailed in [1]. The idea is that if we write ``P`` and ``Q`` in +elimination as detailed in [Kvasnica05](@citet). The idea is that if we write ``P`` and ``Q`` in *simple H-representation*, that is, ``P = \\{x ∈ ℝ^n : Ax ≤ b \\}`` and ``Q = \\{x ∈ ℝ^n : Cx ≤ d \\}``, then their Minkowski sum can be seen as the projection onto the first ``n``-dimensional coordinates of the @@ -103,8 +103,6 @@ itself uses `CDDLib` for variable elimination. The available algorithms are: to it - `Polyhedra.ProjectGenerators` -- projection by computing the V-representation - -[1] Kvasnica, Michal. "Minkowski addition of convex polytopes." (2005): 1-10. """ function minkowski_sum(P::AbstractPolyhedron, Q::AbstractPolyhedron; backend=nothing, algorithm=nothing, prune=true) @@ -325,9 +323,7 @@ for T in [:LazySet, :AbstractPolyhedron, :AbstractPolytope, :AbstractZonotope, end end -# See Proposition 3.1.19 in [1]. -# [1] Kochdumper. *Extensions of polynomial zonotopes and their application to -# verification of cyber-physical systems.* PhD diss., TU Munich, 2022. +# See [Kochdumper21a; Proposition 3.1.19](@citet). @commutative function minkowski_sum(PZ::SparsePolynomialZonotope, Z::AbstractZonotope) c = center(PZ) + center(Z) G = genmat_dep(PZ) diff --git a/src/Convert/SimpleSparsePolynomialZonotope.jl b/src/Convert/SimpleSparsePolynomialZonotope.jl index 6a89f55616..2108012c25 100644 --- a/src/Convert/SimpleSparsePolynomialZonotope.jl +++ b/src/Convert/SimpleSparsePolynomialZonotope.jl @@ -14,10 +14,7 @@ A simple sparse polynomial zonotope. ### Algorithm -This method implements Proposition 3 in [1]. - -[1] Kochdumper, Althoff. *Sparse polynomial zonotopes - a novel set -representation for reachability analysis*. 2021 +This method implements [KochdumperA21; Proposition 3](@citet). """ function Base.convert(::Type{SimpleSparsePolynomialZonotope}, Z::AbstractZonotope) c = center(Z) @@ -43,10 +40,7 @@ A simple sparse polynomial zonotope. ### Algorithm -The method implements Proposition 3.1.4 from [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application to -verification of cyber-physical systems.* PhD diss., Technische Universität München, 2022. +The method implements [Kochdumper21a; Proposition 3.1.4](@citet). """ function Base.convert(::Type{SimpleSparsePolynomialZonotope}, SPZ::SparsePolynomialZonotope) c = center(SPZ) diff --git a/src/Convert/SparsePolynomialZonotope.jl b/src/Convert/SparsePolynomialZonotope.jl index cec8cf302c..87a8539a61 100644 --- a/src/Convert/SparsePolynomialZonotope.jl +++ b/src/Convert/SparsePolynomialZonotope.jl @@ -14,10 +14,7 @@ A sparse polynomial zonotope. ### Algorithm -The method implements Proposition 3.1.9 from [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application to -verification of cyber-physical systems.* PhD diss., Technische Universität München, 2022. +The method implements [Kochdumper21a; Proposition 3.1.19](@citet). """ function convert(::Type{SparsePolynomialZonotope}, Z::AbstractZonotope{N}) where {N} c = center(Z) diff --git a/src/Interfaces/AbstractPolyhedron_functions.jl b/src/Interfaces/AbstractPolyhedron_functions.jl index 807bc0e84b..a75f48aa80 100644 --- a/src/Interfaces/AbstractPolyhedron_functions.jl +++ b/src/Interfaces/AbstractPolyhedron_functions.jl @@ -731,7 +731,7 @@ This computation can be avoided using the `check_nonempty` flag. ### Algorithm -The algorithm is based on Stiemke's theorem of alternatives, see, e.g., [1]. +The algorithm is based on Stiemke's theorem of alternatives, see, e.g., [Mangasarian94](@citet). Let the polyhedron ``P`` be given in constraint form ``Ax ≤ b``. We assume that the polyhedron is non-empty. @@ -741,9 +741,6 @@ Proposition 1. If ``\\ker(A)≠\\{0\\}``, then ``P`` is unbounded. Proposition 2. Assume that ``ker(A)={0}`` and ``P`` is non-empty. Then ``P`` is bounded if and only if the following linear program admits a feasible solution: ``\\min∥y∥_1`` subject to ``A^Ty=0`` and ``y≥1``. - -[1] Mangasarian, Olvi L. *Nonlinear programming.* - Society for Industrial and Applied Mathematics, 1994. """ function _isbounded_stiemke(constraints::AbstractVector{<:HalfSpace{N}}; solver=default_lp_solver(N), diff --git a/src/Interfaces/AbstractZonotope.jl b/src/Interfaces/AbstractZonotope.jl index 00287cbe56..2027472e7e 100644 --- a/src/Interfaces/AbstractZonotope.jl +++ b/src/Interfaces/AbstractZonotope.jl @@ -540,16 +540,13 @@ If this assumption is not given, the implementation tries to work around. ### Algorithm -We follow the algorithm presented in [1]. Three cases are not covered by that +We follow the algorithm presented in [AlthoffSB10](@citet). Three cases are not covered by that algorithm, so we handle them separately. The first case is zonotopes in one dimension. The second case is that there are fewer generators than dimensions, ``p < n``, or the generator matrix is not full rank, in which case we fall back to the (slower) computation based on the vertex representation. The third case is that the zonotope is flat in some dimensions, in which case we project the zonotope to the non-flat dimensions and extend the result later. - -[1] Althoff, Stursberg, Buss. *Computing Reachable Sets of Hybrid Systems Using -a Combination of Zonotopes and Polytopes*. 2009. """ function constraints_list(Z::AbstractZonotope{<:AbstractFloat}) return _constraints_list_zonotope(Z) @@ -661,8 +658,8 @@ their union is `Z` and their intersection is possibly non-empty. ### Algorithm -This function implements [Prop. 3, 1], which we state next. The zonotopic set -``Z = ⟨c, g^{(1, …, p)}⟩`` is split into: +This function implements [AlthoffSB08; Prop. 3](@citet), which we state next. +The zonotopic set ``Z = ⟨c, g^{(1, …, p)}⟩`` is split into: ```math Z₁ = ⟨c - \\frac{1}{2}g^{(j)}, (g^{(1, …,j-1)}, \\frac{1}{2}g^{(j)}, g^{(j+1, …, p)})⟩ \\\\ @@ -673,9 +670,6 @@ such that ``Z₁ ∪ Z₂ = Z`` and ``Z₁ ∩ Z₂ = Z^*``, where ```math Z^* = ⟨c, (g^{(1,…,j-1)}, g^{(j+1,…, p)})⟩. ``` - -[1] Althoff, M., Stursberg, O., & Buss, M. *Reachability analysis of nonlinear -systems with uncertain parameters using conservative linearization*. CDC 2008. """ function split(Z::AbstractZonotope, j::Int) return _split(convert(Zonotope, Z), j) @@ -796,30 +790,21 @@ abstract type AbstractReductionMethod end """ GIR05 <: AbstractReductionMethod -Zonotope order-reduction method from [1]. - -- [1] A. Girard. *Reachability of Uncertain Linear Systems Using Zonotopes*. -HSCC 2005. +Zonotope order-reduction method from [Girard05](@citet). """ struct GIR05 <: AbstractReductionMethod end """ COMB03 <: AbstractReductionMethod -Zonotope order-reduction method from [1]. - -- [1] C. Combastel. *A state bounding observer based on zonotopes*. ECC 2003. +Zonotope order-reduction method from [Combastel03](@citet). """ struct COMB03 <: AbstractReductionMethod end """ ASB10 <: AbstractReductionMethod -Zonotope order-reduction method from [1]. - -- [1] Althoff, M., Stursberg, O., & Buss, M. *Computing reachable sets of hybrid -systems using a combination of zonotopes and polytopes*. Nonlinear analysis: -hybrid systems 2010. +Zonotope order-reduction method from [AlthoffSB10](@citet). """ struct ASB10 <: AbstractReductionMethod end @@ -855,16 +840,8 @@ julia> subtypes(AbstractReductionMethod) See the documentation of each algorithm for references. These methods split the given zonotopic set `Z` into two zonotopes, `K` and `L`, where `K` contains the most "representative" generators and `L` contains the generators that are -reduced, `Lred`, using a box overapproximation. We follow the notation from [1]. -See also [2]. - -- [1] Yang, X., & Scott, J. K. *A comparison of zonotope order reduction -techniques*. Automatica 2018. -- [2] Kopetzki, A. K., Schürmann, B., & Althoff, M. *Methods for order reduction -of zonotopes*. CDC 2017. -- [3] Althoff, M., Stursberg, O., & Buss, M. *Computing reachable sets of hybrid -systems using a combination of zonotopes and polytopes*. Nonlinear analysis: -hybrid systems 2010. +reduced, `Lred`, using a box overapproximation. We follow the notation from +[YangS18](@citet). See also [KopetzkiSA17](@citet). """ function reduce_order(Z::AbstractZonotope, r::Real, method::AbstractReductionMethod=GIR05()) diff --git a/src/LazyOperations/Intersection.jl b/src/LazyOperations/Intersection.jl index 2ab669b8a0..ec4e6403cc 100644 --- a/src/LazyOperations/Intersection.jl +++ b/src/LazyOperations/Intersection.jl @@ -383,13 +383,7 @@ The algorithms are based on solving the associated optimization problem where ``D_h = \\{ λ : λ ≥ 0 \\}`` if ``H`` is a half-space or ``D_h = \\{ λ : λ ∈ ℝ \\}`` if ``H`` is a hyperplane. -For additional information we refer to: - -[1] G. Frehse, R. Ray. *Flowpipe-Guard Intersection for Reachability - Computations with Support Functions.* -[2] C. Le Guernic. *Reachability Analysis of Hybrid Systems with Linear - Continuous Dynamics*, PhD thesis -[3] T. Rockafellar, R. Wets. *Variational Analysis*. +For additional information we refer to [Frehse012, LeGuernic09, RockafellarW98](@citet) """ function ρ(d::AbstractVector, cap::Intersection{N,S1,S2}; algorithm::String="line_search", @@ -430,10 +424,7 @@ The idea is to solve the univariate optimization problem `ρ(di, X ∩ Hi)` for each half-space in the polyhedron and then take the minimum. This gives an overapproximation of the exact support value. -This algorithm is inspired from [1]. - -[1] G. Frehse, R. Ray. *Flowpipe-Guard Intersection for Reachability - Computations with Support Functions*. +This algorithm is inspired from [Frehse012](@citet). ### Notes @@ -897,12 +888,12 @@ The evaluation of the support function of ``X ∩ H`` along direction ``ℓ``. This projection method is based on Prop. 8.2, [1, page 103]. -In the original algorithm, Section 8.2 of [1], the linear map is performed +In the original algorithm, [LeGuernic09; Section 8.2](@citet), the linear map is performed concretely and the intersection is performed lazily (these are the default options in this algorithm, but here the four combinations are available). If the set ``X`` is a zonotope, its concrete projection is again a zonotope (sometimes called "zonogon"). The intersection between this zonogon and the line -can be taken efficiently in a lazy way (see Section 8.2.2 of [1]), +can be taken efficiently in a lazy way (see [LeGuernic09; Section 8.2.2](@cite)), if one uses dispatch on `ρ(y_dir, Sℓ⋂Lγ; kwargs...)` given that `Sℓ` is itself a zonotope. @@ -914,9 +905,6 @@ again for this second calculation. The option `algorithm_2d_intersection` is used for that: if not given, the default support-function algorithm is used (e.g., `"line_search"`). You can still pass additional arguments to the `"line_search"` backend through the `kwargs` arguments. - -[1] C. Le Guernic. *Reachability Analysis of Hybrid Systems with Linear -Continuous Dynamics*, PhD thesis. """ function _projection(ℓ, X::LazySet, H::Union{Hyperplane,Line2D}; lazy_linear_map=false, diff --git a/src/Sets/Ball2/sample.jl b/src/Sets/Ball2/sample.jl index ac5d3a1af2..6e30aaca21 100644 --- a/src/Sets/Ball2/sample.jl +++ b/src/Sets/Ball2/sample.jl @@ -50,7 +50,7 @@ The modified vector `D`. ### Algorithm -This function implements Muller's method of normalized Gaussians [1] to +This function implements Muller's method of normalized Gaussians [Muller59](@citet) to uniformly sample from the interior of the unit ball. Given ``n`` Gaussian random variables ``Z₁, Z₂, …, Z_n`` and a uniformly @@ -62,9 +62,6 @@ of the vectors ``` where ``α := \\sqrt{z₁² + z₂² + … + z_n²}``, is uniform over the ``n``-dimensional unit ball. - -[1] Muller, Mervin E. *A note on a method for generating points uniformly on - n-dimensional spheres.* Communications of the ACM 2.4 (1959): 19-20. """ function _sample_unit_nball_muller!(D::Vector{<:Vector}, n::Int, p::Int; rng::AbstractRNG=GLOBAL_RNG, diff --git a/src/Sets/DensePolynomialZonotope/DensePolynomialZonotope.jl b/src/Sets/DensePolynomialZonotope/DensePolynomialZonotope.jl index d4ce4df937..47f33eebdd 100644 --- a/src/Sets/DensePolynomialZonotope/DensePolynomialZonotope.jl +++ b/src/Sets/DensePolynomialZonotope/DensePolynomialZonotope.jl @@ -14,7 +14,7 @@ Type that represents a polynomial zonotope. ### Notes -Polynomial zonotopes were introduced in [1] and have been applied as non-convex +Polynomial zonotopes were introduced in [Althoff13](@citet) and have been applied as non-convex set representation to the reachability problem of nonlinear ODEs. Mathematically, a polynomial zonotope is defined as the tuple ``(c, E, F, G)``, @@ -60,10 +60,6 @@ The polynomial zonotope ``(c, E, F, G)`` defines the set: ``` where the number of factors in the final product, ``β_j β_k ⋯ β_m``, corresponds to the polynomial order ``η``. - -[1] M. Althoff in *Reachability analysis of nonlinear systems using conservative - polynomialization and non-convex sets*, Hybrid Systems: Computation and - Control, 2013, pp. 173-182. """ struct DensePolynomialZonotope{N,VT,VMT,MT} <: AbstractPolynomialZonotope{N} c::VT diff --git a/src/Sets/HParallelotope/HParallelotope.jl b/src/Sets/HParallelotope/HParallelotope.jl index dbdca1f6aa..040d99a121 100644 --- a/src/Sets/HParallelotope/HParallelotope.jl +++ b/src/Sets/HParallelotope/HParallelotope.jl @@ -36,21 +36,8 @@ default constructor thus checks these conditions, which can be deactivated by passing the argument `check_consistency=false`. For details as well as applications of parallelotopes in reachability analysis -we refer to [1] and [2]. For conversions between set representations we refer to -[3]. - -### References - -[1] Tommaso Dreossi, Thao Dang, and Carla Piazza. *Reachability computation for -polynomial dynamical systems.* Formal Methods in System Design 50.1 (2017): 1-38. - -[2] Tommaso Dreossi, Thao Dang, and Carla Piazza. *Parallelotope bundles for -polynomial reachability.* Proceedings of the 19th International Conference on -Hybrid Systems: Computation and Control. ACM, 2016. - -[3] Matthias Althoff, Olaf Stursberg, and Martin Buss. *Computing reachable sets -of hybrid systems using a combination of zonotopes and polytopes.* Nonlinear -analysis: hybrid systems 4.2 (2010): 233-249. +we refer to [DreossiDP17](@citet) and [DreossiDP16](@citet). For conversions +between set representations we refer to [AlthoffSB10](@citet). """ struct HParallelotope{N,VN<:AbstractVector{N},MN<:AbstractMatrix{N}} <: AbstractZonotope{N} directions::MN diff --git a/src/Sets/HParallelotope/base_vertex.jl b/src/Sets/HParallelotope/base_vertex.jl index 52d7ae4aa9..b7937dad3c 100644 --- a/src/Sets/HParallelotope/base_vertex.jl +++ b/src/Sets/HParallelotope/base_vertex.jl @@ -16,10 +16,7 @@ The base vertex of `P`. Intuitively, the base vertex is the point from which we get the relative positions of all the other points. The base vertex can be computed as the solution of the ``n``-dimensional linear -system ``D_i x = c_{n+i}`` for ``i = 1, …, n``, see [1, Section 3.2.1]. - -[1] Dreossi, Tommaso, Thao Dang, and Carla Piazza. *Reachability computation for -polynomial dynamical systems.* Formal Methods in System Design 50.1 (2017): 1-38. +system ``D_i x = c_{n+i}`` for ``i = 1, …, n``, see [DreossiDP17; Section 3.2.1](@citet). """ function base_vertex(P::HParallelotope) D, c = P.directions, P.offset diff --git a/src/Sets/HParallelotope/extremal_vertices.jl b/src/Sets/HParallelotope/extremal_vertices.jl index b975517027..bfb0d5e9e8 100644 --- a/src/Sets/HParallelotope/extremal_vertices.jl +++ b/src/Sets/HParallelotope/extremal_vertices.jl @@ -25,10 +25,7 @@ The extremal vertices can be computed as the solution of the ``n``-dimensional linear systems of equations ``D x = v_i`` where for each ``i = 1, …, n``, ``v_i = [-c_{n+1}, …, c_i, …, -c_{2n}]``. -We refer to [1, Section 3.2.1] for details. - -[1] Tommaso Dreossi, Thao Dang, and Carla Piazza. *Reachability computation for -polynomial dynamical systems.* Formal Methods in System Design 50.1 (2017): 1-38. +We refer to [DreossiDP17; Section 3.2.1](@citet) for details. """ function extremal_vertices(P::HParallelotope{N,VN}) where {N,VN} D, c = P.directions, P.offset diff --git a/src/Sets/LineSegment/isdisjoint.jl b/src/Sets/LineSegment/isdisjoint.jl index 4da2b65070..705df5d01b 100644 --- a/src/Sets/LineSegment/isdisjoint.jl +++ b/src/Sets/LineSegment/isdisjoint.jl @@ -6,15 +6,12 @@ ### Algorithm The algorithm is inspired from [here](https://stackoverflow.com/a/565282), which -again is the special 2D case of a 3D algorithm from [1]. +itself is the special 2D case of a 3D algorithm from [Goldman90](@citet). We first check if the two line segments are parallel, and if so, if they are collinear. In the latter case, we check membership of any of the end points in the other line segment. Otherwise the lines are not parallel, so we can solve an equation of the intersection point, if it exists. - -[1] Ronald Goldman. *Intersection of two lines in three-space*. Graphics Gems -1990. """ function isdisjoint(L1::LineSegment, L2::LineSegment, witness::Bool=false) r = L1.q - L1.p diff --git a/src/Sets/SimpleSparsePolynomialZonotope/SimpleSparsePolynomialZonotope.jl b/src/Sets/SimpleSparsePolynomialZonotope/SimpleSparsePolynomialZonotope.jl index 76f3e036d4..8c05a2ea31 100644 --- a/src/Sets/SimpleSparsePolynomialZonotope/SimpleSparsePolynomialZonotope.jl +++ b/src/Sets/SimpleSparsePolynomialZonotope/SimpleSparsePolynomialZonotope.jl @@ -25,14 +25,8 @@ is the exponent matrix with matrix elements ``E_{k, i}``. ### Notes -Sparse polynomial zonotopes were introduced in [1]. The *simple* variation -was defined in [2]. - -- [1] N. Kochdumper and M. Althoff. *Sparse Polynomial Zonotopes: A Novel Set -Representation for Reachability Analysis*. Transactions on Automatic Control, -2021. -- [2] N. Kochdumper. *Challenge Problem 5: Polynomial Zonotopes in Julia.* -JuliaReach and JuliaIntervals Days 3, 2021. +Sparse polynomial zonotopes were introduced in [KochdumperA21](@citet). +The *simple* variant was defined in [Kochdumper21b]. """ struct SimpleSparsePolynomialZonotope{N,VN<:AbstractVector{N}, MN<:AbstractMatrix{N}, diff --git a/src/Sets/SimpleSparsePolynomialZonotope/cartesian_product.jl b/src/Sets/SimpleSparsePolynomialZonotope/cartesian_product.jl index 548d1daffb..b2f67824a1 100644 --- a/src/Sets/SimpleSparsePolynomialZonotope/cartesian_product.jl +++ b/src/Sets/SimpleSparsePolynomialZonotope/cartesian_product.jl @@ -6,11 +6,7 @@ ### Algorithm -This method implements Proposition 3.1.22 in [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application - to verification of cyber-physical systems.* PhD diss., Technische Universität - München, 2022. +This method implements [Kochdumper21a; Proposition 3.1.22](@citet). """ function cartesian_product(P1::SimpleSparsePolynomialZonotope, P2::SimpleSparsePolynomialZonotope) diff --git a/src/Sets/SimpleSparsePolynomialZonotope/linear_combination.jl b/src/Sets/SimpleSparsePolynomialZonotope/linear_combination.jl index 09153a30c0..cf483f463c 100644 --- a/src/Sets/SimpleSparsePolynomialZonotope/linear_combination.jl +++ b/src/Sets/SimpleSparsePolynomialZonotope/linear_combination.jl @@ -6,10 +6,7 @@ ### Notes -This method implements the algorithm described in Proposition 3.1.25 of [1]. - -[1] N. Kochdumper. *Extensions of polynomial zonotopes and their application to -verification of cyber-physical systems*. 2021. +This method implements the algorithm described in [Kochdumper21a; Proposition 3.1.25](@citet). """ function linear_combination(P1::SimpleSparsePolynomialZonotope, P2::SimpleSparsePolynomialZonotope) diff --git a/src/Sets/SimpleSparsePolynomialZonotope/quadratic_map.jl b/src/Sets/SimpleSparsePolynomialZonotope/quadratic_map.jl index c67ccd2c7a..f2d1be1b7c 100644 --- a/src/Sets/SimpleSparsePolynomialZonotope/quadratic_map.jl +++ b/src/Sets/SimpleSparsePolynomialZonotope/quadratic_map.jl @@ -14,13 +14,8 @@ The quadratic map of `P` represented as a simple sparse polynomial zonotope. ### Algorithm -This method implements Proposition 12 in [1]. -See also Proposition 3.1.30 in [2]. - -[1] N. Kochdumper, M. Althoff. *Sparse polynomial zonotopes: A novel set -representation for reachability analysis*. 2021 -[2] N. Kochdumper. *Extensions of polynomial zonotopes and their application to -verification of cyber-physical systems*. 2021. +This method implements [KochdumperA21; Proposition 12](@citet). +See also [Kochdumper21a; Proposition 3.1.30](@citet). """ function quadratic_map(Q::Vector{<:AbstractMatrix}, S::SimpleSparsePolynomialZonotope) m = length(Q) @@ -74,10 +69,7 @@ a simple sparse polynomial zonotope. ### Algorithm -This method implements Proposition 3.1.30 in [1]. - -[1] N. Kochdumper. *Extensions of polynomial zonotopes and their application to -verification of cyber-physical systems*. 2021. +This method implements [Kochdumper21a; Proposition 3.1.30](@citet). """ function quadratic_map(Q::Vector{<:AbstractMatrix}, S1::SimpleSparsePolynomialZonotope, S2::SimpleSparsePolynomialZonotope) diff --git a/src/Sets/SparsePolynomialZonotope/SparsePolynomialZonotope.jl b/src/Sets/SparsePolynomialZonotope/SparsePolynomialZonotope.jl index d5aff1e6dd..084bc5ca9a 100644 --- a/src/Sets/SparsePolynomialZonotope/SparsePolynomialZonotope.jl +++ b/src/Sets/SparsePolynomialZonotope/SparsePolynomialZonotope.jl @@ -34,10 +34,7 @@ storing a unique identifier for each dependent factor ``αₖ``. ### Notes -Sparse polynomial zonotopes were introduced in [1]. - -- [1] N. Kochdumper and M. Althoff. *Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis*. - Transactions on Automatic Control, 2021. +Sparse polynomial zonotopes were introduced in [KochdumperA21](@citet). """ struct SparsePolynomialZonotope{N, VN<:AbstractVector{N}, diff --git a/src/Sets/SparsePolynomialZonotope/cartesian_product.jl b/src/Sets/SparsePolynomialZonotope/cartesian_product.jl index d6af3e6699..00531f1ed9 100644 --- a/src/Sets/SparsePolynomialZonotope/cartesian_product.jl +++ b/src/Sets/SparsePolynomialZonotope/cartesian_product.jl @@ -5,11 +5,7 @@ ### Algorithm -This method implements Proposition 3.1.22 in [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application - to verification of cyber-physical systems.* PhD diss., Technische Universität - München, 2022. +This method implements [Kochdumper21a; Proposition 3.1.22](@citet). """ function cartesian_product(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope) c = vcat(center(P1), center(P2)) diff --git a/src/Sets/SparsePolynomialZonotope/exact_sum.jl b/src/Sets/SparsePolynomialZonotope/exact_sum.jl index dad88b7658..7b46fd99b5 100644 --- a/src/Sets/SparsePolynomialZonotope/exact_sum.jl +++ b/src/Sets/SparsePolynomialZonotope/exact_sum.jl @@ -5,11 +5,7 @@ ### Algorithm -This method implements Proposition 3.1.20 in [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application - to verification of cyber-physical systems.* PhD diss., Technische Universität - München, 2022. +This method implements [Kochdumper21a; Proposition 3.1.20](@citet). """ function exact_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope) if indexvector(P1) != indexvector(P2) diff --git a/src/Sets/SparsePolynomialZonotope/extrema.jl b/src/Sets/SparsePolynomialZonotope/extrema.jl index d4fbd3b91b..b4600a1649 100644 --- a/src/Sets/SparsePolynomialZonotope/extrema.jl +++ b/src/Sets/SparsePolynomialZonotope/extrema.jl @@ -8,9 +8,7 @@ function extrema(P::SparsePolynomialZonotope; algorithm::String="zonotope") end end -# Proposition 1 from [1] -# [1] Kochdumper et al.: *Open- and closed-loop neural network verification -# using polynomial zonotopes*. NFM 2023. +# See [KochdumperSAB23; Proposition 1](@citet). function _extrema_polyzono_zonotope(P::SparsePolynomialZonotope{N}) where {N} G = genmat_dep(P) E = expmat(P) diff --git a/src/Sets/SparsePolynomialZonotope/minkowski_sum.jl b/src/Sets/SparsePolynomialZonotope/minkowski_sum.jl index f88ee66ebb..8d37f363cd 100644 --- a/src/Sets/SparsePolynomialZonotope/minkowski_sum.jl +++ b/src/Sets/SparsePolynomialZonotope/minkowski_sum.jl @@ -5,10 +5,7 @@ ### Algorithm -See Proposition 3.1.19 in [1]. - -[1] Kochdumper. *Extensions of polynomial zonotopes and their application to - verification of cyber-physical systems.* PhD diss., TU Munich, 2022. +See [Kochdumper21a; Proposition 3.1.19](@citet). """ function minkowski_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope) diff --git a/src/Sets/SparsePolynomialZonotope/reduce_order.jl b/src/Sets/SparsePolynomialZonotope/reduce_order.jl index 8b7837b15f..9e4a76b0c8 100644 --- a/src/Sets/SparsePolynomialZonotope/reduce_order.jl +++ b/src/Sets/SparsePolynomialZonotope/reduce_order.jl @@ -6,10 +6,7 @@ ### Notes -This method implements the algorithm described in Proposition 3.1.39 of [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application to verification of cyber-physical systems.* - PhD diss., Technische Universität München, 2022. +This method implements the algorithm described in [Kochdumper21a; Proposition 3.1.39](@citet). """ function reduce_order(P::SparsePolynomialZonotope, r::Real, method::AbstractReductionMethod=GIR05()) diff --git a/src/Sets/SparsePolynomialZonotope/support_function.jl b/src/Sets/SparsePolynomialZonotope/support_function.jl index 82bafa1207..fbaa72bc2d 100644 --- a/src/Sets/SparsePolynomialZonotope/support_function.jl +++ b/src/Sets/SparsePolynomialZonotope/support_function.jl @@ -18,10 +18,7 @@ An overapproximation of the support function in the given direction. ### Algorithm -This method implements Proposition 3.1.16 in [1]. - -[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application to verification of cyber-physical systems.* - PhD diss., Technische Universität München, 2022. +This method implements [Kochdumper21a; Proposition 3.1.16](@citet). """ function ρ(d::AbstractVector, P::SparsePolynomialZonotope; enclosure_method=nothing) diff --git a/src/Sets/Star/Star.jl b/src/Sets/Star/Star.jl index 8b11ace1a1..3ecc7c6f9b 100644 --- a/src/Sets/Star/Star.jl +++ b/src/Sets/Star/Star.jl @@ -33,6 +33,9 @@ We remark that a `Star` is mathematically equivalent to the affine map of the polyhedral set `P`, with the transformation matrix and translation vector being `V` and `c`, respectively. +Star sets as defined here were introduced in [DuggiralaV16](@citet); see also +[BakD17](@citet) for a preliminary definition. + ### Examples This example is drawn from Example 1 in [2]. Consider the two-dimensional plane @@ -81,23 +84,6 @@ In this case, the generalized star ``S`` above is equivalent to the rectangle ```math T = \\{(x, y) ∈ ℝ^2 : (2 ≤ x ≤ 4) ∧ (2 ≤ y ≤ 4) \\} ``` - -### References - -Star sets as defined here were introduced in [1]; see also [2] for a preliminary -definition. For applications in reachability analysis of neural networks, see -[3]. - -- [1] Duggirala, P. S., and Mahesh V. *Parsimonious, simulation based verification of linear systems.* - International Conference on Computer Aided Verification. Springer, Cham, 2016. - -- [2] Bak S, Duggirala PS. *Simulation-equivalent reachability of large linear systems with inputs.* - In International Conference on Computer Aided Verification - 2017 Jul 24 (pp. 401-420). Springer, Cham. - -- [3] Tran, H. D., Lopez, D. M., Musau, P., Yang, X., Nguyen, L. V., Xiang, W., & Johnson, T. T. (2019, October). - *Star-based reachability analysis of deep neural networks.* - In International Symposium on Formal Methods (pp. 670-686). Springer, Cham. """ struct Star{N,VN<:AbstractVector{N},MN<:AbstractMatrix{N},PT<:AbstractPolyhedron{N}} <: AbstractPolyhedron{N} diff --git a/src/Sets/Tetrahedron/in.jl b/src/Sets/Tetrahedron/in.jl index ab9c8e13bc..ea54b215e8 100644 --- a/src/Sets/Tetrahedron/in.jl +++ b/src/Sets/Tetrahedron/in.jl @@ -6,9 +6,7 @@ ### Algorithm For each plane of the tetrahedron, we check if the point `x` is on the same side as the remaining vertex. -We need to check this for each plane [1]. - -[1] https://stackoverflow.com/questions/25179693/how-to-check-whether-the-point-is-in-the-tetrahedron-or-not +[We need to check this for each plane](https://stackoverflow.com/questions/25179693/how-to-check-whether-the-point-is-in-the-tetrahedron-or-not). """ function ∈(x::AbstractVector, T::Tetrahedron) v = T.vertices diff --git a/src/Sets/VPolygon/rand.jl b/src/Sets/VPolygon/rand.jl index 12cd65764f..ab38b62780 100644 --- a/src/Sets/VPolygon/rand.jl +++ b/src/Sets/VPolygon/rand.jl @@ -21,11 +21,8 @@ For a negative value we choose a random number in the range ### Algorithm We follow the idea described [here](https://stackoverflow.com/a/47358689) based -on [1]. There is also a nice video available +on [Valtr95](@citet). There is also a nice video available [here](http://cglab.ca/~sander/misc/ConvexGeneration/convex.html). - -[1] Pavel Valtr: *Probability that n random points are in convex position*. -Discret. Comput. Geom. 1995. """ function rand(::Type{VPolygon}; N::Type{<:Real}=Float64, diff --git a/src/Sets/VPolygon/support_vector.jl b/src/Sets/VPolygon/support_vector.jl index e2b7c15b7c..cefad3158b 100644 --- a/src/Sets/VPolygon/support_vector.jl +++ b/src/Sets/VPolygon/support_vector.jl @@ -21,9 +21,7 @@ The brute-force search compares the projection of each vector along the given direction and runs in ``O(n)`` where ``n`` is the number of vertices. The binary search runs in ``O(log n)`` and we follow [this implementation](http://geomalgorithms.com/a14-_extreme_pts.html#polyMax_2D()) -based on an algorithm described in [1]. - -[1] Joseph O'Rourke, *Computational Geometry in C (2nd Edition)*. +based on an algorithm described in [ORourke98](@citet). """ function σ(d::AbstractVector, P::VPolygon) @assert !isempty(P.vertices) "the polygon has no vertices" diff --git a/src/Utils/samples.jl b/src/Utils/samples.jl index 9a685f3bea..1ee68a7af3 100644 --- a/src/Utils/samples.jl +++ b/src/Utils/samples.jl @@ -225,17 +225,11 @@ combination of its vertices, i.e., ``p = ∑_{i} v_i α_i`` for some (non-negative) coefficients ``\\{α_i\\}_i`` that add up to 1. The algorithm chooses a random convex combination (the ``α_i``). To produce this combination, we apply the finite-difference operator on a sorted -uniform sample over ``[0, 1]``; the method can be found in [1] and [2]. +uniform sample over ``[0, 1]``; the method can be found in [Rubin81](@citet) and +[this StackExchange post](https://cs.stackexchange.com/a/3229). If `variant == true`, we start from a random vertex and then repeatedly walk toward a random vertex inside the polytope. - -### References - -[1] *Rubin, Donald B. The Bayesian bootstrap. The annals of statistics (1981): -130-134.* - -[2] [StackExchange post](https://cs.stackexchange.com/a/3229) """ struct RandomWalkSampler <: AbstractSampler variant::Bool @@ -604,8 +598,8 @@ The modified vector `D`. ### Algorithm -This function implements Muller's method of normalized Gaussians [1] to -uniformly sample over the ``n``-dimensional sphere ``S^n`` (which is the +This function implements Muller's method of normalized Gaussians [Muller59](@citet) +to uniformly sample over the ``n``-dimensional sphere ``S^n`` (which is the bounding surface of the ``n``-dimensional unit ball). Given ``n`` canonical Gaussian random variables ``Z₁, Z₂, …, Z_n``, the @@ -615,9 +609,6 @@ distribution of the vectors \\dfrac{1}{α}\\left(z₁, z₂, …, z_n\\right)^T, ``` where ``α := \\sqrt{z₁² + z₂² + … + z_n²}``, is uniform over ``S^n``. - -[1] Muller, Mervin E. *A note on a method for generating points uniformly on - n-dimensional spheres.* Communications of the ACM 2.4 (1959): 19-20. """ function _sample_unit_nsphere_muller!(D::Vector{Vector{N}}, n::Int, p::Int; rng::AbstractRNG=GLOBAL_RNG, diff --git a/test/ConcreteOperations/minkowski_difference.jl b/test/ConcreteOperations/minkowski_difference.jl index 06d44eaa4d..a06927f196 100644 --- a/test/ConcreteOperations/minkowski_difference.jl +++ b/test/ConcreteOperations/minkowski_difference.jl @@ -21,8 +21,7 @@ for N in [Float64, Float32, Rational{Int}] D = minkowski_difference(H1, H2) @test D isa EmptySet{N} && dim(D) == 2 - # zonotopes in 2D (taken from Fig. 2 in [1]) - # [1] M. Althoff: *On computing the Minkowski difference of zonotopes*. 2022 + # zonotopes in 2D (taken from [Althoff15; Fig. 2 in the 2022 version](@citet)) Zm = Zonotope(N[1, 1], N[1 0 1; 0 1 1]) if N isa AbstractFloat diff --git a/test/Sets/HParallelotope.jl b/test/Sets/HParallelotope.jl index 5fdc4bbf6c..6b3d77acc7 100644 --- a/test/Sets/HParallelotope.jl +++ b/test/Sets/HParallelotope.jl @@ -1,8 +1,5 @@ for N in [Float32, Float64, Rational{Int}] - # Example 6 from [1]. - # - # [1] Tommaso Dreossi, Thao Dang, and Carla Piazza. *Reachability computation for polynomial dynamical systems.* - # Formal Methods in System Design 50.1 (2017): 1-38. + # See [DreossiDP17; Example 6](@citet). D = N[-1 0 0; -1 -1 0; 0 0 -1] c = N[-0.80, -0.95, 0, 0.85, 1, 0] P = HParallelotope(D, c)