Just-in-time Self-Verification of Autonomous Systems (justITSELF)

Mission

Engineers and computer scientists are currently developing autonomous systems whose entire set of behaviors in future, untested situations is unknown: How can a designer foresee all situations that an autonomous road vehicle, a robot in a human environment, an agricultural robot, or an unmanned aerial vehicle will face? Keeping in mind that all these examples are safety-critical, it is irresponsible to deploy such systems without testing all possible situations—this, however, seems impossible since even the most important possible situations are unmanageably many.

We propose a paradigm shift that will make it possible to guarantee safety in unforeseeable situations: Instead of verifying the correctness of a system before deployment, I propose just-in-time verification, a new, to-be-developed verification paradigm where a system continuously checks the correctness of its next action by itself in its current environment (and only in it) in a just-in-time manner. Just-in-time verification will substantially cut development costs, increase the autonomy of systems (e.g., the range of deployment of automated driving systems), and reduce or even eliminate certain liability claims.

Main Objective

Realizing a paradigm shift in formal verification: Instead of formally verify-ing a system before deployment, we develop algorithms for just-in-time verification of autonomous systems in which each action is only executed if it is formally verified during the operation of the system. The envisioned approach continuously repeats this process so that the current situation is always considered, making it possible to react to unexpected situations. These verification algorithms will have to be highly efficient, but they only have to be performed for the current situation (drastically reduced verification space).

Developed Tools and Benchmarks

Competitions

We organize and participate in the following competitions:

Applications (selection)

Selected Publications

2021

Althoff, M.: Guaranteed State Estimation in CORA 2021. Proc. of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), EasyChair, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Althoff, M.; Frehse, G.; Girard, A.: Set Propagation Techniques for Reachability Analysis. Annual Review of Control, Robotics, and Autonomous Systems 4 (1), 2021, 369--395 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Althoff, M.; Rath, J.~J.: Comparison of Guaranteed State Estimators for Linear Time-Invariant Systems. Automatica 130, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Althoff, M.; Ábrahám, E.; Forets, M.; Frehse, G.; Freire, D.; Schilling, C.; Schupp, S.; Wetzlinger, M.: ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Proc. of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), EasyChair, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Gaßmann, Victor; Althoff, Matthias: Verified Polynomial Controller Synthesis for Disturbed Nonlinear Systems. IFAC-PapersOnLine 54 (5), 2021, 85-90 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Gruber, F.; Althoff, M.: Computing safe sets of linear sampled-data systems. IEEE Control Systems Letters 5 (2), 2021, 385-390 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Kochdumper, Niklas and Gruber, Felix and Schürmann, Bastian and Gaßmann, Victor and Klischat, Moritz and Althoff, Matthias: AROC: A Toolbox for Automated Reachset Optimal Controller Synthesis. Proc. of the 24th International Conference on Hybrid Systems: Computation and Control, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Kochdumper, Niklas; Gassert, Philipp; Althoff, Matthias: Verification of Collision Avoidance for CommonRoad Traffic Scenarios. Proc. of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Koschi, Markus; Althoff, Matthias: Set-based Prediction of Traffic Participants Considering Occlusions and Traffic Rules. IEEE Transactions on Intelligent Vehicles 6 (2), 2021, 249-265 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Kulmburg, Adrian; Althoff, Matthias: On the co-NP-Completeness of the Zonotope Containment Problem. European Journal of Control, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Luca Geretti, Julien Alexandre dit Sandretto, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Pieter Collins, Parasara Sridhar Duggirala, Marcelo Forets, Edward Kim, Uziel Linares, David P. Sanders, Christian Schilling, Mark Wetzlinger: ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. Proc. of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21) (EPiC Series in Computing), EasyChair, 2021 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Matthias Althoff, Sebastian Maierhofer, and Christian Pek: Provably-Correct and Comfortable Adaptive Cruise Control. IEEE Transactions on Intelligent Vehicles 6 (1), 2021, 159-174 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Schürmann, Bastian; Althoff, Matthias: Optimizing Sets of Solutions for Controlling Constrained Nonlinear Systems. IEEE Transactions on Automatic Control 66 (3), 2021, 981--994 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)

2020

Alanwar, A.; Said, H.; Mehta, A.; Althoff, M.: Event-Triggered Diffusion Kalman Filters. Proc. of the 11th ACM/IEEE International Conference on Cyber-Physical Systems, 2020 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Althoff, Matthias; Bak, Stanley; Bao, Zongnan; Forets, Marcelo; Frehse, Goran; Freire, Daniel; Kochdumper, Niklas; Li, Yangge; Mitra, Sayan; Ray, Rajarshi; Schilling, Christian; Schupp, Stefan; Wetzlinger, Mark: ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Proc. of the 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair, 2020, 16-48 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Christian Pek, Vitaliy Rusinov, Stefanie Manzinger, Murat Can Üste, and Matthias Althoff: CommonRoad Drivability Checker: Simplifying the Development and Validation of Motion Planning Algorithms. Proc. of the IEEE Intelligent Vehicles Symposium, 2020 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Gaßmann, Victor; Althoff, Matthias: Scalable Zonotope-Ellipsoid Conversions using the Euclidean Zonotope Norm. 2020 American Control Conference (ACC), IEEE, 2020, 4715 - 4721 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Geretti, Luca; Alexandre Dit Sandretto, Julien; Althoff, Matthias; Benet, Luis; Chapoutot, Alexandre; Chen, Xin; Collins, Pieter; Forets, Marcelo; Freire, Daniel; Immler, Fabian; Kochdumper, Niklas; Sanders, David P.; Schilling, Christian: ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. Proc. of the 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair, 2020, 49-75 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Matthias Althoff, Matthias Mayer, Robert Müller: Automatic Synthesis of Human Motion from Temporal Logic Specifications. 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2020 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)

2019

Alanwar, Amr; Said, Hazem; Althoff, Matthias: Distributed Secure State Estimation Using Diffusion Kalman Filters and Reachability Analysis. Proc. of the 58th IEEE Conference on Decsion and Control, 2019 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)
Gruber, F.; Althoff, M.: Scalable robust model predictive control for linear sampled-data systems. IEEE Conference on Decision and Control, 2019, 438-444 mehr… BibTeX Volltext ( DOI ) Volltext (mediaTUM)