Relational Differential Dynamic Logic
Juraj Kolˇ c´ ak
1 , J´ er´ emy Dubut
2,3 ,
Ichiro Hasuo
2,4 , Shin-ya Katsumata
2 ,
David Sprunger
2 , and Akihisa Yamada
2
1 LSV, CNRS & ENS Paris-Saclay, Universit´ e Paris-Saclay, Cachan, France
kolcak@lsv.fr
2 National Institute of Informatics, Tokyo, Japan
{dubut,hasuo,s-katsumata,sprunger,akihisayamada}@nii.ac.jp
3 Japanese-French Laboratory for Informatics, CNRS IRL 3527, Tokyo, Japan
4 The Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan
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.
Keywords: hybrid system · cyber-physical system · formal verification
· theorem proving · dynamic logic.
1 Introduction
Hybrid Systems Cyber-physical systems (CPSs) have been studied as a subject in their own right for over a decade, but the rise of automated driving in
the last few years has created a panoply of challenges in the quality assurance of
these systems. In the foreseeable future, millions of cars will be driving on streets
Thanks are due to Stefan Mitsch, Andr´ e Platzer, and Yong Kiam Tan for useful tips
on the KeYmaera X source code; and to Kenji Kamijo, Yoshiyuki Shinya, and Takamasa Suetomi from Mazda Motor Corporation for helpful discussions. The authors
are supported by ERATO HASUO Metamathematics for Systems Design Project
(No. JPMJER1603), JST. I.H. is supported by Grant-in-Aid No. 15KT0012, JSPS.
J.D. is supported by Grant-in-aid No. 19K20215, JSPS. The work was done during
J.K.’s internship at the National Institute of Informatics, Tokyo, Japan.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 191–208, 2020.
https://doi.org/10.1007/978-3-030-45190-5 11
TACAS
Evaluation
Artifact
2020
Accepted
Juraj Kolˇ c´ ak
1 , J´ er´ emy Dubut
2,3 ,
Ichiro Hasuo
2,4 , Shin-ya Katsumata
2 ,
David Sprunger
2 , and Akihisa Yamada
2
1 LSV, CNRS & ENS Paris-Saclay, Universit´ e Paris-Saclay, Cachan, France
kolcak@lsv.fr
2 National Institute of Informatics, Tokyo, Japan
{dubut,hasuo,s-katsumata,sprunger,akihisayamada}@nii.ac.jp
3 Japanese-French Laboratory for Informatics, CNRS IRL 3527, Tokyo, Japan
4 The Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan
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.
Keywords: hybrid system · cyber-physical system · formal verification
· theorem proving · dynamic logic.
1 Introduction
Hybrid Systems Cyber-physical systems (CPSs) have been studied as a subject in their own right for over a decade, but the rise of automated driving in
the last few years has created a panoply of challenges in the quality assurance of
these systems. In the foreseeable future, millions of cars will be driving on streets
Thanks are due to Stefan Mitsch, Andr´ e Platzer, and Yong Kiam Tan for useful tips
on the KeYmaera X source code; and to Kenji Kamijo, Yoshiyuki Shinya, and Takamasa Suetomi from Mazda Motor Corporation for helpful discussions. The authors
are supported by ERATO HASUO Metamathematics for Systems Design Project
(No. JPMJER1603), JST. I.H. is supported by Grant-in-Aid No. 15KT0012, JSPS.
J.D. is supported by Grant-in-aid No. 19K20215, JSPS. The work was done during
J.K.’s internship at the National Institute of Informatics, Tokyo, Japan.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 191–208, 2020.
https://doi.org/10.1007/978-3-030-45190-5 11
TACAS
Evaluation
Artifact
2020
Accepted