{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:23:27Z","timestamp":1743114207504,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642218330"},{"type":"electronic","value":"9783642218347"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21834-7_4","type":"book-chapter","created":{"date-parts":[[2011,6,28]],"date-time":"2011-06-28T02:04:11Z","timestamp":1309226651000},"page":"49-68","source":"Crossref","is-referenced-by-count":5,"title":["Forward Analysis and Model Checking for Trace Bounded WSTS"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Chambart","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Schmitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., \u010cerans, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput.\u00a0160, 109\u2013127 (2000)","journal-title":"Inform. and Comput."},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/B:FORM.0000033962.51898.1a","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Form. Methods in Syst. Des.\u00a025, 39\u201365 (2004)","journal-title":"Form. Methods in Syst. Des."},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inform. and Comput.\u00a0130, 71\u201390 (1996)","journal-title":"Inform. and Comput."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inform. and Comput.\u00a0127, 91\u2013101 (1996)","journal-title":"Inform. and Comput."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TREX: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transfer\u00a010, 401\u2013424 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 474\u2013488. Springer, Heidelberg (2005)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems (2011) (in preparation)","DOI":"10.1007\/978-3-642-22993-0_13"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 55\u201367. Springer, Heidelberg (1994)"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A. Bouajjani","year":"1999","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theor. Comput. Sci.\u00a0221, 211\u2013250 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR11","doi-asserted-by":"crossref","first-page":"275","DOI":"10.3233\/FI-2009-0044","volume":"91","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fund. Inform.\u00a091, 275\u2013303 (2009)","journal-title":"Fund. Inform."},{"key":"4_CR12","first-page":"50","volume-title":"Proc. STOC 1976","author":"E. Cardoza","year":"1976","unstructured":"Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups. In: Proc. STOC 1976, pp. 50\u201354. ACM Press, New York (1976)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Chambart, P., Finkel, A., Schmitz, S.: Forward analysis and model checking for trace bounded WSTS. Research report, LSV (2010), http:\/\/arxiv.org\/abs\/1004.2802 (cs.LO)","DOI":"10.1007\/978-3-642-21834-7_4"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44622-2_17","volume-title":"Computer Science Logic","author":"H. Comon","year":"2000","unstructured":"Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 262\u2013276. Springer, Heidelberg (2000)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1051\/ita:2003001","volume":"36","author":"V. Cortier","year":"2002","unstructured":"Cortier, V.: About the decision of reachability for register machines. Theor. Inform. Appl.\u00a036, 341\u2013358 (2002)","journal-title":"Theor. Inform. Appl."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Demri, S.: On Selective Unboundedness of VASS. In: Proc. INFINITY 2010. Elec. Proc. in Theor. Comput. Sci., vol.\u00a039, pp. 1\u201315 (2010)","DOI":"10.4204\/EPTCS.39.1"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"313","DOI":"10.3166\/jancl.20.313-344","volume":"20","author":"S. Demri","year":"2011","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking CTL* over flat Presburger counter systems. J.\u00a0Appl. Non-Classical Log.\u00a020, 313\u2013344 (2011)","journal-title":"J.\u00a0Appl. Non-Classical Log."},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48523-6_27","volume-title":"Automata, Languages and Programming","author":"C. Dufourd","year":"1999","unstructured":"Dufourd, C., Jan\u010dar, P., Schnoebelen, P.: Boundedness of reset P\/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol.\u00a01644, pp. 301\u2013310. Springer, Heidelberg (1999)"},{"key":"4_CR20","first-page":"70","volume-title":"Proc. LICS 1998","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Proc. LICS 1998, pp. 70\u201380. IEEE, Los Alamitos (1998)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Inf.\u00a034, 85\u2013107 (1997)","journal-title":"Acta Inf."},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"Finkel, A.: Reduction and covering of infinite reachability trees. Inform. and Comput.\u00a089, 144\u2013179 (1990)","journal-title":"Inform. and Comput."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for\u00a0WSTS, part\u00a0I: Completions. In: Proc. STACS 2009. LIPIcs, vol.\u00a03, pp. 433\u2013444. LZI (2009)","DOI":"10.1007\/978-3-642-02930-1_16"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-02930-1_16","volume-title":"Automata, Languages and Programming","author":"A. Finkel","year":"2009","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part\u00a0II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol.\u00a05556, pp. 188\u2013199. Springer, Heidelberg (2009)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci.\u00a0256, 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-63141-0_15","volume-title":"CONCUR\u201997: Concurrency Theory","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 213\u2013227. Springer, Heidelberg (1997)"},{"key":"4_CR28","first-page":"102","volume-title":"Proc. POPL 2009","author":"P. Ganty","year":"2009","unstructured":"Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: Proc. POPL 2009, pp. 102\u2013113. ACM Press, New York (2009)"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1142\/S0129054110007441","volume":"21","author":"P. Gawrychowski","year":"2010","unstructured":"Gawrychowski, P., Krieger, D., Rampersad, N., Shallit, J.: Finding the growth rate of a regular or context-free language in polynomial time. Int. J. Fund. Comput. Sci.\u00a021, 597\u2013618 (2010)","journal-title":"Int. J. Fund. Comput. Sci."},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s00236-007-0050-3","volume":"44","author":"G. Geeraerts","year":"2007","unstructured":"Geeraerts, G., Raskin, J., Begin, L.V.: Well-structured languages. Acta Inf.\u00a044, 249\u2013288 (2007)","journal-title":"Acta Inf."},{"key":"4_CR31","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"Ginsburg, S., Spanier, E.H.: Bounded Algol-like languages. T.\u00a0Amer. Math. Soc.\u00a0113, 333\u2013368 (1964)","journal-title":"T.\u00a0Amer. Math. Soc."},{"key":"4_CR32","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J.\u00a0Comput. Syst. Sci.\u00a03, 147\u2013195 (1969)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"4_CR33","unstructured":"Krohn, M., Kohler, E., Kaashoek, M.F.: Events can make sense. In: Proc. USENIX 2007, pp. 87\u2013100 (2007)"},{"key":"4_CR34","unstructured":"The Li\u00e8ge automata-based symbolic handler (Lash), http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J. Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"key":"4_CR36","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R. Mayr","year":"2003","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. Theor. Comput. Sci.\u00a0297, 337\u2013354 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR37","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci.\u00a06, 223\u2013231 (1978)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR38","first-page":"319","volume-title":"Proc. FOCS 1988","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. FOCS 1988, pp. 319\u2013327. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1090\/S0002-9939-1969-0239891-9","volume":"21","author":"R. Siromoney","year":"1969","unstructured":"Siromoney, R.: A characterization of semilinear sets. Proc. Amer. Math. Soc.\u00a021, 689\u2013694 (1969)","journal-title":"Proc. Amer. Math. Soc."},{"key":"4_CR40","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/0022-0000(81)90067-2","volume":"23","author":"R. Valk","year":"1981","unstructured":"Valk, R., Vidal-Naquet, G.: Petri nets and regular languages. J.\u00a0Comput. Syst. Sci.\u00a023, 299\u2013325 (1981)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"4_CR41","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. LICS 1986, pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21834-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,27]],"date-time":"2021-11-27T00:23:09Z","timestamp":1637972589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21834-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642218330","9783642218347"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21834-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}