# Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

## TL;DR

This paper proves the decidability of synthesizing semialgebraic invariants for the Orbit Problem, providing an algorithm to generate such invariants when they exist, thus advancing verification techniques for linear transformations.

## Contribution

It establishes the decidability of semialgebraic invariant synthesis for the Orbit Problem and offers an algorithm for constructing polynomial-sized invariants in positive cases.

## Key findings

- Decidability of semialgebraic invariant existence for the Orbit Problem.
- Algorithm for synthesizing polynomial-size invariants.
- Contrast with semilinear invariants, whose decidability remains unknown.

## 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} $\mathcal{P} \subseteq \mathbb{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.