Logic for Hybrid Systems

Overview

One of my research interests is logic for dynamical systems such as differential dynamic logic for hybrid systems verification. The behavior of safety-critical systems typically depends on both the state of a discrete controller and continuous physical quantities. Hybrid systems are mathematical models for dynamic systems with interacting discrete and continuous behavior. Their behavior combines continuous evolution (called flow) characterized by differential equations and discrete jumps.

⇓ Download ⇓ or get Source or read Book or watch Videos and follow Tutorial

Hybrid systems are a fascinating area of research. Verification methods for hybrid systems involve a large variety of techniques from several areas of mathematics, computer science, and electrical engineering. The challenges imposed by their combined discrete and continuous behavior require quite interesting combinations of "solution" methods from those areas. For example, techniques from the following areas can be used:

logic, theorem proving, model checking, computer algebra, theory of differential equations, differential algebra, model theory, numerical approximations.

There is a family of logics, proof calculi, and hybrid systems verification systems:

• differential dynamic logic (dL) for verifying hybrid systems [7,26]
• quantified differential dynamic logic (QdL) for verifying distributed hybrid systems [14]
• KeYmaera X verification tool implementing dL-based verification technology for hybrid systems, and its predecessor KeYmaera.
• AMC Approximation Refinement Model Checker [2]

Look at a book [13] and textbook [27] for more comprehensive overviews.

Abstract

Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, proof-theoretically, this is not the case. We present a complete proof-theoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments.

Keywords: proof theory, hybrid dynamical systems, differential dynamic logic, axiomatization, completeness

[17]

Selected Publications

The canonical references on this approach are [7,16,17,8,26]. Also see publications on hybrid systems logic and the publication reading guide.

1. André Platzer and Yong Kiam Tan.
   Differential equation invariance axiomatization.
   J. ACM 67(1), 6:1-6:66, 2020. © The authors
   [bib | ⧉ | pdf | doi | mypdf | slides | video | arXiv | LICS'18 | abstract]
   
   
2. 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 | mypdf | slides | video | arXiv | JACM'20 | abstract]
   
   
3. 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]
   
   
4. 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]
   
   
5. 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]
   
   
6. 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]
   
   
7. 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]
   
   
8. 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]
   
   
9. 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]
   
   
10. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2014.
    [bib | ⧉ | pdf | textbook | course]
    
    
11. 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]
    
    
12. 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]
    
    
13. 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]
    
    
14. 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]
    
    
15. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 1181-1186. 2011. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
16. 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]
    
    
17. André Platzer.
    Logical Analysis of Hybrid Systems:
       Proving Theorems for Complex Dynamics.
    Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
    [bib | ⧉ | doi | book | web | errata | abstract]
    
    
18. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    Formal Methods in System Design 35(1), pp. 98-120, 2009.
    Special issue for selected papers from CAV'08. © Springer
    [bib | ⧉ | pdf | doi | study | CAV'08 | abstract]
    
    
19. André Platzer and Jan-David Quesel.
    KeYmaera: A hybrid theorem prover for hybrid systems.
    In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171-178. Springer, 2008. © Springer
    [bib | ⧉ | pdf | doi | slides | tool | abstract]
    
    
20. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176-189, Springer, 2008. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | FMSD'09 | abstract]
    
    
21. André Platzer and Jan-David Quesel.
    Logical verification and systematic parametric analysis in train control.
    In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pp. 646-649. Springer, 2008. © Springer
    [bib | ⧉ | pdf | doi | poster | abstract]
    
    
22. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation 20(1), pp. 309-352, 2010.
    Special issue for selected papers from TABLEAUX'07. © The author
    [bib | ⧉ | pdf | doi | eprint | study | errata | TABLEAUX'07 | abstract]
    
    
23. 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]
    
    
24. André Platzer.
    Combining deduction and algebraic constraints for hybrid system analysis.
    In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
    [bib | ⧉ | pdf | eprint | slides | abstract]
    
    
25. André Platzer.
    Differential dynamic logic for verifying parametric hybrid systems.
    In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pp. 216-232. Springer, 2007. © Springer
    TABLEAUX Best Paper Award.
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
26. André Platzer.
    A temporal dynamic logic for verifying hybrid system invariants.
    In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pp. 457-471. Springer, 2007. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
27. André Platzer.
    Differential logic for reasoning about hybrid systems.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 746-749. Springer, 2007. © Springer
    [bib | ⧉ | pdf | doi | poster | abstract]
    
    
28. André Platzer and Edmund M. Clarke.
    The image computation problem in hybrid systems model checking.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473-486. Springer, 2007, © Springer
    [bib | ⧉ | pdf | doi | slides | tool | abstract]
    
    
29. Stephanie Kemper and André Platzer.
    SAT-based abstraction refinement for real-time systems.
    In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107-122, 2007
    [bib | ⧉ | pdf | doi | slides | tool | abstract]