Verification of Continuous Dynamical Systems by Timed Automata

Christoffer Sloth, Rafael Wisniewski

Research output: Contribution to journalJournal articleResearchpeer-review

12 Citations (Scopus)
667 Downloads (Pure)

Abstract

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.
Original languageEnglish
JournalFormal Methods in System Design
Volume39
Issue number1
Pages (from-to)47–82
Number of pages36
ISSN0925-9856
DOIs
Publication statusPublished - Aug 2011

Fingerprint

Dive into the research topics of 'Verification of Continuous Dynamical Systems by Timed Automata'. Together they form a unique fingerprint.

Cite this