{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T06:09:57Z","timestamp":1791094197192,"version":"4.1.0"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":1141,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log"],"published-print":{"date-parts":[[2010,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we give a step by step introduction to the theory of<jats:italic>well quasi-ordered<\/jats:italic>transition systems. The framework combines two concepts, namely (i) transition systems which are<jats:italic>monotonic<\/jats:italic>wrt. a<jats:italic>well-quasi ordering<\/jats:italic>; and (ii) a scheme for symbolic<jats:italic>backward<\/jats:italic>reachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also present<jats:italic>better quasi-ordered<\/jats:italic>transition systems which allow the design of efficient symbolic representations of infinite sets of states.<\/jats:p>","DOI":"10.2178\/bsl\/1294171129","type":"journal-article","created":{"date-parts":[[2011,1,4]],"date-time":"2011-01-04T20:22:59Z","timestamp":1294172579000},"page":"457-515","source":"Crossref","is-referenced-by-count":42,"title":["Well (and Better) Quasi-Ordered Transition Systems"],"prefix":"10.1017","volume":"16","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600000706_ref027","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"S1079898600000706_ref024","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-18088-5_43","volume-title":"Proceedings of the ICALP '87, 14th International Colloquium on Automata, Languages, and Programming","author":"Finkel","year":"1987"},{"key":"S1079898600000706_ref032","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"S1079898600000706_ref023","volume-title":"Proceedings of the LICS '99, 14th IEEE International Symposium on Logic in Computer Science","author":"Esparza","year":"1999"},{"key":"S1079898600000706_ref011","first-page":"414","volume-title":"Proceedings of the LICS '90, 5th IEEE International Symposium on Logic in Computer Science","author":"Alur","year":"1990"},{"key":"S1079898600000706_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"S1079898600000706_ref020","volume-title":"Introduction to algorithms","author":"Cormen","year":"2001"},{"key":"S1079898600000706_ref030","first-page":"251","volume-title":"Fundamentals of Information","author":"Lazic","year":"2008"},{"key":"S1079898600000706_ref026","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"S1079898600000706_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5315-4_15"},{"key":"S1079898600000706_ref002","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"S1079898600000706_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"S1079898600000706_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"S1079898600000706_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45740-2_5"},{"key":"S1079898600000706_ref016","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"S1079898600000706_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00105-5"},{"key":"S1079898600000706_ref037","volume-title":"Introduction to constraint databases","author":"Revesz","year":"2002"},{"key":"S1079898600000706_ref022","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"S1079898600000706_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF02277857"},{"key":"S1079898600000706_ref034","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45739-9_15"},{"key":"S1079898600000706_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_8"},{"key":"S1079898600000706_ref013","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"key":"S1079898600000706_ref003","volume-title":"Proceedings of the AVIS'06, 5th International Workshop on on Automated Verification of Infinite-State Systems","author":"Abdulla","year":"2006"},{"key":"S1079898600000706_ref028","unstructured":"Jan\u010dar P. , \u03c92-well quasi-orderings and reachability analysis, Technical Report 158, Department of Computing Systems, Uppsala University, 1999."},{"key":"S1079898600000706_ref015","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000026093.21513.31"},{"key":"S1079898600000706_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"S1079898600000706_ref014","volume-title":"Proceedings of the TACAS '99, 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Biere","year":"1999"},{"key":"S1079898600000706_ref009","first-page":"132","volume-title":"Proceedings of the LICS '00, 16th IEEE International Symposium on Logic in Computer Science","author":"Abdulla","year":"2000"},{"key":"S1079898600000706_ref031","unstructured":"Marcone A. , Fine and axiomatic analysis of the quasi-orderings on (q), Technical Report 17\/99\/RR, Rapporto di Ricerca del Dipartimento di Matematica e Informatica dell'Universit\u00e0 di Udine, 1999."},{"key":"S1079898600000706_ref001","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"S1079898600000706_ref036","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"S1079898600000706_ref004","first-page":"160","volume-title":"Proceedings of the LICS '93, 8th IEEE International Symposium on Logic in Computer Science","author":"Abdulla","year":"1993"},{"key":"S1079898600000706_ref018","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-58201-0_56","volume-title":"Proceedings of the ICALP '94, 21st International Colloquium on Automata, Languages, and Programming","volume":"820","author":"\u010cer\u0101ns","year":"1994"},{"key":"S1079898600000706_ref019","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"S1079898600000706_ref033","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5315-4_14"},{"key":"S1079898600000706_ref038","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"},{"key":"S1079898600000706_ref005","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0053"},{"key":"S1079898600000706_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054179"}],"container-title":["The Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600000706","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T07:39:41Z","timestamp":1592206781000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600000706\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["S1079898600000706"],"URL":"https:\/\/doi.org\/10.2178\/bsl\/1294171129","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12]]}}}