@inproceedings{FijalkowOhlmannOuakninePoulyWorrell17,
  author        = {Nathana{\"{e}}l Fijalkow and
               Pierre Ohlmann and
               Jo{\"{e}}l Ouaknine and
               Amaury Pouly and
               James Worrell},
  title         = {Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem},
  booktitle     = {STACS},
  year          = {2017},
  url           = {https://doi.org/10.4230/LIPIcs.STACS.2017.29},
  doi           = {10.4230/LIPIcs.STACS.2017.29},
  url_Link      = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7005},
  url_Abstract  = {The Orbit Problem consists of determining, given a linear transformation 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.
<br/>
  In this paper, we are concerned with the problem of synthesising suitable invariants P included in 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.
<br/>
  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.},
}

{"_id":"Y3NAp2MsCmeRnv3wq","bibbaseid":"fijalkow-ohlmann-ouaknine-pouly-worrell-semialgebraicinvariantsynthesisforthekannanliptonorbitproblem-2017","downloads":0,"creationDate":"2017-11-28T18:01:09.116Z","title":"Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem","author_short":["Fijalkow, N.","Ohlmann, P.","Ouaknine, J.","Pouly, A.","Worrell, J."],"year":2017,"bibtype":"inproceedings","biburl":"https://nathanael-fijalkow.github.io/perso.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Nathanaël"],"propositions":[],"lastnames":["Fijalkow"],"suffixes":[]},{"firstnames":["Pierre"],"propositions":[],"lastnames":["Ohlmann"],"suffixes":[]},{"firstnames":["Joël"],"propositions":[],"lastnames":["Ouaknine"],"suffixes":[]},{"firstnames":["Amaury"],"propositions":[],"lastnames":["Pouly"],"suffixes":[]},{"firstnames":["James"],"propositions":[],"lastnames":["Worrell"],"suffixes":[]}],"title":"Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem","booktitle":"STACS","year":"2017","url":"https://doi.org/10.4230/LIPIcs.STACS.2017.29","doi":"10.4230/LIPIcs.STACS.2017.29","url_link":"http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7005","url_abstract":"The Orbit Problem consists of determining, given a linear transformation 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. <br/> In this paper, we are concerned with the problem of synthesising suitable invariants P included in 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. <br/> 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.","bibtex":"@inproceedings{FijalkowOhlmannOuakninePoulyWorrell17,\n author = {Nathana{\\\"{e}}l Fijalkow and\n Pierre Ohlmann and\n Jo{\\\"{e}}l Ouaknine and\n Amaury Pouly and\n James Worrell},\n title = {Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem},\n booktitle = {STACS},\n year = {2017},\n url = {https://doi.org/10.4230/LIPIcs.STACS.2017.29},\n doi = {10.4230/LIPIcs.STACS.2017.29},\n url_Link = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7005},\n url_Abstract = {The Orbit Problem consists of determining, given a linear transformation A on Q^d, together with vectors x and y, \n 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.\n<br/>\n In this paper, we are concerned with the problem of synthesising suitable invariants P included in R^d, i.e., sets that are stable under A and contain x and not y, \n thereby providing compact and versatile certificates of non-reachability. \n We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances\n we provide an algorithm to synthesise suitable invariants of polynomial size.\n<br/>\n 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.},\n}\n\n","author_short":["Fijalkow, N.","Ohlmann, P.","Ouaknine, J.","Pouly, A.","Worrell, J."],"key":"FijalkowOhlmannOuakninePoulyWorrell17","id":"FijalkowOhlmannOuakninePoulyWorrell17","bibbaseid":"fijalkow-ohlmann-ouaknine-pouly-worrell-semialgebraicinvariantsynthesisforthekannanliptonorbitproblem-2017","role":"author","urls":{"Paper":"https://doi.org/10.4230/LIPIcs.STACS.2017.29"," link":"http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7005"," abstract":"https://nathanael-fijalkow.github.io/The%20Orbit%20Problem%20consists%20of%20determining,%20given%20a%20linear%20transformation%20A%20on%20Q%5Ed,%20together%20with%20vectors%20x%20and%20y,%20whether%20the%20orbit%20of%20x%20under%20repeated%20applications%20of%20A%20can%20ever%20reach%20y.%20This%20problem%20was%20famously%20shown%20to%20be%20decidable%20by%20Kannan%20and%20Lipton%20in%20the%201980s.%20%3Cbr/%3E%20In%20this%20paper,%20we%20are%20concerned%20with%20the%20problem%20of%20synthesising%20suitable%20invariants%20P%20included%20in%20R%5Ed,%20i.e.,%20sets%20that%20are%20stable%20under%20A%20and%20contain%20x%20and%20not%20y,%20thereby%20providing%20compact%20and%20versatile%20certificates%20of%20non-reachability.%20We%20show%20that%20whether%20a%20given%20instance%20of%20the%20Orbit%20Problem%20admits%20a%20semialgebraic%20invariant%20is%20decidable,%20and%20moreover%20in%20positive%20instances%20we%20provide%20an%20algorithm%20to%20synthesise%20suitable%20invariants%20of%20polynomial%20size.%20%3Cbr/%3E%20It%20is%20worth%20noting%20that%20the%20existence%20of%20semilinear%20invariants,%20on%20the%20other%20hand,%20is%20(to%20the%20best%20of%20our%20knowledge)%20not%20known%20to%20be%20decidable."},"downloads":0,"html":""},"search_terms":["semialgebraic","invariant","synthesis","kannan","lipton","orbit","problem","fijalkow","ohlmann","ouaknine","pouly","worrell"],"keywords":[],"authorIDs":["5a1da46565b42fc01800000f"],"dataSources":["BXc4gcZutK5ptXtTF"]}