file.pdf (519.06 kB)
Differential Dynamic Logic for Verifying Parametric Hybrid Systems
journal contribution
posted on 2002-07-01, 00:00 authored by Andre PlatzerWe introduce a first-order dynamic logic for reasoning about
systems with discrete and continuous state transitions, and we present
a sequent calculus for this logic. As a uniform model, our logic supports
hybrid programs with discrete and differential actions. For handling real
arithmetic during proofs, we lift quantifier elimination to dynamic logic.
To obtain a modular combination, we use side deductions for verifying
interacting dynamics. With this, our logic supports deductive verification
of hybrid systems with symbolic parameters and first-order definable
flows. Using our calculus, we prove a parametric inductive safety
constraint for speed supervision in a train control system.