{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:17:22Z","timestamp":1784837842409,"version":"3.55.0"},"reference-count":62,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,4,1]],"date-time":"2001-04-01T00:00:00Z","timestamp":986083200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4490,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,4]]},"DOI":"10.1016\/s0304-3975(00)00102-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T17:51:54Z","timestamp":1027619514000},"page":"63-92","source":"Crossref","is-referenced-by-count":467,"title":["Well-structured transition systems everywhere!"],"prefix":"10.1016","volume":"256","author":[{"given":"A.","family":"Finkel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ph.","family":"Schnoebelen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00102-X_BIB1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, K. C\u0306er\u0101ns, B. Jonsson, T. Yih-Kuen, General decidability theorems for infinite-state systems, Proc. 11th IEEE Symp. Logic in Computer Science (LICS\u201996), New Brunswick, NJ, USA, July 1996, pp. 313\u2013321.","DOI":"10.1109\/LICS.1996.561359"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB2","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, K. C\u0306er\u0101ns, B. Jonsson, T. Yih-Kuen, Algorithmic analysis of programs with well quasi-ordered domains, Inform. and Comput., to appear.","DOI":"10.1006\/inco.1999.2843"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB3","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, B. Jonsson, Verifying programs with unreliable channels, Proc. 8th IEEE Symp. Logic in Computer Science (LICS\u201993), Montreal, Canada, June 1993, pp. 160\u2013170.","DOI":"10.1109\/LICS.1993.287591"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB4","first-page":"316","article-title":"Undecidability of verifying programs with unreliable channels","volume":"vol. 820","author":"Abdulla","year":"1994"},{"issue":"this Vol.","key":"10.1016\/S0304-3975(00)00102-X_BIB5","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/S0304-3975(00)00105-5","article-title":"Ensuring completeness of symbolic verification methods for infinite-state systems","volume":"256","author":"Abdulla","year":"2001","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB6","first-page":"298","article-title":"Verifying networks of timed processes","volume":"vol. 1384","author":"Abdulla","year":"1998"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/S0304-3975(00)00102-X_BIB8","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(76)90067-0","article-title":"Some decision problems related to the reachability problem for Petri nets","volume":"3","author":"Araki","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB9","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF02576519","article-title":"R\u00e9cursivit\u00e9 et c\u00f4nes rationnels ferm\u00e9s par intersection","volume":"XV(IV)","author":"Arnold","year":"1978","journal-title":"Calcolo"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB10","first-page":"111","article-title":"Context-free languages and pushdown automata","volume":"vol. 1","author":"Autebert","year":"1997"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB11","first-page":"94","article-title":"Decidability of bisimulation equivalence for processes generating context-free languages","volume":"vol. 259","author":"Baeten","year":"1987"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB12","first-page":"361","article-title":"Finite state description of communication protocols","volume":"2","author":"von Bochmann","year":"1978","journal-title":"Comput. Networks ISDN Systems"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB13","first-page":"323","article-title":"Model checking lossy vector addition systems","volume":"vol. 1563","author":"Bouajjani","year":"1999"},{"issue":"2","key":"10.1016\/S0304-3975(00)00102-X_BIB14","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","article-title":"On communicating finite-state machines","volume":"30","author":"Brand","year":"1983","journal-title":"J. ACM"},{"issue":"1\u20132","key":"10.1016\/S0304-3975(00)00102-X_BIB15","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","article-title":"Characterizing finite Kripke structures in propositional temporal logic","volume":"59","author":"Browne","year":"1988","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/S0304-3975(00)00102-X_BIB16","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB17","unstructured":"G. G\u00e9c\u00e9, Etat de l'art des techniques d'analyse des automates finis communicants, Rapport de DEA, Universit\u00e9 de Paris-Sud, Orsay, France, September 1993."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB18","first-page":"304","article-title":"Programs with quasi-stable channels are effectively recognizable","volume":"1254","author":"G\u00e9c\u00e9","year":"1997"},{"issue":"1","key":"10.1016\/S0304-3975(00)00102-X_BIB19","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1006\/inco.1996.0003","article-title":"Unreliable channels are easier to verify than perfect channels","volume":"124","author":"C\u00e9c\u00e9","year":"1995","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB20","doi-asserted-by":"crossref","unstructured":"K.C\u0306er\u0101ns, Deciding properties of integral automata, in: Proc. 21st Internat. Coll. Automata, Languages, and Programming (ICALP\u201994), Jerusalem, Israel, July 1994, Lecture Notes in Computer Science, vol. 820, Springer, Berlin, 35\u201346","DOI":"10.1007\/3-540-58201-0_56"},{"issue":"4","key":"10.1016\/S0304-3975(00)00102-X_BIB21","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1093\/comjnl\/37.4.233","article-title":"Decidable subsets of CCS","volume":"37","author":"Christensen","year":"1994","journal-title":"Comput. J."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB22","first-page":"179","article-title":"Petri nets with marking-dependent arc cardinality","volume":"vol. 815","author":"Ciardo","year":"1994"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB23","first-page":"193","article-title":"Graph rewriting","volume":"vol. B","author":"Courcelle","year":"1990"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB24","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2307\/2370405","article-title":"Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors","volume":"35","author":"Dickson","year":"1913","journal-title":"Amer. J. Math."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB25","first-page":"103","article-title":"Ph. Schnoebelen. Reset nets between decidability and undecidability","volume":"vol. 1443","author":"Dufourd","year":"1998"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB26","unstructured":"J. Esparza, More infinite results, in: Proc. 1st Internat. Workshop on Verification of Infinite State Systems (INFINITY \u201996), Pisa, Italy, August 30\u201331, 1996, Electronic Notes in Theoretical Computer Science, vol. 5, Elsevier, Amsterdam, 1997."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB27","unstructured":"A. Finkel, About monogeneous fifo Petri nets, Proc. 3rd Eur. Workshop on Applications and Theory of Petri Nets, Varenna, Italy, September (1982) 175\u2013192."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB28","unstructured":"A. Finkel, Structuration des Syst\u00e8mes de Transitions, Applications au Contr\u00f4le du Parall\u00e9lisme par Files FIFO, Th\u00e8se de Docteur d'Etat, Universit\u00e9 de Paris-Sud, Orsay, France, June 1986."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB29","first-page":"499","article-title":"A generalization of the procedure of Karp and Miller to well structured transition systems","volume":"vol. 267","author":"Finkel","year":"1987"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB30","unstructured":"A. Finkel, Well structured transition systems, Research Report 365, Lab. de Recherche en Informatique (LRI), Univ. Paris-Sud, Orsay, August 1987."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB31","unstructured":"A. Finkel, A new class of analyzable CFSMs with unbounded FIFO channels, Prelim in: Proc. 8th IFIP WG 6.1 Internat. Symp. Protocol Specification, Testing and Verification, Atlantic City, New Jersey, USA, June 1988."},{"issue":"2","key":"10.1016\/S0304-3975(00)00102-X_BIB32","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","article-title":"Reduction and covering of infinite reachability trees","volume":"89","author":"Finkel","year":"1990","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB33","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BF02277857","article-title":"Decidability of the termination problem for completely specified protocols","volume":"7","author":"Finkel","year":"1994","journal-title":"Distributed Comput."},{"issue":"1","key":"10.1016\/S0304-3975(00)00102-X_BIB34","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00268843","article-title":"Fifo nets without order deadlock","volume":"25","author":"Finkel","year":"1987","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB35","unstructured":"A. Finkel, P. McKenzie, C. Picaronny, A well-structured framework for analysing Petri nets extensions, Research Report LSV-99-2, Lab. Specification and Verification, ENS de Cachan, Cachan, France, February 1999."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB36","unstructured":"R.J. van Glabbeek, W.P. Weijland, Branching time and abstraction in process algebra, in: G. X. Ritter (Ed.), Information Processing 89, North-Holland, Amsterdam, August 1989, 613\u2013618."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB37","doi-asserted-by":"crossref","unstructured":"M.G. Gouda, L.E. Rosier, Synchronizable networks of communicating finite state machines, unpublished manuscript, 1985.","DOI":"10.1137\/0214042"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB38","series-title":"Applications and Theory of Petri Nets (Selected Papers from the First and Second European Workshop, Strasbourg, France, September 1980, Bad Honnef, Germany, September 1981)","first-page":"187","article-title":"Subclasses of self-modifying nets","author":"Heinemann","year":"1982"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB39","first-page":"324","article-title":"Hybrid automata with finite bisimulations","volume":"vol. 944","author":"Henzinger","year":"1995"},{"issue":"7","key":"10.1016\/S0304-3975(00)00102-X_BIB40","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","article-title":"Ordering by divisibility in abstract algebras","volume":"2","author":"Higman","year":"1952","journal-title":"Proc. London Math. Soc. (3)"},{"issue":"2","key":"10.1016\/S0304-3975(00)00102-X_BIB41","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1006\/inco.1993.1069","article-title":"Deciding bisimulation equivalences for a class on non-finite-state programs","volume":"107","author":"Jonsson","year":"1993","journal-title":"Inform. and Comput."},{"issue":"2","key":"10.1016\/S0304-3975(00)00102-X_BIB42","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","article-title":"Parallel program schemata","volume":"3","author":"Karp","year":"1969","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB43","doi-asserted-by":"crossref","unstructured":"O. Kouchnarenko, Ph. Schnoebelen, A model for recursive-parallel programs, in: Proc. 1st Internat. Workshop on Verification of Infinite State Systems (INFINITY\u201996), Pisa, Italy, August 1996, Electronic Notes in Theoretical Computer Science, vol. 5, Elsevier, Amsterdam, 1997.","DOI":"10.1016\/S1571-0661(05)82512-5"},{"issue":"3","key":"10.1016\/S0304-3975(00)00102-X_BIB44","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0097-3165(72)90063-5","article-title":"The theory of well-quasi-ordering: a frequently discovered concept","volume":"13","author":"Kruskal","year":"1972","journal-title":"J. Combin. Theory Ser. A"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB45","first-page":"45","article-title":"A formal framework for the analysis of recursive-parallel programs","volume":"vol. 1277","author":"Kushnarenko","year":"1997"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB46","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1007\/BF01936139","article-title":"On permutative grammars generating context-free languages","volume":"25","author":"M\u00e4kinen","year":"1985","journal-title":"BIT"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB47","unstructured":"R. Mayr, Lossy counter machines, Technical Report TUM-19830, Institut f\u00fcr Informatik, TUM, Munich, Germany, October 1998."},{"issue":"2\u20133","key":"10.1016\/S0304-3975(00)00102-X_BIB48","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0304-3975(85)90014-3","article-title":"An introduction to FIFO nets-monogeneous nets: a subclass of FIFO nets","volume":"35","author":"Memmi","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB49","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB50","first-page":"195","article-title":"Infinite results","volume":"vol. 1119","author":"Moller","year":"1996"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB51","series-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson","year":"1981"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB52","volume":"vol. 4","author":"Reisig","year":"1985"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB53","first-page":"187","article-title":"A closed form for Datalog queries with integer order","volume":"vol. 470","author":"Revesz","year":"1990"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB54","first-page":"464","article-title":"Self-modifying nets, a natural extension of Petri nets","volume":"vol. 62","author":"Valk","year":"1978"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB55","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Nyl\u00e9n, Better is better than well: On efficient verification of infinite-state systems, in: Proc. 15th IEEE Symp. Logic in Computer Science (LICS\u20192000), Santa Barbara, CA, USA, June 2000.","DOI":"10.1109\/LICS.2000.855762"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB56","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Nyl\u00e9n, BQOs and Timed Petri Nets, Available at http:\/\/www.docs.uu.se\/\u00a0\u0303parosh\/publications\/publications.shtml, March 2000.","DOI":"10.1007\/3-540-45740-2_5"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB57","unstructured":"M. Bozzano, G. Delzanno, M. Martelli, A bottom-up semantics for LO, in: Proc. 2nd Int. Conf. Principles and Practice of Declarative Programming (PPDP\u20192000), Montreal, Canada, Sep. 2000, to appear."},{"key":"10.1016\/S0304-3975(00)00102-X_BIB58","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J.-F. Raskin, Symbolic representation of upward-closed sets, in: Proc. 6th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u20192000), Berlin, Germany, Mar.\u2013Apr. 2000, vol. 1785 of Lecture Notes in Computer Science, Springer, 2000, pp. 426\u2013440.","DOI":"10.1007\/3-540-46419-0_29"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB59","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, K.S. Namjoshi, Verification of a parameterized bus arbitration protocol, in: Proc. 10th Int. Conf. Computer Aided Verification (CAV\u201998), Vancouver, BC, Canada, June\u2013July 1998, vol. 1427 of Lecture Notes in Computer Science, Springer, 1998, pp. 452\u2013463.","DOI":"10.1007\/BFb0028766"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB60","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, R. Majumdar, A classification of symbolic transition systems. In Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS\u20192000), Lille, France, Feb. 2000, vol. 1770 of Lecture Notes in Computer Science, Springer, 2000, pp. 13\u201334.","DOI":"10.1007\/3-540-46541-3_2"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB61","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0020-0190(99)00149-0","article-title":"A note onn well quasi-orderings for powersets","volume":"72","author":"Jan\u010dar","year":"1999","journal-title":"Information Processing Letters"},{"key":"10.1016\/S0304-3975(00)00102-X_BIB62","doi-asserted-by":"crossref","unstructured":"M. Leuschel, H. Lehmann, Coverability of Reset Petri nets and other well-structured transition systems by partial deduction, in: Proc. 14th Int. Workshop Computer Science Logic (CSL\u20192000), Fischbachau, Germany, Aug. 2000, Lecture Notes in Computer Science, Springer, 2000, to appear.","DOI":"10.1007\/3-540-44957-4_7"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750000102X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750000102X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,28]],"date-time":"2020-01-28T13:14:12Z","timestamp":1580217252000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439750000102X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,4]]},"references-count":62,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,4]]}},"alternative-id":["S030439750000102X"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00102-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,4]]}}}