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...
Autores principales: | , , , , , |
---|---|
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 |