English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

A system of polynomial ordinary differential equations (ode’s) is specified via a vector of multivariate polynomials, or vector field, F. A safety assertion (psi longrightarrow [F],phi ) means that the system’s trajectory 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 conservation laws implied by (psi ). Checking the validity of algebraic safety assertions is a fundamental problem in, for instance, hybrid systems. We consider generalized versions of this problem, and offer algorithms to: (1) given a user specified polynomial set P and a precondition (psi ), find the smallest algebraic postcondition (phi ) including the variety determined by the valid conservation laws in P (relativized strongest postcondition); (2) given a user specified postcondition (phi ), find the largest algebraic precondition (psi ) (weakest precondition). The first algorithm can also be used to find the weakest algebraic invariant of the system implying all conservation laws in P valid under (psi ). The effectiveness of these algorithms is demonstrated on a challenging case study from the literature.

Complete Algorithms for Algebraic Strongest Postconditions and Weakest Preconditions in Polynomial ODE’S