What's decidable about discrete linear dynamical systems?
DOI10.1007/978-3-031-22337-2_2zbMath1528.68228arXiv2206.11412MaRDI QIDQ6113969
Joël Ouaknine, James Worrell, Toghrul Karimov, Edon Kelmendi
Publication date: 10 August 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2206.11412
model checkingorbit probleminvariant generationSkolem problemlinear recurrence sequencesdiscrete linear dynamical systems
Recurrences (11B37) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Attainable sets, reachability (93B03) Symbolic dynamics (37B10)
Cites Work
- Certifying algorithms
- Positivity of third order linear recurrence sequences
- Occurrence of zero in a linear recursive sequence
- First-order orbit queries
- Algebraic model checking for discrete linear dynamical systems
- On multiphase-linear ranking functions
- Positivity of second order linear recurrent sequences
- On the linear ranking problem for integer linear-constraint loops
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Orbits of Linear Maps and Regular Languages
- On the Complexity of the Orbit Problem
- Polynomial-time algorithm for the orbit problem
- Deux propriétés décidables des suites récurrentes linéaires
- O-Minimal Invariants for Discrete-Time Dynamical Systems
- 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
- Positivity Problems for Low-Order Linear Recurrence Sequences
- The orbit problem in higher dimensions
- Ranking Functions for Linear-Constraint Loops
- Approximate Verification of the Symbolic Dynamics of Markov Chains
- Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function
- Termination of Integer Linear Programs
- CONCUR 2005 – Concurrency Theory
- Verification, Model Checking, and Abstract Interpretation
- Equilibrium states and the ergodic theory of Anosov diffeomorphisms
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: What's decidable about discrete linear dynamical systems?
