The vision of the project is to provide an algorithmic framework for the analysis of dynamical and hybrid automata models and corresponding explication mechanisms. While the majority of existing methods and tools for dynamical and hybrid systems rely either on semi-algorithms (without termination guarantees) or on approximation techniques (without guarantees of the correctness of the analysis results), the focus of the project will be on the development of provably correct and terminating exact algorithms. The project will develop new algorithms for the automated generation of safety guarantees in terms of invariants (i. e., logical assertions that hold for all initial states and are preserved under all transitions) and similar types of certificates for other system properties.
Project A1 has been completed at the end of the first funding phase. This line of research is continued in Project A12.
Principal Investigators
