Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem

DOI10.1007/S00224-019-09913-3MaRDI QIDQ2321928zbMATH OpenOpenAlexFDO

Authors Nathanaël Fijalkow, Pierre Ohlmann, Amaury Pouly, James Worrell, Joël Ouaknine

Publication date 27 August 2019

Published in Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1701.02162

zbMATH Keywords

verificationinvariantsorbit problemalgebraic computationSkolem problem

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Orbit growth in dynamical systems (37C35) Symmetries and invariants of dynamical systems (37C79)

Abstract: The emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable emph{invariants} $mathcalPsubseteqmathbb{R}^d$, emph{i.e.}, sets that are stable under $A$ and contain $x$ and not $y$, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of emph{semilinear} invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.

Recommendations

• Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• scientific article; zbMATH DE number 7559115
• First-order orbit queries
• Left-eigenvectors are certificates of the Orbit problem
• The orbit problem in higher dimensions

Cites work

• scientific article; zbMATH DE number 3125787 (Why is no real title available?)
• scientific article; zbMATH DE number 4029737 (Why is no real title available?)
• scientific article; zbMATH DE number 4071018 (Why is no real title available?)
• scientific article; zbMATH DE number 3785018 (Why is no real title available?)
• scientific article; zbMATH DE number 1160037 (Why is no real title available?)
• scientific article; zbMATH DE number 3336831 (Why is no real title available?)
• Automata, Languages and Programming
• Polynomial approximations of the relational semantics of imperative programs
• Polynomial-time algorithm for the orbit problem
• Precise interprocedural analysis through linear algebra
• Structure and randomness. Pages from year one of a mathematical blog
• The Complexity of theA B CProblem
• Ultimate positivity is decidable for simple linear recurrence sequences

Cited in

(6)

• scientific article; zbMATH DE number 7559115 (Why is no real title available?)
• First-order orbit queries
• The orbit problem is in the GapL hierarchy
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• On the Monniaux problem in abstract interpretation

This page was built for publication: Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem

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