Verification of Continuous Dynamical Systems by Timed Automata

This paper presents a method for abstracting continuous dynamical systems by timed automata. The abstraction is based on partitioning the state space of a dynamical system using positive invariant sets, which form cells that represent locations of a timed automaton. The abstraction is intended to enable formal verification of temporal properties of dynamical systems without simulating any system trajectory, which is currently not possible. Therefore, conditions for obtaining sound, complete, and refinable abstractions are set up. The novelty of the method is the partitioning of the state space, which is generated utilizing sub-level sets of Lyapunov functions, as they are positive invariant sets. It is shown that this partition generates sound and complete abstractions. Furthermore, the complete abstractions can be composed of multiple timed automata, allowing parallelization of the verification process. The proposed abstraction is applied to two examples, which illustrate how sound and complete abstractions are generated and the type of specification we can check. Finally, an example shows how the compositionality of the abstraction can be used to analyze a high-dimensional system.