Multidynamical Systems
Table of Contents 

Overview
Our research develops logical foundations for cyberphysical 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 multidynamical systems, i.e., in terms of the elementary dynamical aspects of their parts. 
Tutorial
or Slides or Intro or Course or Tool 
Hybrid Systems 


Hybrid Games  Stoch. Hyb. Sys. 
Multibillion 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.
Multidynamical 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 crossdepartmental graduate/undergraduate courses on Logical Foundations of CPS as prime examples of STEM integration. Longterm goals include a K12 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 wellintegrated.
Multidynamical Systems
We take a view that we call multidynamical systems [6,7,17], 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 multidynamical systems principle works. Multidynamical systems are dynamical systems that can combine discrete dynamics, continuous dynamics, adversarial dynamics, nondeterministic dynamics, and stochastic dynamics to model cyberphysical systems. Dynamic logics for multidynamical systems capture the foundations and fundamental reasoning principles for those multidynamical systems. 
Tutorial
or Slides or Intro or Hybrid or Hybrid Games or Dist.Hyb. or Stoch.Hyb. or Course 
Selected Publications
A highlevel overview of the principles behind the logical foundations of cyberphysical systems are in an invited IJCAR paper [17]. A technical survey of some aspects of the logical foundations of cyberphysical systems and multidynamical systems can be found in an invited tutorial at LICS'12 [6] and an extended manuscript [7] and in B.EATCS
André Platzer.
Logical Foundations of CyberPhysical Systems.
Invited Talk at HCSS 2014,
Annapolis, MD, May 69, 2014
[slides] 
André Platzer.
Logical Foundations of CyberPhysical Systems.
Invited Talk at NSF CPS Workshop for Aspiring PIs in CyberPhysical Systems 2013
[slides  talk] 
André Platzer.
Logical Foundations of CyberPhysical Systems.
PI Talk at NSF CPS PI Meeting 2013
[slides  talk]

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 2016. © The author
[bib  pdf  doi  arXiv  abstract]

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

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

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2016.
[bib  pdf  course  abstract]

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

Nathan Fulton, Stefan Mitsch, JanDavid 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, pp. 527538. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  poster  tool  abstract]

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, pp. 467481. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  arXiv  abstract]

JanDavid 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. 6791, 2016. © SpringerVerlag
[bib  pdf  doi  abstract]

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

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2014.
[bib  pdf  course  abstract]

André Platzer.
Teaching CPS foundations with contracts.
First Workshop on CyberPhysical Systems Education, pp. 710. 2013.
[bib  pdf  slides  poster  eprint  course  abstract]

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

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

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. 541550. IEEE 2012. © IEEE
[bib  pdf  doi  slides  TR  abstract]

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

André Platzer.
Stochastic differential dynamic logic for stochastic hybrid programs.
In Nikolaj Bjørner and Viorica SofronieStokkermans, editors, International Conference on Automated Deduction, CADE'11, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 431445. Springer, 2011. © SpringerVerlag
[bib  pdf  doi  slides  TR  abstract]

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 2327, 2010. Proceedings, volume 6247 of LNCS, pp. 469483. Springer, 2010. © SpringerVerlag
[bib  pdf  doi  slides  TR  LMCS'12  abstract]

André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning, 41(2), pp. 143189, 2008. © SpringerVerlag
[bib  pdf  doi  study  abstract]