Logical Foundations of Cyber-Physical Systems

Multi-dynamical Systems

Table of Contents
  1. Overview
  2. Multi-dynamical Systems
  3. Selected Publications


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

Tutorial or
Slides or
Intro or
Course or

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

We take a view that we call multi-dynamical systems [10,9], 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.

Tutorial or
Slides or
Intro or
Hybrid or
Dist.Hyb. or
Stoch.Hyb. or

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.

Selected Publications

A brief survey of the logical foundations of cyber-physical systems and multi-dynamical systems can be found in an invited tutorial at LICS'12 [10] and an extended manuscript [9]. 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. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 2015. © The author
    [bib | pdf | doi | arXiv | abstract]

  2. 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'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pages 527-538. Springer, 2015. © Springer-Verlag
    [bib | pdf | doi | slides | poster | tool | abstract]

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

  4. 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. 2015. © Springer-Verlag
    [bib | pdf | doi | abstract]

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

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

  7. André Platzer.
    A Complete Axiomatization of Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-100R, January 2013, extended in revised version from July 2013. Extended version arXiv:1408.1980.
    [bib | pdf | slides | arXiv | abstract]

  8. André Platzer.
    Teaching CPS foundations with contracts.
    First Workshop on Cyber-Physical Systems Education, pages 7-10. 2013.
    [bib | pdf | slides | poster | eprint | course | abstract]

  9. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv:1205.4788, May 2012.
    [bib | pdf | arXiv | abstract]

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

  11. 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, pages 541-550. IEEE 2012. © IEEE
    [bib | pdf | doi | slides | TR | abstract]

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

  13. 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'11, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pages 431-445. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | slides | TR | abstract]

  14. 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, pages 469-483. Springer, 2010. © Springer-Verlag
    [bib | pdf | doi | slides | TR | LMCS'12 | abstract]

  15. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]