@article{Boreale:SCP:2020,
    Abstract = {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.},
    Author = {Boreale, Michele},
    File = {Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs - boreale2020 - a.pdf},
    ISSN = {0167-6423},
    Journal = {Science of Computer Programming},
    Keywords = {Ordinary differential equations, Postconditions, Preconditions, Invariants, Gr{\"o}bner bases},
    Pages = {102441},
    Title = {Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial odes},
    URL = {https://www.sciencedirect.com/science/article/pii/S0167642320300514},
    Volume = {193},
    Year = {2020},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0167642320300514},
    bdsk-url-2 = {https://doi.org/10.1016/j.scico.2020.102441},
    date-added = {2023-03-25 19:18:08 +0100},
    date-modified = {2023-04-06 07:23:45 +0200},
    doi = {10.1016/j.scico.2020.102441}
}

@article{Boreale:SCP:2020, Abstract = {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.}, Author = {Boreale, Michele}, File = {Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs - boreale2020 - a.pdf}, ISSN = {0167-6423}, Journal = {Science of Computer Programming}, Keywords = {Ordinary differential equations, Postconditions, Preconditions, Invariants, Gr{\"o}bner bases}, Pages = {102441}, Title = {Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial odes}, URL = {https://www.sciencedirect.com/science/article/pii/S0167642320300514}, Volume = {193}, Year = {2020}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0167642320300514}, bdsk-url-2 = {https://doi.org/10.1016/j.scico.2020.102441}, date-added = {2023-03-25 19:18:08 +0100}, date-modified = {2023-04-06 07:23:45 +0200}, doi = {10.1016/j.scico.2020.102441} }