{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:55:47Z","timestamp":1743090947001,"version":"3.37.3"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,2,26]],"date-time":"2019-02-26T00:00:00Z","timestamp":1551139200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100012338","name":"Alan Turing Institute","doi-asserted-by":"crossref","award":["EP\/N510129\/1"],"award-info":[{"award-number":["EP\/N510129\/1"]}],"id":[{"id":"10.13039\/100012338","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["648701"],"award-info":[{"award-number":["648701"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N008197\/1"],"award-info":[{"award-number":["EP\/N008197\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2019,7]]},"DOI":"10.1007\/s00224-019-09913-3","type":"journal-article","created":{"date-parts":[[2019,2,26]],"date-time":"2019-02-26T07:37:49Z","timestamp":1551166669000},"page":"1027-1048","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-4680","authenticated-orcid":false,"given":"Nathana\u00ebl","family":"Fijalkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Ohlmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amaury","family":"Pouly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,26]]},"reference":[{"key":"9913_CR1","volume-title":"Real Algebraic Geometry, Volume 36 of A Series of Modern Surveys in Mathematics","author":"J Bochnak","year":"1998","unstructured":"Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry, Volume 36 of A Series of Modern Surveys in Mathematics. Springer, Berlin (1998)"},{"unstructured":"Cai, J.-Y.: Computing Jordan Normal Forms Exactly for Commuting Matrices in Polynomial Time. Technical report, SUNY at Buffalo (2000)","key":"9913_CR2"},{"key":"9913_CR3","volume-title":"An Introduction to Diophantine Approximation","author":"JWS Cassels","year":"1965","unstructured":"Cassels, J.W.S.: An Introduction to Diophantine Approximation. Cambridge University Press, Cambridge (1965)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM Press (1978)","key":"9913_CR4","DOI":"10.1145\/512760.512770"},{"issue":"6","key":"9913_CR5","doi-asserted-by":"publisher","first-page":"1878","DOI":"10.1137\/S0097539794276853","volume":"29","author":"J-Y Cai","year":"2000","unstructured":"Cai, J.-Y., Lipton, R.J., Zalcstein, Y.: The complexity of the A B C problem. SIAM J. Comput. 29(6), 1878\u20131888 (2000)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9913_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.scico.2006.03.004","volume":"64","author":"M Col\u00f3n","year":"2007","unstructured":"Col\u00f3n, M.: Polynomial approximations of the relational semantics of imperative programs. Sci. Comput. Program. 64(1), 76\u201396 (2007)","journal-title":"Sci. Comput. Program."},{"key":"9913_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525919","volume-title":"Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series","author":"LPD den Dries van","year":"1998","unstructured":"van den Dries, LPD: Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1998)"},{"unstructured":"Ge, G.: Testing equalities of multiplicative representations in polynomial time. In: SFCS, pp. 422\u2013426. IEEE Computer Society (1993)","key":"9913_CR8"},{"key":"9913_CR9","volume-title":"Lectures on Linear Sequential Machines","author":"MA Harrison","year":"1969","unstructured":"Harrison, M.A.: Lectures on Linear Sequential Machines. Academic Press, New York-Londres (1969)"},{"doi-asserted-by":"crossref","unstructured":"Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: STOC, pp. 252\u2013261 (1980)","key":"9913_CR10","DOI":"10.1145\/800141.804673"},{"issue":"4","key":"9913_CR11","doi-asserted-by":"publisher","first-page":"808","DOI":"10.1145\/6490.6496","volume":"33","author":"Ravindran Kannan","year":"1986","unstructured":"Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808\u2013821 (1986)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Masser, D.W.: Linear relations on algebraic groups. In: Baker, A. (ed.) New Advances in Transcendence Theory, pp 248\u2013262. Cambridge University Press, Cambridge (1988)","key":"9913_CR12","DOI":"10.1017\/CBO9780511897184.016"},{"doi-asserted-by":"crossref","unstructured":"Mignotte, M.: Some useful bounds. In: Computer Algebra, Volume 4 of Computing Supplementum 4. Springer, Vienna (1982)","key":"9913_CR13","DOI":"10.1007\/978-3-7091-3406-1_16"},{"doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on Karr\u2019s algorithm. In: ICALP, Volume 3142 of Lecture Notes in Computer Science, pp. 1016\u20131028. Springer (2004)","key":"9913_CR14","DOI":"10.1007\/978-3-540-27836-8_85"},{"doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330\u2013341. ACM (2004)","key":"9913_CR15","DOI":"10.1145\/982962.964029"},{"doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Ultimate positivity is decidable for simple linear recurrence sequences. In: ICALP, pp. 330\u2013341 (2014)","key":"9913_CR16","DOI":"10.1007\/978-3-662-43951-7_28"},{"doi-asserted-by":"crossref","unstructured":"Tao, T.: Structure and Randomness. AMS (2008)","key":"9913_CR17","DOI":"10.1090\/mbk\/059"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-019-09913-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-019-09913-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-019-09913-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,25]],"date-time":"2020-02-25T19:10:47Z","timestamp":1582657847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-019-09913-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,26]]},"references-count":17,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,7]]}},"alternative-id":["9913"],"URL":"https:\/\/doi.org\/10.1007\/s00224-019-09913-3","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2019,2,26]]},"assertion":[{"value":"26 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}