Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
复制标题
Kannan-Lipton 轨道问题的半代数不变综合
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
J. Worrell
中科院分区：
文献类型：
--
作者：
Nathanaël Fijalkow;Pierre Ohlmann;Joël Ouaknine;Amaury Pouly;J. Worrell
轨道问题包括确定，给定d维有序数Q^d上的线性变换a，以及向量x和y，在a的重复应用下，x的轨道是否能到达y。这个问题在20世纪80年代被坎南和利普顿证明是可决定的。
The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals 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 which are subsets of 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 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.