{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:23Z","timestamp":1740122723807,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,2,28]],"date-time":"2024-02-28T00:00:00Z","timestamp":1709078400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,2,28]],"date-time":"2024-02-28T00:00:00Z","timestamp":1709078400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Software Systems (MPI-SWS)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce the notion of <jats:italic>porous invariants<\/jats:italic> for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbb {Z}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Z<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-linear invariants (those defined as conjunctions of linear equations with integer coefficients), we show that a strongest such invariant can be computed in polynomial time. For the more general class of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbb {N}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>N<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-semi-linear invariants (those defined as Boolean combinations of linear inequalities with integer coefficients), such a strongest invariant need not exist. Here we show that for point targets the existence of a separating invariant is undecidable in general. However we show that such separating invariants can be computed either by restricting the number of program variables or by restricting from multipath to single-path loops. Additionally, we consider porous targets, represented as <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbb {Z}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Z<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-semi-linear sets (those defined as Boolean combinations of equations with integer coefficients). We show that an invariant can be computed providing the target spans the whole space. We present our tool <jats:sc>porous<\/jats:sc>, which computes porous invariants.<\/jats:p>","DOI":"10.1007\/s10703-024-00444-3","type":"journal-article","created":{"date-parts":[[2024,2,28]],"date-time":"2024-02-28T14:02:00Z","timestamp":1709128920000},"page":"235-271","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Porous invariants for linear systems"],"prefix":"10.1007","volume":"63","author":[{"given":"Engel","family":"Lefaucheux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Purser","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":[[2024,2,28]]},"reference":[{"key":"444_CR1","volume-title":"G\u00f6del, Escher, Bach: an eternal golden braid","author":"RH Douglas","year":"1979","unstructured":"Douglas RH (1979) G\u00f6del, Escher, Bach: an eternal golden braid. Basic Books, New York"},{"issue":"4","key":"444_CR2","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Fehnker A, Han Z, Krogh BH, Ouaknine J, Stursberg O, Theobald M (2003) Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int J Found Comput Sci 14(4):583\u2013604. https:\/\/doi.org\/10.1142\/S012905410300190X","journal-title":"Int J Found Comput Sci"},{"key":"444_CR3","doi-asserted-by":"publisher","unstructured":"Lefaucheux E, Ouaknine J, Purser D, Worrell J (2021) Porous invariants. In: Silva A, Leino KRM (eds) Computer aided verification\u201333rd international conference, CAV 2021, virtual event, July 20-23, 2021, proceedings, part II. Lecture notes in computer science, vol 12760. Springer, Cham, pp 172\u2013194. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_8","DOI":"10.1007\/978-3-030-81688-9_8"},{"key":"444_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr M (1976) Affine relationships among variables of a program. Acta Inform 6:133\u2013151. https:\/\/doi.org\/10.1007\/BF00268497","journal-title":"Acta Inform"},{"key":"444_CR5","doi-asserted-by":"publisher","unstructured":"Fijalkow N, Lefaucheux E, Ohlmann P, Ouaknine J, Pouly A, Worrell J (2019) On the monniaux problem in abstract interpretation. In: Chang BE (eds) Static analysis\u201326th international symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, proceedings. Lecture notes in computer science, vol 11822. Springer, Cham, pp 162\u2013180. https:\/\/doi.org\/10.1007\/978-3-030-32304-2_9","DOI":"10.1007\/978-3-030-32304-2_9"},{"issue":"4","key":"444_CR6","doi-asserted-by":"publisher","first-page":"808","DOI":"10.1145\/6490.6496","volume":"33","author":"R Kannan","year":"1986","unstructured":"Kannan R, Lipton RJ (1986) Polynomial-time algorithm for the orbit problem. J ACM 33(4):808\u2013821. https:\/\/doi.org\/10.1145\/6490.6496","journal-title":"J ACM"},{"issue":"6","key":"444_CR7","first-page":"539","volume":"57","author":"A Markov","year":"1947","unstructured":"Markov A (1947) On certain insoluble problems concerning matrices. Doklady Akad Nauk SSSR 57(6):539\u2013542","journal-title":"Doklady Akad Nauk SSSR"},{"issue":"4","key":"444_CR8","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s00236-018-0324-y","volume":"56","author":"D Monniaux","year":"2019","unstructured":"Monniaux D (2019) On the decidability of the existence of polyhedral invariants in transition systems. Acta Inform 56(4):385\u2013389. https:\/\/doi.org\/10.1007\/s00236-018-0324-y","journal-title":"Acta Inform"},{"key":"444_CR9","doi-asserted-by":"publisher","unstructured":"Hrushovski E, Ouaknine J, Pouly A, Worrell J (2018) Polynomial invariants for affine programs. In: Dawar A, Gr\u00e4del E (eds.), Proceedings of the 33rd annual ACM\/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 09-12, 2018, ACM, New York, NY, USA, pp 530\u2013539. https:\/\/doi.org\/10.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"issue":"2","key":"444_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3501299","volume":"23","author":"S Almagor","year":"2022","unstructured":"Almagor S, Chistikov D, Ouaknine J, Worrell J (2022) O-minimal invariants for discrete-time dynamical systems. ACM Trans Comput Logic 23(2):1\u201320. https:\/\/doi.org\/10.1145\/3501299","journal-title":"ACM Trans Comput Logic"},{"key":"444_CR11","doi-asserted-by":"publisher","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Aho AV, Zilles SN, Szymanski TG (eds) Conference record of the 5th annual ACM symposium on principles of programming languages, Tucson, Arizona, USA, January 1978. ACM, New York, NY, USA, pp 84\u201396. https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"444_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290368","volume":"3","author":"Z Kincaid","year":"2019","unstructured":"Kincaid Z, Breck J, Cyphert J, Reps TW (2019) Closed forms for numerical loops. Proc ACM Program Lang 3:1\u201329. https:\/\/doi.org\/10.1145\/3290368","journal-title":"Proc ACM Program Lang"},{"key":"444_CR13","doi-asserted-by":"publisher","unstructured":"Bozga M, Iosif R, Konecn\u00fd F (2010) Fast acceleration of ultimately periodic relations. In: Touili T, Cook B, Jackson PB (eds) Computer aided verification, 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture notes in computer science, vol 6174. Springer, Berlin, Heidelberg, pp 227\u2013242. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23. Extended VERIMAG technical report, TR-2012-10, 2012. http:\/\/www-verimag.imag.fr\/TR\/TR-2012-10.pdf","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"444_CR14","doi-asserted-by":"publisher","unstructured":"Finkel A, G\u00f6ller S, Haase C (2013) Reachability in register machines with polynomial updates. In: Chatterjee K, Sgall J (eds) Mathematical foundations of computer science 2013\u201338th international symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings. Lecture notes in computer science, vol 8087. Springer, Berlin, Heidelberg, pp 409\u2013420. https:\/\/doi.org\/10.1007\/978-3-642-40313-2_37","DOI":"10.1007\/978-3-642-40313-2_37"},{"key":"444_CR15","unstructured":"Fremont D (2013) The reachability problem for affine functions on the integers. arXiv:1304.2639"},{"issue":"1","key":"444_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl J, Aschermann C, Brockschmidt M, Emmes F, Frohn F, Fuhs C, Hensel J, Otto C, Pl\u00fccker M, Schneider-Kamp P, Str\u00f6der T, Swiderski S, Thiemann R (2017) Analyzing program termination and complexity automatically with AProVE. J Autom Reason 58(1):3\u201331. https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J Autom Reason"},{"key":"444_CR17","doi-asserted-by":"publisher","unstructured":"Heizmann M, Hoenicke J, Podelski A (2014) Termination analysis by learning terminating programs. In: Biere A, Bloem R (eds) Computer aided verification\u201326th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture notes in computer science, vol 8559. Springer, Cham, pp 797\u2013813. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_53","DOI":"10.1007\/978-3-319-08867-9_53"},{"issue":"4","key":"444_CR18","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1051\/ita:2003001","volume":"36","author":"V Cortier","year":"2002","unstructured":"Cortier V (2002) About the decision of reachability for register machines. RAIRO Theor Inform Appl 36(4):341\u2013358. https:\/\/doi.org\/10.1051\/ita:2003001","journal-title":"RAIRO Theor Inform Appl"},{"issue":"3","key":"444_CR19","doi-asserted-by":"publisher","first-page":"4","DOI":"10.2168\/LMCS-6(3:22)2010","volume":"6","author":"J Leroux","year":"2010","unstructured":"Leroux J (2010) The general vector addition system reachability problem by presburger inductive invariants. Log Methods Comput Sci 6(3):4\u201313. https:\/\/doi.org\/10.2168\/LMCS-6(3:22)2010","journal-title":"Log Methods Comput Sci"},{"key":"444_CR20","doi-asserted-by":"publisher","unstructured":"Leroux J (2011) Vector addition system reachability problem: a short self-contained proof. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. ACM, New York, NY, USA. https:\/\/doi.org\/10.1145\/1926385.1926421","DOI":"10.1145\/1926385.1926421"},{"issue":"2","key":"444_CR21","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1090\/S0002-9947-1964-0181500-1","volume":"113","author":"S Ginsburg","year":"1964","unstructured":"Ginsburg S, Spanier EH (1964) Bounded Algol-like languages. Trans Am Math Soc 113(2):333\u2013368. https:\/\/doi.org\/10.1090\/S0002-9947-1964-0181500-1","journal-title":"Trans Am Math Soc"},{"issue":"2","key":"444_CR22","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W Tzeng","year":"1992","unstructured":"Tzeng W (1992) A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J Comput 21(2):216\u2013227. https:\/\/doi.org\/10.1137\/0221017","journal-title":"SIAM J Comput"},{"key":"444_CR23","doi-asserted-by":"publisher","unstructured":"Leroux J (2004) Disjunctive invariants for numerical systems. In: Wang F (ed) Automated technology for verification and analysis: 2nd international conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. Lecture notes in computer science, vol 3299. Springer, Berlin, Heidelberg, pp 93\u2013107. https:\/\/doi.org\/10.1007\/978-3-540-30476-0_12","DOI":"10.1007\/978-3-540-30476-0_12"},{"issue":"4","key":"444_CR24","doi-asserted-by":"publisher","first-page":"1838","DOI":"10.1007\/BF01095643","volume":"34","author":"A Chistov","year":"1986","unstructured":"Chistov A (1986) Algorithm of polynomial complexity for factoring polynomials and finding the components of varieties in subexponential time. J Sov Math 34(4):1838\u20131882","journal-title":"J Sov Math"},{"key":"444_CR25","unstructured":"Shmonin G (2009) Lattices and Hermite normal form. Swiss federal institute of technology lausanne (EPFL). Lecture notes for the course Integer Points in Polyhedra at the swiss federal institute of technology lausanne (EPFL)"},{"issue":"4","key":"444_CR26","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1137\/0208040","volume":"8","author":"R Kannan","year":"1979","unstructured":"Kannan R, Bachem A (1979) Polynomial algorithms for computing the smith and hermite normal forms of an integer matrix. SIAM J Comput 8(4):499\u2013507. https:\/\/doi.org\/10.1137\/0208040","journal-title":"SIAM J Comput"},{"issue":"53","key":"444_CR27","first-page":"173","volume":"57","author":"L Kronecker","year":"1857","unstructured":"Kronecker L (1857) Zwei S\u00e4tze \u00fcber gleichungen mit ganzzahligen coefficienten. J Reine Angew Math 57(53):173\u2013175","journal-title":"J Reine Angew Math"},{"issue":"4","key":"444_CR28","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1051\/ita:2006039","volume":"40","author":"V Halava","year":"2006","unstructured":"Halava V, Harju T (2006) Undecidability of infinite post correspondence problem for instances of size 9. RAIRO Theor Inform Appl 40(4):551\u2013557. https:\/\/doi.org\/10.1051\/ita:2006039","journal-title":"RAIRO Theor Inform Appl"},{"issue":"3","key":"444_CR29","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1051\/ita\/2012015","volume":"46","author":"J Dong","year":"2012","unstructured":"Dong J, Liu Q (2012) Undecidability of infinite post correspondence problem for instances of size 8. RAIRO Theor Inform Appl 46(3):451\u2013457. https:\/\/doi.org\/10.1051\/ita\/2012015","journal-title":"RAIRO Theor Inform Appl"},{"key":"444_CR30","doi-asserted-by":"publisher","unstructured":"Ouaknine J, Worrell J (2012) Decision problems for linear recurrence sequences. In: Finkel A, Leroux J, Potapov I (eds) Reachability problems\u20136th international workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings. Lecture notes in computer science, vol 7550. Springer, Berlin, Heidelberg, pp 21\u201328. https:\/\/doi.org\/10.1007\/978-3-642-33512-9_3","DOI":"10.1007\/978-3-642-33512-9_3"},{"key":"444_CR31","doi-asserted-by":"publisher","unstructured":"Chonev V, Ouaknine J, Worrell J (2015) The polyhedron-hitting problem. In: Indyk P (ed) Proceedings of the 26th annual ACM-SIAM symposium on discrete algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, SIAM, USA, pp 940\u2013956. https:\/\/doi.org\/10.1137\/1.9781611973730.64","DOI":"10.1137\/1.9781611973730.64"},{"issue":"3","key":"444_CR32","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/2857050","volume":"63","author":"V Chonev","year":"2016","unstructured":"Chonev V, Ouaknine J, Worrell J (2016) On the complexity of the orbit problem. J ACM 63(3):23\u201312318","journal-title":"J ACM"},{"key":"444_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498727","volume":"6","author":"T Karimov","year":"2022","unstructured":"Karimov T, Lefaucheux E, Ouaknine J, Purser D, Varonka A, Whiteland MA, Worrell J (2022) What\u2019s decidable about linear loops? Proc ACM Program Lang 6:1\u201325","journal-title":"Proc ACM Program Lang"},{"key":"444_CR34","first-page":"163","volume":"8","author":"T Skolem","year":"1934","unstructured":"Skolem T (1934) Ein verfahren zur behandlung gewisser exponentialer gleichungen und diophantischer gleichungen. C r 8:163\u2013188","journal-title":"C r"},{"key":"444_CR35","doi-asserted-by":"publisher","unstructured":"Bilu Y, Luca F, Nieuwveld J, Ouaknine J, Purser D, Worrell J (2022) Skolem meets Schanuel. In: Szeider S, Ganian R, Silva A (eds) 47th international symposium on mathematical foundations of computer science, MFCS 2022, August 22-26, 2022, Vienna, Austria. LIPIcs, vol 241. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Germany, pp 20\u201312015. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.20","DOI":"10.4230\/LIPIcs.MFCS.2022.20"},{"key":"444_CR36","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7920425","author":"E Lefaucheux","year":"2023","unstructured":"Lefaucheux E, Ouaknine J, Purser D, Worrell J (2023) Porous invariants for linear systems: POROUS tool and experimental data. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.7920425","journal-title":"Zenodo"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00444-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00444-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00444-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T17:13:00Z","timestamp":1729530780000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00444-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,28]]},"references-count":36,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["444"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00444-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2024,2,28]]},"assertion":[{"value":"31 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 February 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}