STL model checking of continuous and hybrid systems

Hendrik Roehm; Jens Oehlerking; Thomas Heinz; Matthias Althoff

doi:10.1007/978-3-319-46520-3_26

STL model checking of continuous and hybrid systems

Hendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff

Informatics 6 - Associate Professorship of Cyber Physical Systems

Robert Bosch GmbH

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

34 Scopus citations

Abstract

Signal Temporal Logic (STL) is a formalism for reasoning about temporal properties of continuous-time traces of hybrid systems. Previous work on this subject mostly focuses on robust satisfaction of an STL formula for a particular trace. In contrast, we present a method solving the problem of formally verifying an STL formula for continuous and hybrid system models, which exhibit uncountably many traces. We consider an abstraction of a model as an evolution of reachable sets. Through leveraging the representation of the abstraction, the continuoustime verification problem is reduced to a discrete-time problem. For the given abstraction, the reduction to discrete-time and our decision procedure are sound and complete for finitely represented reach sequences and sampled time STL formulas. Our method does not rely on a special representation of reachable sets and thus any reachability analysis tool can be used to generate the reachable sets. The benefit of the method is illustrated on an example from the context of automated driving.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings
Editors	Cyrille Artho, Doron Peled, Axel Legay
Publisher	Springer Verlag
Pages	412-427
Number of pages	16
ISBN (Print)	9783319465197
DOIs	https://doi.org/10.1007/978-3-319-46520-3_26
State	Published - 2016
Event	14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan Duration: 17 Oct 2016 → 20 Oct 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9938 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Country/Territory	Japan
City	Chiba
Period	17/10/16 → 20/10/16

Keywords

Continuous time
Hybrid systems
Model checking
Reachability analysis
Temporal logic

Access to Document

10.1007/978-3-319-46520-3_26

Cite this

Roehm, H., Oehlerking, J., Heinz, T., & Althoff, M. (2016). STL model checking of continuous and hybrid systems. In C. Artho, D. Peled, & A. Legay (Eds.), Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings (pp. 412-427). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9938 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-46520-3_26

Roehm, Hendrik ; Oehlerking, Jens ; Heinz, Thomas et al. / STL model checking of continuous and hybrid systems. Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings. editor / Cyrille Artho ; Doron Peled ; Axel Legay. Springer Verlag, 2016. pp. 412-427 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9e88b277108e4e838379e1406cf612c3,

title = "STL model checking of continuous and hybrid systems",

abstract = "Signal Temporal Logic (STL) is a formalism for reasoning about temporal properties of continuous-time traces of hybrid systems. Previous work on this subject mostly focuses on robust satisfaction of an STL formula for a particular trace. In contrast, we present a method solving the problem of formally verifying an STL formula for continuous and hybrid system models, which exhibit uncountably many traces. We consider an abstraction of a model as an evolution of reachable sets. Through leveraging the representation of the abstraction, the continuoustime verification problem is reduced to a discrete-time problem. For the given abstraction, the reduction to discrete-time and our decision procedure are sound and complete for finitely represented reach sequences and sampled time STL formulas. Our method does not rely on a special representation of reachable sets and thus any reachability analysis tool can be used to generate the reachable sets. The benefit of the method is illustrated on an example from the context of automated driving.",

keywords = "Continuous time, Hybrid systems, Model checking, Reachability analysis, Temporal logic",

author = "Hendrik Roehm and Jens Oehlerking and Thomas Heinz and Matthias Althoff",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 ; Conference date: 17-10-2016 Through 20-10-2016",

year = "2016",

doi = "10.1007/978-3-319-46520-3_26",

language = "English",

isbn = "9783319465197",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "412--427",

editor = "Cyrille Artho and Doron Peled and Axel Legay",

booktitle = "Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings",

}

Roehm, H, Oehlerking, J, Heinz, T & Althoff, M 2016, STL model checking of continuous and hybrid systems. in C Artho, D Peled & A Legay (eds), Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9938 LNCS, Springer Verlag, pp. 412-427, 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17/10/16. https://doi.org/10.1007/978-3-319-46520-3_26

STL model checking of continuous and hybrid systems. / Roehm, Hendrik; Oehlerking, Jens; Heinz, Thomas et al.
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings. ed. / Cyrille Artho; Doron Peled; Axel Legay. Springer Verlag, 2016. p. 412-427 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9938 LNCS).

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

TY - GEN

T1 - STL model checking of continuous and hybrid systems

AU - Roehm, Hendrik

AU - Oehlerking, Jens

AU - Heinz, Thomas

AU - Althoff, Matthias

N1 - Publisher Copyright: © Springer International Publishing AG 2016.

PY - 2016

Y1 - 2016

N2 - Signal Temporal Logic (STL) is a formalism for reasoning about temporal properties of continuous-time traces of hybrid systems. Previous work on this subject mostly focuses on robust satisfaction of an STL formula for a particular trace. In contrast, we present a method solving the problem of formally verifying an STL formula for continuous and hybrid system models, which exhibit uncountably many traces. We consider an abstraction of a model as an evolution of reachable sets. Through leveraging the representation of the abstraction, the continuoustime verification problem is reduced to a discrete-time problem. For the given abstraction, the reduction to discrete-time and our decision procedure are sound and complete for finitely represented reach sequences and sampled time STL formulas. Our method does not rely on a special representation of reachable sets and thus any reachability analysis tool can be used to generate the reachable sets. The benefit of the method is illustrated on an example from the context of automated driving.

AB - Signal Temporal Logic (STL) is a formalism for reasoning about temporal properties of continuous-time traces of hybrid systems. Previous work on this subject mostly focuses on robust satisfaction of an STL formula for a particular trace. In contrast, we present a method solving the problem of formally verifying an STL formula for continuous and hybrid system models, which exhibit uncountably many traces. We consider an abstraction of a model as an evolution of reachable sets. Through leveraging the representation of the abstraction, the continuoustime verification problem is reduced to a discrete-time problem. For the given abstraction, the reduction to discrete-time and our decision procedure are sound and complete for finitely represented reach sequences and sampled time STL formulas. Our method does not rely on a special representation of reachable sets and thus any reachability analysis tool can be used to generate the reachable sets. The benefit of the method is illustrated on an example from the context of automated driving.

KW - Continuous time

KW - Hybrid systems

KW - Model checking

KW - Reachability analysis

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84992493117&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-46520-3_26

DO - 10.1007/978-3-319-46520-3_26

M3 - Conference contribution

AN - SCOPUS:84992493117

SN - 9783319465197

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 412

EP - 427

BT - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings

A2 - Artho, Cyrille

A2 - Peled, Doron

A2 - Legay, Axel

PB - Springer Verlag

T2 - 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016

Y2 - 17 October 2016 through 20 October 2016

ER -

Roehm H, Oehlerking J, Heinz T, Althoff M. STL model checking of continuous and hybrid systems. In Artho C, Peled D, Legay A, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings. Springer Verlag. 2016. p. 412-427. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-46520-3_26

STL model checking of continuous and hybrid systems

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this