## Complete semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem

*Nathanaël Fijalkow*, *Pierre Ohlmann*,
*Joël
Ouaknine*, *Amaury Pouly*, and *James Worrell*
The *Orbit Problem* consists of determining, given a matrix
*A* on **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 *invariants*
*P* ⊆ **R**^{d}, 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
succinct invariants of polynomial size.

Our results imply that the class of closed semialgebraic invariants is
*closure-complete*: there exists a closed semialgebraic invariant if
and only if *y* is not in the topological closure of the orbit of *x*
under *A*.

*Theory of Computing Systems*, 2019. 23 pages.

PDF
© 2019 Nathanaël Fijalkow, Pierre Ohlmann, Joël
Ouaknine, Amaury Pouly, and James Worrell.

Imprint / Data Protection