Andre Platzer - The Structure of Differential Invariants and Differential Cut Elimination

lmcs:809 - Logical Methods in Computer Science, November 21, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:16)2012
The Structure of Differential Invariants and Differential Cut Elimination

Authors: Andre Platzer ORCID-iD

    The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.


    Volume: Volume 8, Issue 4
    Published on: November 21, 2012
    Accepted on: June 25, 2015
    Submitted on: April 10, 2011
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Classical Analysis and ODEs,Mathematics - Dynamical Systems,Mathematics - Logic,math.CA
    Fundings :
      Source : OpenAIRE Research Graph
    • Collaborative Research: Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology; Funder: National Science Foundation; Code: 0926181
    • CAREER: Logical Foundations of Cyber-Physical Systems; Funder: National Science Foundation; Code: 1054246
    • CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid Systems; Funder: National Science Foundation; Code: 0931985

    Linked data

    Source : ScholeXplorer IsReferencedBy ARXIV 1605.00604
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1605.00604
    Source : ScholeXplorer IsReferencedBy DOI 10.1177/0278364917733549
    • 1605.00604
    • 10.48550/arxiv.1605.00604
    • 10.1177/0278364917733549
    • 10.1177/0278364917733549
    • 10.1177/0278364917733549
    Formal verification of obstacle avoidance and navigation of ground robots
    Mitsch, Stefan ; Ghorbal, Khalil ; Vogelbacher, David ; Platzer, André ;

    18 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 647 times.
    This article's PDF has been downloaded 480 times.