O-Minimal Invariants for Discrete-Time Dynamical Systems
From MaRDI portal
Publication:5002799
DOI10.4230/LIPIcs.ICALP.2018.114zbMath1499.68066arXiv1802.09263OpenAlexW4205250428WikidataQ114820565 ScholiaQ114820565MaRDI QIDQ5002799
Shaull Almagor, Joël Ouaknine, James Worrell, Dmitry Chistikov
Publication date: 28 July 2021
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1802.09263
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Model theory of ordered structures; o-minimality (03C64)
Related Items
Porous invariants, Certifying DFA bounds for recognition and separation, What's decidable about discrete linear dynamical systems?, Certifying inexpressibility, Unnamed Item, Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Termination of linear programs with nonlinear constraints
- Generating all polynomial invariants in simple loops
- Logarithmic forms and group varieties.
- On the Complexity of the Orbit Problem
- Proving non-termination
- Non-linear loop invariant generation using Gröbner bases
- Polynomial-time algorithm for the orbit problem
- On the Positivity Problem for Simple Linear Recurrence Sequences,
- Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences
- Computer Aided Verification
- The Polyhedron-Hitting Problem
- On Termination of Integer Linear Loops
- Positivity Problems for Low-Order Linear Recurrence Sequences
- Static Analysis
- The orbit problem in higher dimensions
- Ranking Functions for Linear-Constraint Loops
- Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function
- Verification, Model Checking, and Abstract Interpretation
- Termination of Integer Linear Programs
- Computer Aided Verification
