2026-07-21T12:28:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3763 2024-03-06T10:29:08Z ddc:004 open_access

Abstracting Continuous Nonpolynomial Dynamical Systems Denman, William Formal Verification Automated Theorem Proving Abstraction Nonpolynomial System MetiTarski The reachability problem, whether some unsafe state can be reached, is known to be undecidable for nonlinear dynamical systems. However, finite-state abstractions have successfully been used for safety verification. This paper presents a method for automatically abstracting nonpolynomial systems that do not have analytical or closed form solutions. The abstraction is constructed by splitting up the state-space using nonpolynomial Lyapunov functions. These functions place guarantees on the behaviour of the system without requiring the explicit calculation of trajectories. MetiTarski, an automated theorem prover for special functions (sin, cos, sqrt, exp) is used to identify possible transitions between the abstract states. The resulting finite-state system is perfectly suited for verification by a model checker. Schloss Dagstuhl – Leibniz-Zentrum für Informatik William Denman 2012 Is Part Of OASIcs, Volume 28, 2012 Imperial College Computing Student Workshop InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICCSW.2012.42 urn:nbn:de:0030-drops-37638 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2012.42 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode