Differential Dynamic Logic for Verifying Parametric Hybrid Systems Export

@incollection{citeulike:5957379, abstract = {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.}, author = {Platzer, Andr\'{e}}, citeulike-article-id = {5957379}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-73099-6_17}, citeulike-linkout-1 = {http://www.springerlink.com/content/m755147247522794}, doi = {10.1007/978-3-540-73099-6_17}, journal = {Automated Reasoning with Analytic Tableaux and Related Methods}, keywords = {dynamic-logic, hybrid-systems, theorem-proving}, pages = {216--232}, posted-at = {2009-10-17 21:15:02}, priority = {2}, title = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems}, url = {http://dx.doi.org/10.1007/978-3-540-73099-6_17}, year = {2007} }

TY - CHAP ID - citeulike:5957379 L3 - citeulike-article-id:5957379 N2 - 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. JF - Automated Reasoning with Analytic Tableaux and Related Methods EP - 232 TI - Differential Dynamic Logic for Verifying Parametric Hybrid Systems SP - 216 KW - dynamic-logic KW - hybrid-systems KW - theorem-proving AU - Platzer, André PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-73099-6_17 ER -