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.