Differential-algebraic dynamic logic for differential-algebraic programs

We generalise dynamic logic to a logic for
differential-algebraic programs, i.e., discrete
programs augmented with first-order
differential-algebraic formulas as continuous evolution
constraints in addition to first-order discrete jump
formulas. These programs characterise interacting
discrete and continuous dynamics of hybrid systems
elegantly and uniformly. For our logic, we introduce a
calculus over real arithmetic with discrete induction
and a new differential induction with which
differential-algebraic programs can be verified by
exploiting their differential constraints algebraically
without having to solve them. We develop the theory of
differential induction and differential refinement and
analyse their deductive power. As a case study, we
present parametric tangential roundabout maneuvers in
air traffic control and prove collision avoidance in
our calculus.

@article{DBLP:journals/logcom/Platzer10,
	pdf = {pub/DAL.pdf},
	ref = {DBLP:conf/tableaux/Platzer07},
	refname = {TABLEAUX'07},
	study = {info/KeYmaera.html#case-studies},
	errata = {pub/DAL-errata.txt},
	author = {['André Platzer']},
	title = {Differential-algebraic Dynamic Logic for
               Differential-algebraic Programs},
	journal = {J. Log. Comput.},
	longjournal = {Journal of Logic and Computation},
	year = {2010},
	volume = {20},
	number = {1},
	pages = {309-352},
	note = {Advance Access published on November 18,
               2008},
	doi = {10.1093/logcom/exn070},
	keywords = {dynamic logic, differential constraints,
               sequent calculus, verification of hybrid
               systems, differential induction,
               theorem proving},
	abstract = {
    We generalise dynamic logic to a logic for
    differential-algebraic programs, i.e., discrete
    programs augmented with first-order
    differential-algebraic formulas as continuous evolution
    constraints in addition to first-order discrete jump
    formulas. These programs characterise interacting
    discrete and continuous dynamics of hybrid systems
    elegantly and uniformly. For our logic, we introduce a
    calculus over real arithmetic with discrete induction
    and a new differential induction with which
    differential-algebraic programs can be verified by
    exploiting their differential constraints algebraically
    without having to solve them. We develop the theory of
    differential induction and differential refinement and
    analyse their deductive power. As a case study, we
    present parametric tangential roundabout maneuvers in
    air traffic control and prove collision avoidance in
    our calculus.}
}