Implicit semi-algebraic abstraction for polynomial dynamical systems

DOI10.1007/978-3-030-81685-8_25zbMATH Open1493.68217OpenAlexW3186194270MaRDI QIDQ832202FDOQ832202

Authors: Sergio Mover, Alberto Griggio, Ahmed Irfan, Stefano Tonetta, Alessandro Cimatti 

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_25

Recommendations

• Complete abstractions of dynamical systems by timed automata
• A method for invariant generation for polynomial continuous systems
• scientific article; zbMATH DE number 2085344
• Deductive verification of continuous dynamical systems
• Algorithms for exact and approximate linear abstractions of polynomial continuous systems

Mathematics Subject Classification ID

Nonlinear ordinary differential equations and systems (34A34) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• The MathSAT5 SMT solver
• Differential dynamic logic for hybrid systems
• Integrability and nonintegrability of dynamical systems
• Title not available (Why is that?)
• Infinite-state invariant checking with IC3 and predicate abstraction
• Predicate abstraction for software verification
• Computing differential invariants of hybrid systems as fixed points
• Abstractions for hybrid systems
• A symbolic approach to predicate abstraction.
• Barrier certificates for nonlinear model validation
• Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
• A method for invariant generation for polynomial continuous systems
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions

Cited In (4)

• Abstract simulation of reaction networks via Boolean networks
• Complete abstractions of dynamical systems by timed automata
• Order-reduction abstractions for safety verification of high-dimensional linear systems
• Algorithms for exact and approximate linear abstractions of polynomial continuous systems

Uses Software

• SymPy
• KeYmaera
• z3
• MathSAT5
• PySMT
• CTIGAR
• KeYmaera X

This page was built for publication: Implicit semi-algebraic abstraction for polynomial dynamical systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832202)