Cargando…

Relational Differential Dynamic Logic

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

Descripción completa

Detalles Bibliográficos
Autores principales: Kolčák, Juraj, Dubut, Jérémy, Hasuo, Ichiro, Katsumata, Shin-ya, Sprunger, David, Yamada, Akihisa
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439732/
http://dx.doi.org/10.1007/978-3-030-45190-5_11
_version_ 1783573039763423232
author Kolčák, Juraj
Dubut, Jérémy
Hasuo, Ichiro
Katsumata, Shin-ya
Sprunger, David
Yamada, Akihisa
author_facet Kolčák, Juraj
Dubut, Jérémy
Hasuo, Ichiro
Katsumata, Shin-ya
Sprunger, David
Yamada, Akihisa
author_sort Kolčák, Juraj
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7439732
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74397322020-08-21 Relational Differential Dynamic Logic Kolčák, Juraj Dubut, Jérémy Hasuo, Ichiro Katsumata, Shin-ya Sprunger, David Yamada, Akihisa Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2020-03-13 /pmc/articles/PMC7439732/ http://dx.doi.org/10.1007/978-3-030-45190-5_11 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Kolčák, Juraj
Dubut, Jérémy
Hasuo, Ichiro
Katsumata, Shin-ya
Sprunger, David
Yamada, Akihisa
Relational Differential Dynamic Logic
title Relational Differential Dynamic Logic
title_full Relational Differential Dynamic Logic
title_fullStr Relational Differential Dynamic Logic
title_full_unstemmed Relational Differential Dynamic Logic
title_short Relational Differential Dynamic Logic
title_sort relational differential dynamic logic
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439732/
http://dx.doi.org/10.1007/978-3-030-45190-5_11
work_keys_str_mv AT kolcakjuraj relationaldifferentialdynamiclogic
AT dubutjeremy relationaldifferentialdynamiclogic
AT hasuoichiro relationaldifferentialdynamiclogic
AT katsumatashinya relationaldifferentialdynamiclogic
AT sprungerdavid relationaldifferentialdynamiclogic
AT yamadaakihisa relationaldifferentialdynamiclogic