Verification of Continuous Dynamical Systems by Timed Automata

Christoffer Sloth, Rafael Wisniewski

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

11 Citationer (Scopus)
575 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
TidsskriftFormal Methods in System Design
Vol/bind39
Udgave nummer1
Sider (fra-til)47–82
Antal sider36
ISSN0925-9856
DOI
StatusUdgivet - aug. 2011

Fingerprint

Timed Automata
Dynamical systems
Dynamical system
Acoustic waves
Lyapunov functions
Invariant Set
Trajectories
Specifications
Partitioning
State Space
Compositionality
Abstraction
Formal Verification
Level Set
Parallelization
Lyapunov Function
High-dimensional
Partition
Trajectory
Specification

Citer dette

@article{fae965d4b0cd46268d38e8fb85c6a932,
title = "Verification of Continuous Dynamical Systems by Timed Automata",
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.",
author = "Christoffer Sloth and Rafael Wisniewski",
year = "2011",
month = "8",
doi = "10.1007/s10703-011-0118-0",
language = "English",
volume = "39",
pages = "47–82",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer",
number = "1",

}

Verification of Continuous Dynamical Systems by Timed Automata. / Sloth, Christoffer; Wisniewski, Rafael.

I: Formal Methods in System Design, Bind 39, Nr. 1, 08.2011, s. 47–82.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Verification of Continuous Dynamical Systems by Timed Automata

AU - Sloth, Christoffer

AU - Wisniewski, Rafael

PY - 2011/8

Y1 - 2011/8

N2 - 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.

AB - 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.

U2 - 10.1007/s10703-011-0118-0

DO - 10.1007/s10703-011-0118-0

M3 - Journal article

VL - 39

SP - 47

EP - 82

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 1

ER -