Combinatorial Abstractions of Dynamical Systems

TL;DR

This paper discusses the use of combinatorial abstractions to simplify the verification of dynamical systems, aiming to address the complexity of reachability calculations in safety verification.

Contribution

It introduces indirect verification methods that utilize reduced-complexity models to preserve key properties of dynamical systems for more feasible analysis.

Findings

Abstracted models retain safety properties

Reduced complexity improves verification efficiency

Method applicable to various dynamical systems

Abstract

Formal verification has been successfully developed in computer science for verifying combinatorial classes of models and specifications. In like manner, formal verification methods have been developed for dynamical systems. However, the verification of system properties, such as safety, is based on reachability calculations, which are the sources of insurmountable complexity. This talk addresses indirect verification methods, which are based on abstracting the dynamical systems by models of reduced complexity and preserving central properties of the original systems.