TY - GEN
T1 - Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
AU - Fijalkow, Nathanaël
AU - Ohlmann, Pierre
AU - Ouaknine, Joël
AU - Pouly, Amaury
AU - Worrell, James
N1 - Publisher Copyright:
© Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell.
PY - 2017/3/1
Y1 - 2017/3/1
N2 - The Orbit Problem consists of determining, given a linear transformation A on ℚ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 ⊆ ℝ, 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.
AB - The Orbit Problem consists of determining, given a linear transformation A on ℚ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 ⊆ ℝ, 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.
KW - Algebraic computation
KW - Invariants
KW - Orbit Problem
KW - Skolem Problem
KW - Verification
UR - https://www.scopus.com/pages/publications/85016169223
U2 - 10.4230/LIPIcs.STACS.2017.29
DO - 10.4230/LIPIcs.STACS.2017.29
M3 - Conference contribution
AN - SCOPUS:85016169223
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017
A2 - Vallee, Brigitte
A2 - Vollmer, Heribert
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017
Y2 - 8 March 2017 through 11 March 2017
ER -