Logical Foundations of Cyber-Physical Systems

  1. Home
    2. >>
  2. Research
    3. >>
  3. Log.Found.CPS

Logic of
Multi-dynamical Systems

Table of Contents
  1. Overview
  2. Multi-dynamical Systems
  3. Selected Publications
Textbook: Logical Foundations of Cyber-Physical Systems

Overview

My research develops logical foundations for cyber-physical systems (CPS), i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound. Ensuring their correct functioning, however, is a serious challenge. Scientists and engineers need analytic tools to understand and predict the behavior of their systems. That's the key to designing smart and reliable control.

By providing such analytic foundations, this research addresses an intellectual grand challenge that has substantial scientific, economical, societal, and educational impact arising from the benefits of improved CPS analysis and design. In order to tame their complexity, we study CPS as multi-dynamical systems, i.e., in terms of the elementary dynamical aspects of their parts.

Mission or
Slides or
Tutorial or
Book or
Course or
Tool
Hybrid Systems
Hybrid Systems combine discrete dynamics with continuous dynamics Hybrid Games combine discrete dynamics with continuous dynamics and adversarial dynamics Stochastic Hybrid Systems combine discrete dynamics with continuous dynamics and stochastic dynamics Continous Systems can be modeled by differential equations and proved by differential invariants Discrete Systems are well-studied in the form of conventional computer programs Nondeterministic effects in multi-dynamical systems
Hybrid Games Stoch. Hyb. Sys.

Multi-billion dollar industries spend 50% of the development cost on control software design and testing. This cannot be sustained any longer. The foundations of computer science have revolutionized our society. We need even stronger foundations when software reaches out into our physical world.

Multi-dynamical systems are a unifying principle for education and enable students to focus on one dynamical aspect at a time without missing the big picture. They overcome the divide between computer science and engineering that keeps causing unreconcilable differences among design teams. This project develops cross-departmental graduate/undergraduate courses on Logical Foundations of CPS as prime examples of STEM integration. Long-term goals include a K-12 outreach that inspires the youth to pursue science careers with an early exposure to mathematical beauty and exciting societal challenges. CPS foundations excel in demonstrating the paramount importance of discrete and continuous mathematics, not even as separate disciplines, but well-integrated.

Multi-dynamical Systems

This research takes a view that we call multi-dynamical systems [6,7,16], i.e., the principle to understand complex systems as a combination of multiple elementary dynamical aspects. This approach helps us tame the complexity of complex systems by understanding that their complexity just comes from combining lots of simple dynamical aspects with one another. The overall system itself is still as complicated as the whole application. But since differential dynamic logics and proofs are compositional, we can leverage the fact that the individual parts of a system are simpler than the whole, and we can prove correctness properties about the whole system by reduction to simpler proofs about their parts. This approach demonstrates that the whole can be greater than the sum of all parts. The whole system is complicated, but we can still tame its complexity by an analysis of its parts, which are simpler. Completeness results are the theoretical justification why this multi-dynamical systems principle works.

Multi-dynamical systems are dynamical systems that can combine discrete dynamics, continuous dynamics, adversarial dynamics, nondeterministic dynamics, and stochastic dynamics to model cyber-physical systems. Dynamic logics for multi-dynamical systems capture the foundations and fundamental reasoning principles for those multi-dynamical systems.

Tutorial or
Slides or
Intro or
Book or
Hybrid or
Hybrid Games or
Dist.Hyb. or
Stoch.Hyb. or
Course

Selected Publications

