Loading...
Please wait, while we are loading the content...
Similar Documents
Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs
| Content Provider | arXiv |
|---|---|
| Author | Boreale, Michele |
| Date of Submission | 2020-03-29 |
| 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. |
| Related Links | https://arxiv.org/pdf/1708.05377.pdf |
| Page Count | 19 |
| arXiv | 1708.05377 |
| Language | English |
| Access Restriction | Open |
| Subject Keyword | Computer Science - Logic in Computer Science Specifying and Verifying and Reasoning about Programs Computer Science |
| Content Type | Text |
| Resource Type | Article |
| Subject | Computer Science |
