Differential dynamic logic for hybrid systems.

Hybrid systems are models for complex physical systems
and are defined as dynamical systems with interacting
discrete transitions and continuous evolutions along
differential equations. With the goal of developing a
theoretical and practical foundation for deductive
verification of hybrid systems, we introduce a dynamic
logic for hybrid programs, which is a program notation
for hybrid systems. As a verification technique that is
suitable for automation, we introduce a free variable
proof calculus with a novel combination of real-valued
free variables and Skolemisation for lifting quantifier
elimination for real arithmetic to dynamic logic. The
calculus is compositional, i.e., it reduces properties
of hybrid programs to properties of their parts. Our
main result proves that this calculus axiomatises the
transition behaviour of hybrid systems completely
relative to differential equations. In a case study
with cooperating traffic agents of the European Train
Control System, we further show that our calculus is
well-suited for verifying realistic hybrid systems with
parametric system dynamics.

@article{DBLP:journals/jar/Platzer08,
	pdf = {https://link.springer.com/content/pdf/10.1007/s10817-008-9103-8.pdf},
	study = {info/KeYmaera.html#case-studies},
	author = {['André Platzer']},
	title = {Differential Dynamic Logic for Hybrid
               Systems.},
	journal = {J. Autom. Reas.},
	longjournal = {Journal of Automated Reasoning},
	year = {2008},
	volume = {41},
	number = {2},
	pages = {143-189},
	doi = {10.1007/s10817-008-9103-8},
	issn = {0168-7433},
	keywords = {dynamic logic, differential equations,
               sequent calculus, axiomatisation, automated
               theorem proving, verification of hybrid
               systems},
	abstract = {
    Hybrid systems are models for complex physical systems
    and are defined as dynamical systems with interacting
    discrete transitions and continuous evolutions along
    differential equations. With the goal of developing a
    theoretical and practical foundation for deductive
    verification of hybrid systems, we introduce a dynamic
    logic for hybrid programs, which is a program notation
    for hybrid systems. As a verification technique that is
    suitable for automation, we introduce a free variable
    proof calculus with a novel combination of real-valued
    free variables and Skolemisation for lifting quantifier
    elimination for real arithmetic to dynamic logic. The
    calculus is compositional, i.e., it reduces properties
    of hybrid programs to properties of their parts. Our
    main result proves that this calculus axiomatises the
    transition behaviour of hybrid systems completely
    relative to differential equations. In a case study
    with cooperating traffic agents of the European Train
    Control System, we further show that our calculus is
    well-suited for verifying realistic hybrid systems with
    parametric system dynamics.
  }
}