Proofs for an Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions

TL;DR

This paper introduces a method for abstracting continuous dynamical systems into timed automata using Lyapunov functions for partitioning, enabling verification with soundness, completeness, and refinability.

Contribution

It proposes a novel abstraction technique based on Lyapunov functions and proves soundness for Morse-Smale systems and completeness for linear systems.

Findings

Sound abstractions for Morse-Smale systems

Complete and refinable abstractions for linear systems

Partitioning with Lyapunov sub-level sets enhances verification

Abstract

In this report proofs are presented for a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata. To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up. It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are proved.