Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem
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 concern...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Schloss Dagstuhl
2017
|
| _version_ | 1826262423801167872 |
|---|---|
| author | Fijalkow, N Ohlmann, P Ouaknine, J Pouly, A Worrell, J |
| author_facet | Fijalkow, N Ohlmann, P Ouaknine, J Pouly, A Worrell, J |
| author_sort | Fijalkow, N |
| collection | OXFORD |
| description | 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 ⊆ 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. |
| first_indexed | 2024-03-06T19:35:57Z |
| format | Conference item |
| id | oxford-uuid:1f0cfb5a-f0d9-4858-9d63-8878effe024a |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:35:57Z |
| publishDate | 2017 |
| publisher | Schloss Dagstuhl |
| record_format | dspace |
| spelling | oxford-uuid:1f0cfb5a-f0d9-4858-9d63-8878effe024a2022-03-26T11:19:43ZSemialgebraic invariant synthesis for the Kannan-Lipton Orbit ProblemConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1f0cfb5a-f0d9-4858-9d63-8878effe024aSymplectic Elements at OxfordSchloss Dagstuhl2017Fijalkow, NOhlmann, POuaknine, JPouly, AWorrell, JThe 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 ⊆ 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. |
| spellingShingle | Fijalkow, N Ohlmann, P Ouaknine, J Pouly, A Worrell, J Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title | Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title_full | Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title_fullStr | Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title_full_unstemmed | Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title_short | Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem |
| title_sort | semialgebraic invariant synthesis for the kannan lipton orbit problem |
| work_keys_str_mv | AT fijalkown semialgebraicinvariantsynthesisforthekannanliptonorbitproblem AT ohlmannp semialgebraicinvariantsynthesisforthekannanliptonorbitproblem AT ouakninej semialgebraicinvariantsynthesisforthekannanliptonorbitproblem AT poulya semialgebraicinvariantsynthesisforthekannanliptonorbitproblem AT worrellj semialgebraicinvariantsynthesisforthekannanliptonorbitproblem |