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
1980s.
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.
PDF
© 2017 Nathanaël Fijalkow, Pierre Ohlmann, Joël
Ouaknine, Amaury Pouly, and James Worrell.