{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:17:25Z","timestamp":1784873845790,"version":"3.55.0"},"reference-count":67,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T00:00:00Z","timestamp":1603065600000},"content-version":"unspecified","delay-in-days":79,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We define representations for downward-closed subsets of a rich family of well-quasi-orders, and more generally for closed subsets of an even richer family of Noetherian topological spaces. This includes the cases of finite words, of multisets, of finite trees, notably. Those representations are given as finite unions of ideals, or more generally of irreducible closed subsets. All the representations we explore are computable, in the sense that we exhibit algorithms that decide inclusion, and compute finite unions and finite intersections. The origin of this work lies in the need for computing finite representations of sets of successors of the downward closure of one state, or more generally of a downward-closed set of states, in a well-structured transition system, and this is where we start: we define adequate notions of completions of well-quasi-orders, and more generally, of Noetherian spaces. For verification purposes, we argue that the required completions must be ideal completions, or more generally sobrifications, that is, spaces of irreducible closed subsets.<\/jats:p>","DOI":"10.1017\/s0960129520000195","type":"journal-article","created":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T02:48:56Z","timestamp":1603075736000},"page":"752-832","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Forward analysis for WSTS, part I: completions"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0702-3232","authenticated-orcid":false,"given":"Alain","family":"Finkel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5879-3304","authenticated-orcid":false,"given":"Jean","family":"Goubault-Larrecq","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,10,19]]},"reference":[{"key":"S0960129520000195_ref35","first-page":"27","article-title":"Spaces with no infinite discrete subspace","volume":"53","author":"Goubault-Larrecq","year":"2019","journal-title":"Topology Proceedings"},{"key":"S0960129520000195_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF02576519"},{"key":"S0960129520000195_ref22","doi-asserted-by":"publisher","DOI":"10.2307\/1968767"},{"key":"S0960129520000195_ref34","unstructured":"Goubault-Larrecq, J. (2013). Non-Hausdorff Topology and Domain Theory, Selected Topics in Point-Set Topology, New Mathematical Monographs, vol. 22, Cambridge University Press."},{"key":"S0960129520000195_ref6","first-page":"160","article-title":"Verifying programs with unreliable channels","author":"Abdulla","year":"1993","journal-title":"LICS'93"},{"key":"S0960129520000195_ref2","first-page":"313","article-title":"General decidability theorems for infinite-state systems","author":"Abdulla","year":"1996","journal-title":"LICS"},{"key":"S0960129520000195_ref58","first-page":"4","volume-title":"Proceedings of the 9th International Symposium on Static Analysis (SAS'02)","author":"M\u00fcller-Olm","year":"2002"},{"key":"S0960129520000195_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90009-7"},{"key":"S0960129520000195_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18088-5_43"},{"key":"S0960129520000195_ref32","first-page":"453","article-title":"On Noetherian spaces","author":"Goubault-Larrecq","year":"2007","journal-title":"LICS'07"},{"key":"S0960129520000195_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-8641(97)00222-8"},{"key":"S0960129520000195_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"S0960129520000195_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_2"},{"key":"S0960129520000195_ref55","first-page":"477","article-title":"On boundedness in depth in the pi-calculus","volume":"273","author":"Meyer","year":"2008","journal-title":"IFIP TCS"},{"key":"S0960129520000195_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.01.006"},{"key":"S0960129520000195_ref64","unstructured":"Sturmfels, B. (2002). Solving Systems of Polynomial Equations, CBMS Regional Conferences Series, vol. 97, American Mathematical Society."},{"key":"S0960129520000195_ref52","first-page":"56","article-title":"Demystifying reachability in vector addition systems","author":"Leroux","year":"2015","journal-title":"LICS'15"},{"key":"S0960129520000195_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"S0960129520000195_ref44","first-page":"1","article-title":"FO2(<, +1, \u223c) on data trees, data tree automata and branching vector addition systems","volume":"12","author":"Jacquemard","year":"2016","journal-title":"LMCS"},{"key":"S0960129520000195_ref19","first-page":"64","article-title":"Vector addition tree automata","author":"de Groote","year":"2004","journal-title":"LICS'04"},{"key":"S0960129520000195_ref21","first-page":"70","article-title":"On model checking for non-deterministic infinite-state systems","author":"Emerson","year":"1998","journal-title":"LICS'98"},{"key":"S0960129520000195_ref4","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000033962.51898.1a"},{"key":"S0960129520000195_ref50","volume-title":"Challenges in Symbolic Computation Software","author":"Laplagne","year":"2006"},{"key":"S0960129520000195_ref23","unstructured":"Faith, C. C. (1999). Rings and Things and a Fine Array of Twentieth Century Associative Algebra, American Mathematical Society."},{"key":"S0960129520000195_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"S0960129520000195_ref12","first-page":"329","article-title":"Termination orderings for associative-commutative rewriting systems","volume":"1","author":"Bachmair","year":"1985","journal-title":"Journal of Logic and Computation"},{"key":"S0960129520000195_ref13","volume-title":"Proceedings of the 37th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'17)","volume":"16","author":"Blondin","year":"2017"},{"key":"S0960129520000195_ref27","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:28)2012"},{"key":"S0960129520000195_ref9","unstructured":"Adams, W. W. and Loustaunau, P. (1994). An Introduction to Gr\u00f6bner Bases, Graduate Studies in Mathematics, vol. 3, American Mathematical Society, 289."},{"key":"S0960129520000195_ref16","first-page":"1982","volume-title":"Computer Algebra, Symbolic and Algebraic Computation","author":"Buchberger"},{"key":"S0960129520000195_ref5","first-page":"343","volume-title":"FORMATS\/FTRTFT","author":"Abdulla","year":"2004"},{"key":"S0960129520000195_ref38","unstructured":"Grothendieck, A. (1960). \u00c9l\u00e9ments de g\u00e9om\u00e9trie alg\u00e9brique (r\u00e9dig\u00e9s avec la collaboration de Jean Dieudonn\u00e9): I. Le langage des sch\u00e9mas, vol. 4, Publications math\u00e9matiques de l'I.H.\u00c9.S, 5\u2013228."},{"key":"S0960129520000195_ref51","first-page":"251","article-title":"Nets with tokens which carry data","volume":"88","author":"Lazi\u010d","year":"2008","journal-title":"Fundamenta Informaticae"},{"key":"S0960129520000195_ref7","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky","year":"1994"},{"key":"S0960129520000195_ref56","doi-asserted-by":"publisher","DOI":"10.1038\/218019a0"},{"key":"S0960129520000195_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00646-1"},{"key":"S0960129520000195_ref53","first-page":"238","article-title":"An algorithm for the general Petri net reachability problem","author":"Mayr","year":"1981","journal-title":"Proceedings of the 13th Annual ACM Symposium on the Theory of Computing (STOC'81)"},{"key":"S0960129520000195_ref60","first-page":"46","volume-title":"18th Annual Symposium on Foundations of Computer Science","author":"Pnueli","year":"1977"},{"key":"S0960129520000195_ref26","first-page":"433","article-title":"Forward analysis for WSTS, part I: Completions","author":"Finkel","year":"2009","journal-title":"Proceedings of the 26th Annual Symposium on Theoretical Aspects of Computer Science (STACS'09)"},{"key":"S0960129520000195_ref36","first-page":"1","volume-title":"43rd International Colloquium on Automata, Languages, and Programming","volume":"95, 97","author":"Goubault-Larrecq","year":"2016"},{"key":"S0960129520000195_ref1","first-page":"305","volume-title":"CAV'98","author":"Abdulla","year":"1998"},{"key":"S0960129520000195_ref14","unstructured":"Blondin, M. , Finkel, A. and Goubault-Larrecq, J. (2017b). Forward analysis for WSTS, Part III: Karp-Miller trees. Logical Methods in Computer Science 16 (2), 2020. doi: 10.23638\/LMCS-16(2:13)2020. Long and improved version of Blondin et al. (2017a)."},{"key":"S0960129520000195_ref67","first-page":"94","volume-title":"Proceedings of the 13th International Conference Foundations of Software Science and Computational Structures (FoSSaCS'10)","author":"Wies","year":"2010"},{"key":"S0960129520000195_ref62","first-page":"263","volume-title":"ACL'94","author":"Rambow","year":"1994"},{"key":"S0960129520000195_ref29","first-page":"49","volume-title":"VMCAI'06","author":"Ganty","year":"2006"},{"key":"S0960129520000195_ref31","volume-title":"Encyclopedia of Mathematics and its Applications","author":"Gierz","year":"2003"},{"key":"S0960129520000195_ref18","unstructured":"Cormen, T. H. , Leiserson, C. E. , Rivest, R. L. and Stein, C. (2001). Introduction to Algorithms, 2nd edition, MIT Press and McGraw-Hill."},{"key":"S0960129520000195_ref37","first-page":"258","volume-title":"Proceedings of the 5th International Conference on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes (AAECC-5), 1987","author":"Grieco","year":"1989"},{"key":"S0960129520000195_ref20","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"S0960129520000195_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/BF01691346"},{"key":"S0960129520000195_ref39","unstructured":"Halfon, S. (2018). On Effective Representations of Well Quasi-Orderings. Phd thesis, ENS Paris-Saclay, Universit\u00e9 Paris-Saclay."},{"key":"S0960129520000195_ref40","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"S0960129520000195_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BF02194315"},{"key":"S0960129520000195_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129520000195_ref3","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"S0960129520000195_ref41","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.83.145"},{"key":"S0960129520000195_ref43","unstructured":"Jacob\u00e9 de Naurois, P. (2014). Coverability in a nonfunctional extension of BVASS. hal-00947136. https:\/\/hal.archives-ouvertes.fr\/hal-00947136."},{"key":"S0960129520000195_ref17","unstructured":"Comon, H. , Dauchet, M. , Gilleron, R. , Jacquemard, F. , Lugiez, D. , Tison, S. and Tommasi, M. (2004). Tree automata techniques and applications. www.grappa.univ-lille3.fr\/tata."},{"key":"S0960129520000195_ref47","first-page":"267","volume-title":"Proceedings of the 14th Annual ACM Symposium on the Theory of Computing (STOC'82)","author":"Kosaraju","year":"1982"},{"key":"S0960129520000195_ref45","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/1992260504491"},{"key":"S0960129520000195_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"S0960129520000195_ref63","first-page":"514","article-title":"On the computational complexity of dominance links in grammatical formalisms","author":"Schmitz","year":"2010","journal-title":"ACL'10"},{"key":"S0960129520000195_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"S0960129520000195_ref48","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129520000195_ref66","doi-asserted-by":"crossref","first-page":"217","DOI":"10.46298\/dmtcs.350","article-title":"Karp-Miller trees for a branching extension of VASS","volume":"7","author":"Verma","year":"2005","journal-title":"Discrete Mathematics and Theoretical Computer Science"},{"key":"S0960129520000195_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"S0960129520000195_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782361"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,23]],"date-time":"2022-11-23T20:31:29Z","timestamp":1669235489000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000195\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8]]},"references-count":67,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,8]]}},"alternative-id":["S0960129520000195"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000195","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}