The Orbit Problem consists of determining, given a linear
transformation A on Qd,
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
In this paper, we are concerned with the problem of synthesising suitable invariants P ⊆ Rd, 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 semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
Proceedings of STACS 17, LIPIcs 66, 2017. 13 pages.
© 2017 Nathanaël Fijalkow, Pierre Ohlmann, Joël
Ouaknine, Amaury Pouly, and James Worrell.