# On the Underapproximation of Reach Sets of Abstract Continuous-Time Systems

## TL;DR

This paper introduces a new method for proving reachability in abstract continuous-time systems by constructing a suitable superset of the target set, facilitating formal verification in proof assistants.

## Contribution

It proposes a novel approach to approximate reach sets of continuous-time systems using supersets with specific properties, enabling easier formal reasoning.

## Key findings

- Method effectively proves reachability in abstract models
- Applicable to continuous and hybrid dynamical systems
- Facilitates formal verification in proof assistants

## Abstract

We consider the problem of proving that each point in a given set of states ("target set") can indeed be reached by a given nondeterministic continuous-time dynamical system from some initial state. We consider this problem for abstract continuous-time models that can be concretized as various kinds of continuous and hybrid dynamical systems. The approach to this problem proposed in this paper is based on finding a suitable superset S of the target set which has the property that each partial trajectory of the system which lies entirely in S either is defined as the initial time moment, or can be locally extended backward in time, or can be locally modified in such a way that the resulting trajectory can be locally extended back in time. This reformulation of the problem has a relatively simple logical expression and is convenient for applying various local existence theorems and local dynamics analysis methods to proving reachability which makes it suitable for reasoning about the behavior of continuous and hybrid dynamical systems in proof assistants such as Mizar, Isabelle, etc.