Scalable Formal Methods for Cyber-Physical Systems through Generator-Based Set Representations

• Applicant: Professor Dr.-Ing. Matthias Althoff
• Subject Area: Theoretical Computer Science
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 556510606

While methods already exist that can formally verify cyber-physical systems with a mixed discrete/continuous dynamics, their widespread use will only occur if these methods become more scalable. In recent years, many of the biggest pushes towards more scalable approaches originated from new set representations. Based on a recent discovery, we propose novel generator-based set representations. The basis of our to-be-developed set representations is a novel way of representing polytopes. While polytopes have been researched at least since the 19th century, so far, the complexity of the Minkowski sum has been enormous because of the large number of resulting faces. For instance, the number of required vertices is exponential in the dimension of the space. However, our novel set representation makes it possible to compute the Minkowski sum of polytopes with linear complexity with respect to the system dimension. Since the Minkowski sum is a central operation for the formal verification of cyber-physical systems, our novel set representations will make it possible to formally verify systems using polytopes in polynomial time with respect to the system dimension. In particular, this project will research a) scalable set representations that can be customized for different algorithms; b) efficient and tight over-approximations of operations to achieve polynomial complexity with respect to the dimension of the space; and c) efficient order reduction techniques for set representations. The to-be-developed extensions of our new set representation for polytopes will make it possible to represent non-convex sets with holes that inherit the favorable properties for computing Minkowski sums, linear maps, and convex hulls. We will demonstrate our approach not only on ARCH benchmarks, but also on power systems in the CoSES lab at the Technical University of Munich.

• DFG Programme: Research Grants