Differential-algebraic Dynamic Logic for Differential-algebraic Programs

作者：Platzer Andre^*

来源：Journal of Logic and Computation, 2010, 20(1): 309-352.

DOI：10.1093/logcom/exn070

• Dynamic logic
• differential constraints
• sequent calculus
• verification of hybrid systems
• differential induction
• theorem proving

We generalize dynamic logic to a logic for differential-algebraic (DA) 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 characterize 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 DA 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.

• 出版日期2010-2