dW differential weakening tries proving the postcondition P
of a
differential equation system [{x'=f(x) & Q}]P
from its evolution domain constraint Q
by reducing it to Q→P
.
If this succeeds, the property is independent of x′=f(x)
.
See also
R
is an invariant of the
differential equation system.Learning resources