Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem

DOI10.1007/S00224-019-09913-3zbMATH Open1461.37028arXiv1701.02162OpenAlexW2916340081MaRDI QIDQ2321928FDOQ2321928

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

Publication date: 27 August 2019

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Precise interprocedural analysis through linear algebra
• Polynomial-time algorithm for the orbit problem
• Polynomial approximations of the relational semantics of imperative programs
• The Complexity of theA B CProblem
• Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences
• Automata, Languages and Programming

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)