@inproceedings{ImmlerAlthoffBenetetal.2019, author = {Immler, Fabian and Althoff, Matthias and Benet, Luis and Chapoutot, Alexandre and Chen, Xin and Forets, Marcelo and Geretti, Luca and Kochdumper, Niklas and Sanders, David P. and Schilling, Christian}, title = {ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics}, volume = {61}, booktitle = {ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems}, editor = {Frehse, Goran and Althoff, Matthias}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/m75b}, pages = {41 -- 61}, year = {2019}, language = {en} } @inproceedings{AlthoffBakForetsetal.2019, author = {Althoff, Matthias and Bak, Stanley and Forets, Marcelo and Frehse, Goran and Kochdumper, Niklas and Ray, Rajarshi and Schilling, Christian and Schupp, Stefan}, title = {ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics}, volume = {61}, booktitle = {ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems}, editor = {Frehse, Goran and Althoff, Matthias}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/bj1w}, pages = {14 -- 40}, year = {2019}, language = {en} } @inproceedings{GerettiAlexandreDitSandrettoAlthoffetal.2020, author = {Geretti, Luca and Alexandre Dit Sandretto, Julien and Althoff, Matthias and Benet, Luis and Chapoutot, Alexandre and Chen, Xin and Collins, Pieter and Forets, Marcelo and Freire, Daniel and Immler, Fabian and Kochdumper, Niklas and Sanders, David P. and Schilling, Christian}, title = {ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics}, volume = {74}, booktitle = {ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20)}, editor = {Frehse, Goran and Althoff, Matthias}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/zkf6}, pages = {49 -- 75}, year = {2020}, language = {en} } @inproceedings{AlthoffBakBaoetal.2020, author = {Althoff, Matthias and Bak, Stanley and Bao, Zongnan and Forets, Marcelo and Frehse, Goran and Freire, Daniel and Kochdumper, Niklas and Li, Yangge and Mitra, Sayan and Ray, Rajarshi and Schilling, Christian and Schupp, Stefan and Wetzlinger, Mark}, title = {ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics}, volume = {74}, booktitle = {ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20)}, editor = {Frehse, Goran and Althoff, Matthias}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/7dt2}, pages = {16 -- 48}, year = {2020}, language = {en} } @inproceedings{ImmlerAlthoffChenetal.2018, author = {Immler, Fabian and Althoff, Matthias and Chen, Xin and Fan, Chuchu and Frehse, Goran and Kochdumper, Niklas and Li, Yangge and Mitra, Sayan and Tomar, Mahendra Singh and Zamani, Majid}, title = {ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics}, volume = {54}, booktitle = {ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems}, editor = {Frehse, Goran}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/mskf}, pages = {53 -- 70}, year = {2018}, language = {en} } @inproceedings{AlthoffBakChenetal.2018, author = {Althoff, Matthias and Bak, Stanley and Chen, Xin and Fan, Chuchu and Forets, Marcelo and Frehse, Goran and Kochdumper, Niklas and Li, Yangge and Mitra, Sayan and Ray, Rajarshi and Schilling, Christian and Schupp, Stefan}, title = {ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics}, volume = {54}, booktitle = {ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems}, editor = {Frehse, Goran}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/73mb}, pages = {23 -- 52}, year = {2018}, language = {en} } @inproceedings{AlthoffGrebenyukKochdumper2018, author = {Althoff, Matthias and Grebenyuk, Dmitry and Kochdumper, Niklas}, title = {Implementation of Taylor models in CORA 2018}, volume = {54}, booktitle = {ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems}, editor = {Frehse, Goran}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/zzc7}, pages = {145 -- 173}, year = {2018}, language = {en} } @inproceedings{SchuermannKochdumperAlthoff2019, author = {Sch{\"u}rmann, Bastian and Kochdumper, Niklas and Althoff, Matthias}, title = {Reachset Model Predictive Control for Disturbed Nonlinear Systems}, booktitle = {2018 IEEE Conference on Decision and Control (CDC)}, publisher = {IEEE}, address = {Piscataway}, isbn = {978-1-5386-1395-5}, doi = {https://doi.org/10.1109/CDC.2018.8619781}, pages = {3463 -- 3470}, year = {2019}, language = {en} } @inproceedings{WetzlingerKochdumperAlthoff2021, author = {Wetzlinger, Mark and Kochdumper, Niklas and Althoff, Matthias}, title = {Adaptive Parameter Tuning for Reachability Analysis of Linear Systems}, booktitle = {2020 59th IEEE Conference on Decision and Control (CDC)}, publisher = {IEEE}, address = {Piscataway}, isbn = {978-1-7281-7447-1}, doi = {https://doi.org/10.1109/CDC42340.2020.9304431}, pages = {5145 -- 5152}, year = {2021}, language = {en} } @inproceedings{WetzlingerKochdumperBaketal.2023, author = {Wetzlinger, Mark and Kochdumper, Niklas and Bak, Stanley and Althoff, Matthias}, title = {Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions}, pages = {5}, booktitle = {Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, part of CPS-IoT Week}, publisher = {ACM}, address = {New York}, isbn = {979-8-4007-0033-0}, doi = {https://doi.org/10.1145/3575870.3587121}, year = {2023}, language = {en} } @inproceedings{KochdumperTarrafRechmaletal.2020, author = {Kochdumper, Niklas and Tarraf, Ahmad and Rechmal, Malgorzata and Olbrich, Markus and Hedrich, Lars and Althoff, Matthias}, title = {Establishing Reachset Conformance for the Formal Analysis of Analog Circuits}, booktitle = {ASP-DAC 2020: 25th Asia and South Pacific Design Automation Conference, Proceedings}, publisher = {IEEE}, address = {Piscataway}, isbn = {978-1-7281-4123-7}, doi = {https://doi.org/10.1109/ASP-DAC47756.2020.9045120}, pages = {199 -- 204}, year = {2020}, language = {en} } @inproceedings{KochdumperAlthoff2020, author = {Kochdumper, Niklas and Althoff, Matthias}, title = {Reachability Analysis for Hybrid Systems with Nonlinear Guard Sets}, pages = {2}, booktitle = {Proceedings of the 23rd ACM International Conference on Hybrid Systems: Computation and Control (part of CPS-IoT Week)}, publisher = {ACM}, address = {New York}, isbn = {978-1-4503-7018-9}, doi = {https://doi.org/10.1145/3365365.3382194}, year = {2020}, language = {en} } @inproceedings{KochdumperSchuermannAlthoff2020, author = {Kochdumper, Niklas and Sch{\"u}rmann, Bastian and Althoff, Matthias}, title = {Utilizing Dependencies to Obtain Subsets of Reachable Sets}, pages = {1}, booktitle = {Proceedings of the 23rd ACM International Conference on Hybrid Systems: Computation and Control (part of CPS-IoT Week)}, publisher = {ACM}, address = {New York}, isbn = {978-1-4503-7018-9}, doi = {https://doi.org/10.1145/3365365.3382192}, year = {2020}, language = {en} } @inproceedings{KochdumperAlthoff2021, author = {Kochdumper, Niklas and Althoff, Matthias}, title = {Computing Non-Convex Inner-Approximations of Reachable Sets for Nonlinear Continuous Systems}, booktitle = {2020 59th IEEE Conference on Decision and Control (CDC)}, publisher = {IEEE}, address = {Piscataway}, isbn = {978-1-7281-7447-1}, doi = {https://doi.org/10.1109/CDC42340.2020.9304022}, pages = {2130 -- 2137}, year = {2021}, language = {en} } @inproceedings{KochdumperGassertAlthoff2021, author = {Kochdumper, Niklas and Gassert, Philipp and Althoff, Matthias}, title = {Verification of Collision Avoidance for CommonRoad Traffic Scenarios}, volume = {80}, booktitle = {8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)}, editor = {Frehse, Goran and Althoff, Matthias}, publisher = {EasyChair}, address = {Bramhall}, issn = {2398-7340}, doi = {https://doi.org/10.29007/1973}, pages = {184 -- 194}, year = {2021}, language = {en} } @inproceedings{KochdumperGruberSchuermannetal.2021, author = {Kochdumper, Niklas and Gruber, Felix and Sch{\"u}rmann, Bastian and Gaßmann, Victor and Klischat, Moritz and Althoff, Matthias}, title = {AROC: A Toolbox for Automated Reachset Optimal Controller Synthesis}, pages = {23}, booktitle = {Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control (part of CPS-IoT Week)}, publisher = {ACM}, address = {New York}, isbn = {978-1-4503-8339-4}, doi = {https://doi.org/10.1145/3447928.3456703}, year = {2021}, language = {en} } @inproceedings{KochdumperSchillingAlthoffetal.2023, author = {Kochdumper, Niklas and Schilling, Christian and Althoff, Matthias and Bak, Stanley}, title = {Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes}, booktitle = {NASA Formal Methods: 15th International Symposium, NFM 2023 Houston, TX, USA, May 16-18, 2023, Proceedings}, editor = {Rozier, Kristin Yvonne and Chaudhuri, Swarat}, publisher = {Springer}, address = {Cham}, isbn = {978-3-031-33170-1}, doi = {https://doi.org/10.1007/978-3-031-33170-1_2}, pages = {16 -- 36}, year = {2023}, language = {en} } @article{SchuermannKlischatKochdumperetal.2021, author = {Sch{\"u}rmann, Bastian and Klischat, Moritz and Kochdumper, Niklas and Althoff, Matthias}, title = {Formal Safety Net Control Using Backward Reachability Analysis}, volume = {67}, journal = {IEEE Transactions on Automatic Control}, number = {11}, publisher = {IEEE}, address = {New York}, issn = {1558-2523}, doi = {https://doi.org/10.1109/TAC.2021.3124188}, pages = {5698 -- 5713}, year = {2021}, language = {en} } @article{VerdierKochdumperAlthoffetal.2022, author = {Verdier, Cees Ferdinand and Kochdumper, Niklas and Althoff, Matthias and Mazo, Manuel}, title = {Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications}, volume = {2022}, pages = {110184}, journal = {Automatica}, number = {139}, publisher = {Elsevier}, address = {Amsterdam}, issn = {1873-2836}, doi = {https://doi.org/10.1016/j.automatica.2022.110184}, year = {2022}, abstract = {We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the specification, an initial condition violating the specification is extracted as a counterexample. Based on this counterexample, candidate solutions are refined until eventually a solution is found (or a user-specified number of iterations is met). The resulting sampled-data controller is expressed as a closed-form expression, enabling both interpretability and the implementation in embedded hardware with limited memory and computation power. The effectiveness of our approach is demonstrated for multiple systems.}, language = {en} } @article{WetzlingerKochdumperBaketal.2023, author = {Wetzlinger, Mark and Kochdumper, Niklas and Bak, Stanley and Althoff, Matthias}, title = {Fully Automated Verification of Linear Systems Using Inner and Outer Approximations of Reachable Sets}, volume = {68}, journal = {IEEE Transactions on Automatic Control}, number = {12}, publisher = {IEEE}, address = {New York}, issn = {1558-2523}, doi = {https://doi.org/10.1109/TAC.2023.3292008}, pages = {7771 -- 7786}, year = {2023}, language = {en} } @article{LuetzowKochdumperAlthoff2025, author = {L{\"u}tzow, Laura and Kochdumper, Niklas and Althoff, Matthias}, title = {Underapproximative Methods for the Order Reduction of Zonotopes}, volume = {9}, journal = {IEEE Control Systems Letters}, publisher = {IEEE}, address = {New York}, issn = {2475-1456}, doi = {https://doi.org/10.1109/LCSYS.2025.3577642}, pages = {1730 -- 1735}, year = {2025}, abstract = {Zonotopes are a widely used set representation in set-based computations due to their compact representation size and their closure under many relevant set operations. However, certain set operations, such as the Minkowski sum, increase the zonotope order, which in turn increases the computational cost of further computations. To address this issue, various order reduction techniques have been proposed, most of which focus on overapproximating the original zonotope. While overapproximations are crucial for safety verification, some applications - such as reachset-conformant identification and backward reachability analysis - require underapproximations (also referred to as inner-approximations). Besides providing a comprehensive survey of existing underapproximative order reduction methods, we propose four novel reduction methods in this letter. We analyze the computational cost of all methods and evaluate the tightness of the resulting underapproximations through numerical experiments on more than 2000 randomly generated zonotopes. The results demonstrate that our proposed methods achieve a favorable balance between computational efficiency and approximation accuracy, making them well-suited for applications in control, estimation, and system identification.}, language = {en} } @unpublished{KochdumperAlthoff2019, author = {Kochdumper, Niklas and Althoff, Matthias}, title = {Representation of Polytopes as Polynomial Zonotopes}, publisher = {arXiv}, address = {Ithaca}, doi = {https://doi.org/10.48550/arXiv.1910.07271}, year = {2019}, language = {en} } @article{KochdumperAlthoff2020, author = {Kochdumper, Niklas and Althoff, Matthias}, title = {Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis}, volume = {66}, journal = {IEEE Transactions on Automatic Control}, number = {9}, publisher = {IEEE}, address = {New York}, issn = {1558-2523}, doi = {https://doi.org/10.1109/TAC.2020.3024348}, pages = {4043 -- 4058}, year = {2020}, language = {en} } @article{KochdumperAlthoff2023, author = {Kochdumper, Niklas and Althoff, Matthias}, title = {Constrained polynomial zonotopes}, volume = {60}, journal = {Acta Informatica}, number = {3}, publisher = {Springer}, address = {Berlin}, issn = {1432-0525}, doi = {https://doi.org/10.1007/s00236-023-00437-5}, pages = {279 -- 316}, year = {2023}, abstract = {We introduce constrained polynomial zonotopes, a novel non-convex set representation that is closed under linear map, Minkowski sum, Cartesian product, convex hull, intersection, union, and quadratic as well as higher-order maps. We show that the computational complexity of the above-mentioned set operations for constrained polynomial zonotopes is at most polynomial in the representation size. The fact that constrained polynomial zonotopes are generalizations of zonotopes, polytopes, polynomial zonotopes, Taylor models, and ellipsoids further substantiates the relevance of this new set representation. In addition, the conversion from other set representations to constrained polynomial zonotopes is at most polynomial with respect to the dimension, and we present efficient methods for representation size reduction and for enclosing constrained polynomial zonotopes by simpler set representations.}, language = {en} } @article{KochdumperKrasowskiWangetal.2023, author = {Kochdumper, Niklas and Krasowski, Hanna and Wang, Xiao and Bak, Stanley and Althoff, Matthias}, title = {Provably Safe Reinforcement Learning via Action Projection Using Reachability Analysis and Polynomial Zonotopes}, volume = {2}, journal = {IEEE Open Journal of Control Systems}, publisher = {IEEE}, address = {New York}, issn = {2694-085X}, doi = {https://doi.org/10.1109/OJCSYS.2023.3256305}, pages = {79 -- 92}, year = {2023}, abstract = {While reinforcement learning produces very promising results for many applications, its main disadvantage is the lack of safety guarantees, which prevents its use in safety-critical systems. In this work, we address this issue by a safety shield for nonlinear continuous systems that solve reach-avoid tasks. Our safety shield prevents applying potentially unsafe actions from a reinforcement learning agent by projecting the proposed action to the closest safe action. This approach is called action projection and is implemented via mixed-integer optimization. The safety constraints for action projection are obtained by applying parameterized reachability analysis using polynomial zonotopes, which enables to accurately capture the nonlinear effects of the actions on the system. In contrast to other state-of-the-art approaches for action projection, our safety shield can efficiently handle input constraints and dynamic obstacles, eases incorporation of the spatial robot dimensions into the safety constraints, guarantees robust safety despite process noise and measurement errors, and is well suited for high-dimensional systems, as we demonstrate on several challenging benchmark systems.}, language = {en} }