{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T04:04:01Z","timestamp":1751774641422,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3-4","license":[{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2014-04162"],"award-info":[{"award-number":["RGPIN-2014-04162"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.<\/jats:p>","DOI":"10.1007\/s00165-018-0460-8","type":"journal-article","created":{"date-parts":[[2018,7,18]],"date-time":"2018-07-18T23:32:13Z","timestamp":1531956733000},"page":"463-489","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parameterized verification of monotone information systems"],"prefix":"10.1145","volume":"30","author":[{"given":"Rapha\u00ebl","family":"Chane-Yack-Fa","sequence":"first","affiliation":[{"name":"GRIL, D\u00e9partement d\u2019informatique, Facult\u00e9 des sciences, Universit\u00e9 de Sherbrooke, Sherbrooke, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[{"name":"GRIL, D\u00e9partement d\u2019informatique, Facult\u00e9 des sciences, Universit\u00e9 de Sherbrooke, Sherbrooke, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amel","family":"Mammar","sequence":"additional","affiliation":[{"name":"T\u00e9l\u00e9com SudParis, SAMOVAR-CNRS, \u00c9vry, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[{"name":"LSV, CNRS &amp; ENS Paris-Saclay, Universit\u00e9 Paris-Saclay, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Abdulla PA Cerans K Jonsson B Tsay YK (1996) General decidability theorems for infinite-state systems. In: Logic in computer science. IEEE pp 313\u2013321"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abdulla PA Haziza F Hol\u00edk L (2013) All for the price of few. In: Verification model checking and abstract interpretation volume 7737 of LNCS. Springer pp 476\u2013495","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bingham JD Hu AJ (2005) Empirically efficient verification for a class of infinite-state systems. In: Tools and algorithms for the construction and analysis of systems volume 3440 of LNCS. Springer pp 77\u201392","DOI":"10.1007\/978-3-540-31980-1_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/553142"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Clarke E Talupur M Veith H (2006) Environment abstraction for parameterized verification. In: Verification model checking and abstract interpretation volume 3855 of LNCS. Springer pp 126\u2013141","DOI":"10.1007\/11609773_9"},{"key":"e_1_2_1_2_8_2","unstructured":"Chane-Yack-Fa R (2017) Verification of parameterized algebraic state transition diagrams. Technical report D\u00e9partement d\u2019informatique Facult\u00e9 des Sciences Universit\u00e9 de Sherbrooke. http:\/\/info.usherbrooke.ca\/mfrappier\/Papers\/pastd.pdf"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Dufourd C Finkel A Schnoebelen P (1998) Reset nets between decidability and undecidability. In: Automata languages and programming volume 1443 of LNCS. Springer pp 103\u2013115","DOI":"10.1007\/BFb0055044"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.3190160509"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Delzanno G Sangnier A Zavattaro G (2010) Parameterized verification of ad hoc networks. In: Concurrency theory volume 6269 of LNCS. Springer pp 313\u2013327","DOI":"10.1007\/978-3-642-15375-4_22"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Embe-Jiague M Frappier M Gervais F Konopacki P Laleau R Milhau J St-Denis R (2010) Model-driven engineering of functional security policies. In: International conference on enterprise information systems. SciTePress pp 374\u2013379","DOI":"10.5220\/0003019403740379"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Emerson EA Kahlon V (2000) Reducing model checking of the many to the few. In: Automated deduction volume 1831 of LNCS. Springer pp 236\u2013254","DOI":"10.1007\/10721959_19"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Frappier M Fraikin B Chossart R Chane-Yack-Fa R Ouenzar M (2010) Comparison of model checking tools for information systems. In: Formal Methods and software engineering volume 6447 of LNCS. Springer pp 581\u2013596","DOI":"10.1007\/978-3-642-16901-4_38"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0064-1"},{"key":"e_1_2_1_2_17_2","unstructured":"Frappier M Gervais F Laleau R Fraikin B (2008) Algebraic state transition diagrams. Technical report Universit\u00e9 de Sherbrooke. http:\/\/info.usherbrooke.ca\/mfrappier\/Papers\/astd.pdf"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Finkel A (1987) A generalization of the procedure of karp and miller to well structured transition systems. In: Automata languages and programming volume 267 of LNCS. Springer pp 499\u2013508","DOI":"10.1007\/3-540-18088-5_43"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02277857"},{"issue":"1","key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","article-title":"Well-structured transition systems everywhere!","volume":"256","author":"Finkel Alain","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0024-z"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Higman G (1952) Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society vol s3-2 pp 326\u2013336","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Hanna Y Samuelson D Basu S Rajan H (2010) Automating cut-off for multi-parameterized systems. In: Formal methods and software engineering volume 6447 of LNCS. Springer pp 338\u2013354","DOI":"10.1007\/978-3-642-16901-4_23"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kaiser A Kroening D Wahl T (2010) Dynamic cutoff detection in parameterized concurrent programs. In: Computer aided verification volume 6174 of LNCS. Springer pp 645\u2013659","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_1_2_28_2","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture","volume":"95","author":"Kruskal JB","year":"1960","journal-title":"Trans Am Math Soc"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"K\u00f6nig B St\u00fcckrath J (2014) A general framework for well-structured graph transformation systems. In: Concurrency theory volume 8704 of LNCS. Springer pp 467\u2013481","DOI":"10.1007\/978-3-662-44584-6_32"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"McMillan KL (1999) Verification of infinite state systems by compositional model checking. In: Correct hardware design and verification methods volume 1703 of LNCS. Springer pp 219\u2013234","DOI":"10.1007\/3-540-48153-2_17"},{"key":"e_1_2_1_2_31_2","unstructured":"Meyer R (2009) Structural Stationarity in the \u03c0-Calculus. Ph.D. thesis Department f\u00fcr Informatik Carl von Ossietzky Universit\u00e4t Oldenburg"},{"volume-title":"Communication and concurrency","year":"1989","author":"Milner R","key":"e_1_2_1_2_32_2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/539513"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/550448"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2009.07.003"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Siirtola A Kortelainen J (2009) Algorithmic verification with multiple and nested parameters. In: Formal methods and software engineering volume 5885 of LNCS. Springer pp 561\u2013580","DOI":"10.1007\/978-3-642-10373-5_29"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Siirtola A Kortelainen J (2009) Parameterised process algebraic verification by precongruence reduction. In: Application of concurrency to system design. IEEE pp 158\u2013167","DOI":"10.1109\/ACSD.2009.9"},{"key":"e_1_2_1_2_38_2","unstructured":"Schmitz S Schnoebelen P (2012) Algorithmic aspects of wqo theory. Lecture Notes"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0362-6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0460-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0460-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0460-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0460-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T21:52:26Z","timestamp":1751752346000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0460-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8]]},"references-count":39,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["10.1007\/s00165-018-0460-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0460-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2018,8]]},"assertion":[{"value":"12 October 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}