Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs

A system of polynomial ordinary differential equations (ODEs) is specified via a vector of multivariate polynomials, or vector field, F. A safety assertion ψ⟶[F]ϕ means that the trajectory of the system will lie in a subset ϕ (the postcondition) of the state-space, whenever the initial state belongs to a subset ψ (the precondition). We consider the case when ϕ and ψ are algebraic varieties, that is, zero sets of polynomials. In particular, polynomials specifying the postcondition can be seen as a system's conservation laws implied by ψ. Checking the validity of algebraic safety assertions is a fundamental problem in, for instance, hybrid systems. We consider a generalized version of this problem, and offer an algorithm that, given a user specified polynomial set P and an algebraic precondition ψ, finds the largest subset of polynomials in P implied by ψ (relativized strongest postcondition). Under certain assumptions on ϕ, this algorithm can also be used to find the largest algebraic invariant included in ϕ and the weakest algebraic precondition for ϕ. Applications to continuous semialgebraic systems are also considered. The effectiveness of the proposed algorithm is demonstrated on several case studies from the literature.