Academic
Publications
Differential-algebraic Dynamic Logic for Differential-algebraic Programs

Differential-algebraic Dynamic Logic for Differential-algebraic Programs,10.1093/logcom/exn070,Journal of Logic and Computation,André Platzer

Differential-algebraic Dynamic Logic for Differential-algebraic Programs   (Citations: 15)
BibTex | RIS | RefWorks Download
Journal: Journal of Logic and Computation - LOGCOM , vol. 20, no. 1, pp. 309-352, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Deductive verification of hybrid systems has seen great advancement through a recent series of work by Platzer and his colleagues, including [5, 6]. Their formalism is variations of dynamic logic, augmented with differential equations to incorporate flowdynamics...

    Kohei Suenagaet al. Programming with Infinitesimals: A WHILE-Language for Hybrid System Mo...

    • ...For example, differential-algebraic dynamic logic [17] due to Platzer was invented by extending dynamic logic with continuous statements...
    • ...Unfortunately, the approaches in [20, 9] were discovered in [28, 27, 17] to have certain problems with their soundness, if at the boundary of a CI, f is not strictly inward the invariant set...

    Jiang Liuet al. Computing semi-algebraic invariants for polynomial dynamical systems

    • ...For this purpose, we present a generalization of differential invariants [15, 18, 16]...
    • ...ferential invariant F Differential invariants [15, 18, 16] are formulas F that do not change their truth-value along the dynamics of a differential equation describing a continuous system transition in a hybrid system; see Fig. 2. To prove that F is a differential invariant, it is sufficient to check a condition on the directional derivatives of all terms of the formula [18]...
    • ...plate equations [24, 23], differential invariants [15, 18, 16] and a constraint-based template approach [7]...
    • ...For entry, we use a simplified procedure based on what has been used in classical roundabouts [26, 15]...
    • ...cal proof rules, which we have previously shown to apply to hybrid systems [15]...
    • ...We call formula F in rule DI a quantified differential invariant for quantified differential equation ∀ if (i) � = θ & H. Note that stronger assumptions than H are generally unsound for the premiss of DI; see previous work for details [15, 16]...
    • ...Without a condition like T (i, j), roundabouts can be unsafe [15, 16] so it is crucial that entry establishes it. For a systematic derivation of how to construct T (i, j), we refer to previous work [15, 16]...
    • ...Without a condition like T (i, j), roundabouts can be unsafe [15, 16] so it is crucial that entry establishes it. For a systematic derivation of how to construct T (i, j), we refer to previous work [15, 16]...

    André Platzer. Quantified differential invariants

    • ...In the literature, the Differential Algebraic Dynamic Logic [8] can deal with differential equations through differential invariants...

    Jiang Liuet al. A Calculus for Hybrid CSP

    • ...For systems with more complicated differential equations, so-called differential invariants [5] can be used to verify properties of differential equations when the solution is unknown or undecidable...

    André Platzer. Differential Dynamic Logics

Sort by: