%0 Journal Article %A Platzer, Andre %D 2002 %T Differential Dynamic Logic for Verifying Parametric Hybrid Systems %U https://kilthub.cmu.edu/articles/journal_contribution/Differential_Dynamic_Logic_for_Verifying_Parametric_Hybrid_Systems/6604841 %R 10.1184/R1/6604841.v1 %2 https://kilthub.cmu.edu/ndownloader/files/12095261 %K dynamic logic %K sequent calculus %K verification of parametric hybrid systems %K quantifier elimination %X We 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. %I Carnegie Mellon University