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

TL;DR

This paper presents algorithms for computing algebraic strongest postconditions and weakest preconditions in polynomial ODE systems, enabling verification of safety assertions expressed as algebraic varieties.

Contribution

It introduces a comprehensive algorithmic framework for algebraic postconditions and preconditions in polynomial ODEs, including practical applications and case studies.

Findings

Algorithm effectively computes algebraic strongest postconditions.

Method can find largest algebraic invariants within a given set.

Demonstrated success on multiple real-world case studies.

Abstract

A system of polynomial ordinary differential equations (ODEs) is specified via a vector of multivariate polynomials, or vector field, $F$. A safety assertion $\psi\rightarrow[F]\phi$ means that the trajectory of the system will lie in a subset $\phi$ (the postcondition) of the state-space, whenever the initial state belongs to a subset $\psi$ (the precondition). We consider the case when $\phi$ and $\psi$ 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 $\psi$. 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 $\psi$, finds the largest subset of polynomials in $P$ implied by $\psi$ (relativized strongest postcondition). Under certain assumptions on $\phi$, this algorithm can also be used to find the largest algebraic invariant included in $\phi$ and the weakest algebraic precondition for $\phi$. Applications to continuous semialgebraic systems are also considered. The effectiveness of the proposed algorithm is demonstrated on several case studies from the literature.