Computer Science – Logic in Computer Science
Scientific paper
2011-04-11
Computer Science
Logic in Computer Science
Scientific paper
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 can be checked for invariance along a differential equation just by using their differential structure and without having to solve the differential equation. 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 differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power of differential invariants increases further when adding auxiliary differential variables to the dynamics.
No associations
LandOfFree
The Structure of Differential Invariants and Differential Cut Elimination does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The Structure of Differential Invariants and Differential Cut Elimination, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Structure of Differential Invariants and Differential Cut Elimination will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-58849