A1 – Analysing and Explicating Dynamical and Hybrid Systems

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.

Principal Investigators

Principal Investigator
Max Planck Institute for Software Systems
Principal Investigator
Technische Universität Dresden

Researchers

Florian Funke
( , , )
Simon Jantsch
( , )
Toghrul Karimov
( )
Engel Lefaucheux
( )
Eike Neumann
( )
David Purser
( )
Markus Whiteland
( )

Publications

View all Publications
Loading Data...