Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

Rebekah Carter; Eva M. Navarro-López

doi:10.1007/978-3-642-33365-1_6

Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

We look at the problem of proving inevitability of continuous dynamical systems. An inevitability property says that a region of the state space will eventually be reached: this is a type of liveness property from the computer science viewpoint, and is related to attractivity of sets in dynamical systems. We consider a method of Maler and Batt to make an abstraction of a continuous dynamical system to a timed automaton, and show that a potentially infinite number of splits will be made if the splitting of the state space is made arbitrarily. To solve this problem, we define a method which creates a finite-sized timed automaton abstraction for a class of linear dynamical systems, and show that this timed abstraction proves inevitability. © 2012 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Place of Publication	Berlin, Heidelberg
Publisher	Springer Nature
Pages	59-74
Number of pages	15
Volume	7595
ISBN (Print)	9783642333644
DOIs	https://doi.org/10.1007/978-3-642-33365-1_6
Publication status	Published - 2012
Event	10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 - London Duration: 1 Jul 2012 → … http://www.springerlink.com/content/yj5744782834104r/

Conference

Conference	10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
City	London
Period	1/07/12 → …
Internet address	http://www.springerlink.com/content/yj5744782834104r/

Keywords

Abstraction
Automated verification
Continuous-time systems
Liveness properties
Timed automata

Access to Document

10.1007/978-3-642-33365-1_6

Cite this

Carter, R., & Navarro-López, E. M. (2012). Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. (Vol. 7595, pp. 59-74). Springer Nature. https://doi.org/10.1007/978-3-642-33365-1_6

@inproceedings{65476a27889047ec8a50e5b0ae6dc71c,

title = "Dynamically-driven timed automaton abstractions for proving liveness of continuous systems",

abstract = "We look at the problem of proving inevitability of continuous dynamical systems. An inevitability property says that a region of the state space will eventually be reached: this is a type of liveness property from the computer science viewpoint, and is related to attractivity of sets in dynamical systems. We consider a method of Maler and Batt to make an abstraction of a continuous dynamical system to a timed automaton, and show that a potentially infinite number of splits will be made if the splitting of the state space is made arbitrarily. To solve this problem, we define a method which creates a finite-sized timed automaton abstraction for a class of linear dynamical systems, and show that this timed abstraction proves inevitability. {\textcopyright} 2012 Springer-Verlag.",

keywords = "Abstraction, Automated verification, Continuous-time systems, Liveness properties, Timed automata",

author = "Rebekah Carter and Navarro-L{\'o}pez, {Eva M.}",

note = "RCUK,EPSRC; 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 ; Conference date: 01-07-2012",

year = "2012",

doi = "10.1007/978-3-642-33365-1_6",

language = "English",

isbn = "9783642333644",

volume = "7595",

pages = "59--74",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

url = "http://www.springerlink.com/content/yj5744782834104r/",

}

Carter, R & Navarro-López, EM 2012, Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 7595, Springer Nature, Berlin, Heidelberg, pp. 59-74, 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012, London, 1/07/12. https://doi.org/10.1007/978-3-642-33365-1_6

Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. / Carter, Rebekah; Navarro-López, Eva M.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 7595 Berlin, Heidelberg: Springer Nature, 2012. p. 59-74.

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

AU - Carter, Rebekah

AU - Navarro-López, Eva M.

N1 - RCUK,EPSRC

PY - 2012

Y1 - 2012

N2 - We look at the problem of proving inevitability of continuous dynamical systems. An inevitability property says that a region of the state space will eventually be reached: this is a type of liveness property from the computer science viewpoint, and is related to attractivity of sets in dynamical systems. We consider a method of Maler and Batt to make an abstraction of a continuous dynamical system to a timed automaton, and show that a potentially infinite number of splits will be made if the splitting of the state space is made arbitrarily. To solve this problem, we define a method which creates a finite-sized timed automaton abstraction for a class of linear dynamical systems, and show that this timed abstraction proves inevitability. © 2012 Springer-Verlag.

AB - We look at the problem of proving inevitability of continuous dynamical systems. An inevitability property says that a region of the state space will eventually be reached: this is a type of liveness property from the computer science viewpoint, and is related to attractivity of sets in dynamical systems. We consider a method of Maler and Batt to make an abstraction of a continuous dynamical system to a timed automaton, and show that a potentially infinite number of splits will be made if the splitting of the state space is made arbitrarily. To solve this problem, we define a method which creates a finite-sized timed automaton abstraction for a class of linear dynamical systems, and show that this timed abstraction proves inevitability. © 2012 Springer-Verlag.

KW - Abstraction

KW - Automated verification

KW - Continuous-time systems

KW - Liveness properties

KW - Timed automata

U2 - 10.1007/978-3-642-33365-1_6

DO - 10.1007/978-3-642-33365-1_6

M3 - Conference contribution

SN - 9783642333644

VL - 7595

SP - 59

EP - 74

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

CY - Berlin, Heidelberg

T2 - 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012

Y2 - 1 July 2012

ER -

Carter R, Navarro-López EM. Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 7595. Berlin, Heidelberg: Springer Nature. 2012. p. 59-74 doi: 10.1007/978-3-642-33365-1_6

Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this