Logic for Hybrid Systems

Overview

One of my research interests is the area of hybrid system verification, primarily logical methods for verifying hybrid systems. The behaviour 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 behaviour. Their behaviour combines continuous evolution (called flow) characterised by differential equations and discrete jumps.

Download or Launch KeYmaera

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 behaviour 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, approximation theory.

For verifying hybrid systems, I have developed a famliy of logics, proof calculi, and verification systems:

• differential dynamic logic (dL) for verifying hybrid systems [10]
• quantified differential dynamic logic (QdL) for verifying distributed hybrid systems [2]
• KeYmaera verification tool implementing dL-based verification technology for hybrid systems
• AMC Approximation Refinement Model Checker [15]

See my book [3] for an overview.

Selected Publications

The canonical references on this approach are [10] and [9]. Also see the publication reading guide.

1. 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. 2011.
   [bib | pdf | doi | study]
   
   
2. 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 | TR]
   
   
3. André Platzer.
   Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
   Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
   [bib | book | doi | web]
   
   
4. André Platzer and Edmund M. Clarke.
   Computing differential invariants of hybrid systems as fixedpoints.
   Formal Methods in System Design, 35(1), pages 98-120, 2009. © Springer-Verlag
   [bib | pdf | doi | study]
   
   
5. 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, pages 171-178. Springer, 2008. © Springer-Verlag
   [bib | pdf | doi | slides | tool]
   
   
6. 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, pages 176-189, Springer, 2008. © Springer-Verlag
   [bib | pdf | doi | study | TR]
   
   
7. André Platzer and Edmund M. Clarke.
   Computing Differential Invariants of Hybrid Systems as Fixedpoints.
   School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
   [bib | pdf | study | CAV'08]
   
   
8. 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, pages 646-649. Springer, 2008. © Springer-Verlag
   [bib | pdf | doi]
   
   
9. André Platzer.
   Differential-algebraic dynamic logic for differential-algebraic programs.
   Journal of Logic and Computation, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
   [bib | pdf | doi | example]
   
   
10. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | example]
    
    
11. André Platzer.
    Combining deduction and algebraic constraints for hybrid system analysis.
    In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
    [bib | pdf]
    
    
12. 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, pages 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | example | TR]
    
    
13. 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, pages 457-471. Springer, 2007. © Springer-Verlag
    [bib | pdf | doi | slides | example | TR]
    
    
14. 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, pages 746-749. Springer, 2007. © Springer-Verlag
    [bib | pdf | doi]
    
    
15. André Platzer and Edmund M. Clarke.
    The image computation problem in hybrid systems model checking.
    In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 473-486. Springer, 2007, © Springer-Verlag
    [bib | pdf | doi | slides]
    
    
16. 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]