Implicit semi-algebraic abstraction for polynomial dynamical systems

DOI10.1007/978-3-030-81685-8_25MaRDI QIDQ832202zbMATH OpenOpenAlexFDO

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

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cites work

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

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

Describes a project that uses

Uses Software

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

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)