Relational differential dynamic logic

Juraj Kolčák; Jérémy Dubut; Ichiro Hasuo; Shin ya Katsumata; David Sprunger; Akihisa Yamada

doi:10.1007/978-3-030-45190-5_11

Relational differential dynamic logic

Juraj Kolčák
, Jérémy Dubut
, Ichiro Hasuo
, Shin ya Katsumata
, David Sprunger
, Akihisa Yamada

Université Paris
National Institute of Informatics (NII)
CNRS UMI3527
The Graduate University for Advanced Studies

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

5 Citations (Scopus)

Abstract

In the field of quality assurance of hybrid systems, Platzer’s differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as “an earlier engagement of the emergency brake yields a smaller collision speed.” A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings
Editors	Armin Biere, David Parker
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	191-208
Number of pages	18
ISBN (Print)	9783030451899
DOIs	https://doi.org/10.1007/978-3-030-45190-5_11
Publication status	Published - 1 Jan 2020
Externally published	Yes
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020

Publication series

Name	Lecture Notes in Computer Science
Volume	12078 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Keywords

cyber-physical system
dynamic logic
formal verification
hybrid system
theorem proving

Access to Document

10.1007/978-3-030-45190-5_11

Cite this

Kolčák, J., Dubut, J., Hasuo, I., Katsumata, S. Y., Sprunger, D., & Yamada, A. (2020). Relational differential dynamic logic. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 191-208). (Lecture Notes in Computer Science; Vol. 12078 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-45190-5_11

Kolčák, Juraj ; Dubut, Jérémy ; Hasuo, Ichiro et al. / Relational differential dynamic logic. Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings. editor / Armin Biere ; David Parker. Springer Science and Business Media Deutschland GmbH, 2020. pp. 191-208 (Lecture Notes in Computer Science).

@inproceedings{25b21e70cfd84ca18a5e684a1560c168,

title = "Relational differential dynamic logic",

abstract = "In the field of quality assurance of hybrid systems, Platzer{\textquoteright}s differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as {\textquotedblleft}an earlier engagement of the emergency brake yields a smaller collision speed.{\textquotedblright} A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.",

keywords = "cyber-physical system, dynamic logic, formal verification, hybrid system, theorem proving",

author = "Juraj Kol{\v c}{\'a}k and J{\'e}r{\'e}my Dubut and Ichiro Hasuo and Katsumata, \{Shin ya\} and David Sprunger and Akihisa Yamada",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).; 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

year = "2020",

month = jan,

day = "1",

doi = "10.1007/978-3-030-45190-5\_11",

language = "English",

isbn = "9783030451899",

series = "Lecture Notes in Computer Science",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "191--208",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings",

}

Kolčák, J, Dubut, J, Hasuo, I, Katsumata, SY, Sprunger, D & Yamada, A 2020, Relational differential dynamic logic. in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings. Lecture Notes in Computer Science, vol. 12078 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 191-208, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45190-5_11

Relational differential dynamic logic. / Kolčák, Juraj; Dubut, Jérémy; Hasuo, Ichiro et al.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings. ed. / Armin Biere; David Parker. Springer Science and Business Media Deutschland GmbH, 2020. p. 191-208 (Lecture Notes in Computer Science; Vol. 12078 LNCS).

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

TY - GEN

T1 - Relational differential dynamic logic

AU - Kolčák, Juraj

AU - Dubut, Jérémy

AU - Hasuo, Ichiro

AU - Katsumata, Shin ya

AU - Sprunger, David

AU - Yamada, Akihisa

PY - 2020/1/1

Y1 - 2020/1/1

N2 - In the field of quality assurance of hybrid systems, Platzer’s differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as “an earlier engagement of the emergency brake yields a smaller collision speed.” A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

AB - In the field of quality assurance of hybrid systems, Platzer’s differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as “an earlier engagement of the emergency brake yields a smaller collision speed.” A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

KW - cyber-physical system

KW - dynamic logic

KW - formal verification

KW - hybrid system

KW - theorem proving

UR - https://www.scopus.com/pages/publications/85083991430

U2 - 10.1007/978-3-030-45190-5_11

DO - 10.1007/978-3-030-45190-5_11

M3 - Conference contribution

AN - SCOPUS:85083991430

SN - 9783030451899

T3 - Lecture Notes in Computer Science

SP - 191

EP - 208

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings

A2 - Biere, Armin

A2 - Parker, David

PB - Springer Science and Business Media Deutschland GmbH

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Kolčák J, Dubut J, Hasuo I, Katsumata SY, Sprunger D, Yamada A. Relational differential dynamic logic. In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 191-208. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-45190-5_11

Relational differential dynamic logic

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this