A very readable comprehensive resource on the Logical Foundations of Cyber-Physical Systems can be found in the textbook [20] of the same name. A high-level overview of the underlying principles are in an invited IJCAR'16 paper [16]. A good technical survey of several aspects of the logical foundations of cyber-physical systems and multi-dynamical systems can be found in an invited tutorial at LICS'12 [6] and an extended manuscript [7] and in B.EATCS [10]. Main technical developments of core multi-dynamical systems are in the literature [1,4,5,14,17,23,27,31]. Also see publications by area and the publication reading guide. Many other papers develop part of the logical foundations of cyber-physical systems. See complete list of publications.

  1. Yong Kiam Tan and André Platzer.
    An axiomatic approach to existence and liveness for differential equations.
    Formal Aspects of Computing 33(4), pp. 461-518, 2021.
    Special issue for selected papers from FM'19. © The authors
    [bib | ⧉ | pdf | doi | arXiv | FM'19 | abstract]

  2. Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
    Pegasus: Sound continuous invariant generation.
    Formal Methods in System Design 58(1), pp. 5-41, 2022.
    Special issue for selected papers from FM'19. © The authors
    [bib | ⧉ | pdf | doi | tool | arXiv | FM'19 | abstract]

  3. Brandon Bohrer and André Platzer.
    Refining constructive hybrid games.
    In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29 - July 5, Paris, France, Proceedings, volume 167 of LIPIcs, pp. 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]

  4. Brandon Bohrer and André Platzer.
    Constructive hybrid games.
    In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454-473. Springer 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]

  5. André Platzer and Yong Kiam Tan.
    Differential equation invariance axiomatization.
    J. ACM 67(1), 6:1-6:66, 2020. © The authors
    [bib | ⧉ | pdf | doi | slides | video | arXiv | LICS'18 | abstract]

  6. Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
    Pegasus: A framework for sound continuous invariant generation.
    In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods - The Next 30 Years, volume 11800 of LNCS, pp. 138-157. Springer, 2019. © Springer
    FM Best Tool Paper Award.
    [bib | ⧉ | pdf | doi | slides | tool | FMSD'22 | abstract]

  7. André Platzer.
    Uniform substitution at one fell swoop.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019. © The author
    [bib | ⧉ | pdf | doi | mypdf | slides | Isabelle | arXiv | errata | abstract]

  8. Brandon Bohrer and André Platzer.
    A hybrid, dynamic logic for hybrid-dynamic information flow.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 115-124. ACM 2018. © The authors. Publication rights licensed to ACM
    [bib | ⧉ | pdf | doi | slides | TR | abstract]

  9. André Platzer and Yong Kiam Tan.
    Differential equation axiomatization:
       The impressive power of differential ghosts.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819-828. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | slides | video | arXiv | JACM'20 | abstract]

  10. André Platzer.
    Uniform substitution for differential game logic.
    In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, Oxford, UK, Proceedings, volume 10900 of LNCS, pp. 211-227. Springer 2018. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv | abstract]

  11. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
    VeriPhy: Verified controller executables from verified cyber-physical system models.
    In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617-630. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | slides | video | abstract]

  12. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ⧉ | doi | slides | video | book | web | errata | abstract]

  13. Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
    Bellerophon: Tactical theorem proving for hybrid systems.
    In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. Springer, 2017. © Springer
    [bib | ⧉ | pdf | doi | slides | kyx | abstract]

  14. André Platzer.
    Differential hybrid games.
    ACM Trans. Comput. Log. 18(3), pp. 19:1-19:44, 2017. © The author
    [bib | ⧉ | pdf | doi | arXiv | abstract]

  15. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning 59(2), pp. 219-265, 2017. © The author
    [bib | ⧉ | pdf | doi | mypdf | arXiv | abstract]

  16. André Platzer.
    Logic & proofs for cyber-physical systems.
    In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 15-21. Springer, 2016. © Springer
    Invited paper.
    [bib | ⧉ | pdf | doi | slides | abstract]

  17. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    Formal Methods in System Design 49(1), pp. 33-74. 2016.
    Special issue for selected papers from RV'14. © The authors
    [bib | ⧉ | pdf | doi | mypdf | RV'14 | abstract]

  18. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. © The author
    [bib | ⧉ | pdf | doi | arXiv | errata | abstract]

  19. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer.
    KeYmaera X: An aXiomatic tactical theorem prover for hybrid systems.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | poster | tool | tooldoi | abstract]

  20. André Platzer.
    A uniform substitution calculus for differential dynamic logic.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467-481. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv | JAR'17 | abstract]

  21. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
    How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
    STTT 18(1), pp. 67-91, 2016. © The authors
    [bib | ⧉ | pdf | doi | mypdf | abstract]

  22. André Platzer.
    Analog and hybrid computation: Dynamical systems and programming languages.
    Bulletin of the EATCS 114, 2014. © The author
    Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
    [bib | ⧉ | pdf | eprint | abstract]

  23. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2014.
    [bib | ⧉ | pdf | textbook | course]

  24. André Platzer.
    Teaching CPS foundations with contracts.
    First Workshop on Cyber-Physical Systems Education (CPS-Ed 2013), pp. 7-10. 2013.
    [bib | ⧉ | pdf | eprint | slides | poster | course | abstract]

  25. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
    [bib | ⧉ | pdf | arXiv | LICS'12 | abstract]

  26. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | ⧉ | pdf | doi | slides | abstract]

  27. André Platzer.
    The complete proof theory of hybrid systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541-550. IEEE 2012. © IEEE
    [bib | ⧉ | pdf | doi | slides | TR | abstract]

  28. André Platzer.
    A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
    Logical Methods in Computer Science 8(4), pp. 1-44, 2012.
    Special issue for selected papers from CSL'10. © The author
    [bib | ⧉ | pdf | doi | arXiv | CSL'10 | abstract]

  29. André Platzer.
    Stochastic differential dynamic logic for stochastic hybrid programs.
    In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE-23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446-460. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | abstract]

  30. André Platzer.
    Quantified differential dynamic logic for distributed hybrid systems.
    In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | LMCS'12 | abstract]

  31. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning 41(2), pp. 143-189, 2008. © The author
    [bib | ⧉ | pdf | doi | mypdf | study | abstract]

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.

Copyright © by André Platzer        Last modified: 2023-11-29

Publications | Research | Tools | Courses | A. Platzer