@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} } @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} } @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} } @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} } @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{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{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} }