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.
Thanks are due to Stefan Mitsch, André 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.
Chapter PDF
Similar content being viewed by others
References
Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1–21:29 (2017). https://doi.org/10.1145/3110265
Azevedo de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.: Probabilistic Relational Reasoning via Metrics. In: LICS 2019. pp. 1–19. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785715
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) POPL 2004. pp. 14–25. ACM (2004). https://doi.org/10.1145/964001.964003
Bryce, D., Sun, J., Bae, K., Zuliani, P., Wang, Q., Gao, S., Schmarov, F., Kong, S., Chen, W., Tavares, Z.: dReach homepage. http://dreal.github.io/dReach/
Butler, M.J., Abrial, J., Banach, R.: Modelling and Refining Hybrid Systems in Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action Systems to Distributed Systems: The Refinement Approach, pp. 29–42. Chapman and Hall/CRC (2016). https://doi.org/10.1201/b20053-5
Chicone, C.: Ordinary Differential Equations with Applications, Texts in Applied Mathematics, vol. 34. Springer-Verlag New York, 2 edn. (2006)
Fainekos, G.E., Pappas, G.J.: Robustness of Temporal Logic Specifications. In: Havelund, K., Núñez, M., Rosu, G., Wolff, B. (eds.) Formal Approaches to Software Testing and Runtime Verification, First Combined International Workshops, FATES 2006 and RV 2006, Revised Selected Papers. LNCS, vol. 4262, pp. 178–192. Springer (2006). https://doi.org/10.1007/11940197_12
Girard, A., Pappas, G.J.: Approximate Bisimulation: A Bridge Between Computer Science and Control Theory. Eur. J. Control 17(5–6), 568–578 (2011). https://doi.org/10.3166/ejc.17.568-578
Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge, MA, USA (2000)
Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of Hybrid Systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 462–478. Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_34
Liebrenz, T., Herber, P., Glesner, S.: Deductive Verification of Hybrid Control Systems Modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89–105. Springer (2018). https://doi.org/10.1007/978-3-030-02450-5_6
Lindelöf, E.: Sur l’application de la méthode des approximations successives aux équations différentielles ordinaires du premier ordre. Journal de mathématiques pures et appliquées 4e série 10, 117–128 (1894)
Loos, S.M., Platzer, A.: Differential Refinement Logic. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) LICS 2016. pp. 505–514. ACM (2016). https://doi.org/10.1145/2933575.2934555
Mitsch, S., Platzer, A.: The KeYmaera X Proof IDE – Concepts on Usability in Hybrid Systems Theorem Proving. In: Dubois, C., Masci, P., Méry, D. (eds.) F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016). https://doi.org/10.4204/EPTCS.240.5
Platzer, A.: KeYmaera homepage. http://symbolaris.com/info/KeYmaera.html
Platzer, A.: KeYmaera X homepage. http://www.ls.cs.cmu.edu/KeYmaeraX/index.html
Platzer, A.: Differential Dynamic Logic for Hybrid Systems. J. Autom. Reasoning 41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8
Platzer, A.: The Complete Proof Theory of Hybrid Systems. In: LICS 2012. pp. 541–550. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.64
Platzer, A.: A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reasoning 59(2), 219–265 (2017). https://doi.org/10.1007/s10817-016-9385-1
Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018). https://doi.org/10.1007/978-3-319-63588-0
Platzer, A., Tan, Y.K.: Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. In: Dawar, A., Grädel, E. (eds.) LICS 2018. pp. 819–828. ACM (2018). https://doi.org/10.1145/3209108.3209147
Robinson, A.: Non-standard analysis. Princeton University Press (1966).
Suenaga, K., Hasuo, I.: Programming with Infinitesimals: A While-Language for Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 392–403. Springer (2011). https://doi.org/10.1007/978-3-642-22012-8_31
Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard modeling of continuous-time signals. In: Giacobazzi, R., Cousot, R. (eds.) POPL 2013. pp. 417–430. ACM (2013). https://doi.org/10.1145/2429069.2429120
Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 476–493. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4_28
Wolfram Research, Inc.: Mathematica, Version 12.0 (2019), https://www.wolfram.com/mathematica, Champaign, IL
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
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.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Kolčák, J., Dubut, J., Hasuo, I., Katsumata, Sy., Sprunger, D., Yamada, A. (2020). Relational Differential Dynamic Logic. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)