{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:41:49Z","timestamp":1725565309875},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_28","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"361-371","source":"Crossref","is-referenced-by-count":0,"title":["Image Computation in Infinite State Model Checking"],"prefix":"10.1007","author":[{"given":"Alain","family":"Finkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-thefly analysis of systems with unbounded, lossy FIFO channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"28_CR2","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":"28_CR3","unstructured":"Alv homepage.: http:\/\/www.cs.ucsb.edu\/~bultan\/composite\/"},{"key":"28_CR4","unstructured":"Babylon homepage: http:\/\/www.ulb.ac.be\/di\/ssd\/lvbegin\/CST\/-index.html"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-45069-6_26","volume-title":"Computer Aided Verification","author":"C. Bartziz","year":"2003","unstructured":"Bartziz, C., Bultan, T.: Efficient image computation in infinite state model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 249\u2013261. Springer, Heidelberg (2003)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"issue":"5\u20136","key":"28_CR7","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/S0020-0190(00)00055-7","volume":"74","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., Wolper, P.: An efficient automata approach to some problems on context-free grammars. Information Processing Letters\u00a074(5\u20136), 221\u2013227 (2000)","journal-title":"Information Processing Letters"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-46419-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.-P. Bodeveix","year":"2000","unstructured":"Bodeveix, J.-P., Filali, M.: FMona: a tool for expressing validation techniques over infinite state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 204\u2013219. Springer, Heidelberg (2000)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic modelchecking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"issue":"4","key":"28_CR11","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems\u00a021(4), 747\u2013789 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1\u20132","key":"28_CR12","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. Theoretical Computer Science\u00a0221(1\u20132), 211\u2013250 (1999)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"28_CR13","doi-asserted-by":"crossref","first-page":"191","DOI":"10.36045\/bbms\/1103408547","volume":"1","author":"V. Bruy\u00e8re","year":"1994","unstructured":"Bruy\u00e8re, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc.\u00a01(2), 191\u2013238 (1994)","journal-title":"Bull. Belg. Math. Soc."},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"issue":"2","key":"28_CR15","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/S0304-3975(03)00314-1","volume":"309","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science\u00a0309(2), 413\u2013468 (2003)","journal-title":"Theoretical Computer Science"},{"key":"28_CR16","unstructured":"Brain homepage, http:\/\/www.cs.man.ac.uk\/voronkov\/BRAIN\/index.html"},{"issue":"3","key":"28_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming","author":"C. Dufourd","year":"1998","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 103\u2013115. Springer, Heidelberg (1998)"},{"key":"28_CR20","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":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-44585-4_28","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 298\u2013310. Springer, Heidelberg (2001)"},{"key":"28_CR22","first-page":"70","volume-title":"Proc. 13th IEEE Symp. Logic in Computer Science (LICS 1998)","author":"E. Allen Emerson","year":"1998","unstructured":"Allen Emerson, E., Namjoshi, K.S.: On model checking for nondeterministic infinite-state systems. In: Proc. 13th IEEE Symp. Logic in Computer Science (LICS 1998), Indianapolis, IN, USA, June 1998, pp. 70\u201380. IEEE Comp. Soc. Press, Los Alamitos (1998)"},{"key":"28_CR23","unstructured":"Fast homepage, http:\/\/www.lsv.ens-cachan.fr\/fast\/"},{"key":"28_CR24","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 Presburgeraccelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-24732-6_14","volume-title":"Model Checking Software","author":"A. Finkel","year":"2004","unstructured":"Finkel, A., Leroux, J.: Polynomial time image computation with interval-definable counters system. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 182\u2013197. Springer, Heidelberg (2004)"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/3-540-44618-4_40","volume-title":"CONCUR 2000 - Concurrency Theory","author":"A. Finkel","year":"2000","unstructured":"Finkel, A., Iyer, S.P., Sutre, G.: Well-abstracted transition systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 566\u2013580. Springer, Heidelberg (2000)"},{"issue":"1-2","key":"28_CR28","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! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"28_CR29","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas and languages. Pacific J. Math.\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific J. Math."},{"issue":"4","key":"28_CR30","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N. Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. of Foundations Computer Science\u00a013(4), 571\u2013586 (2002)","journal-title":"Int. J. of Foundations Computer Science"},{"key":"28_CR31","unstructured":"Lash homepage, http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"28_CR32","unstructured":"Leroux, J.: Algorithmique de la v\u00e9rification des syst\u00e8mes \u00e0 compteurs. Approximation et acc\u00e9l\u00e9ration. Impl\u00e9mentation de l\u2019outil Fast. PhD thesis, Ecole Normale Sup\u00e9rieure de Cachan, Laboratoire Sp\u00e9cification et V\u00e9rification. CNRS UMR 8643, d\u00e9cembre (2003)"},{"key":"28_CR33","unstructured":"Mona homepage, http:\/\/www.brics.dk\/mona\/index.html"},{"issue":"2","key":"28_CR34","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(77)90001-9","volume":"5","author":"A. Mandel","year":"1977","unstructured":"Mandel, A., Simon, I.: On finite semigroups of matrices. Theoretical Computer Science\u00a05(2), 101\u2013111 (1977)","journal-title":"Theoretical Computer Science"},{"key":"28_CR35","unstructured":"Reutenauer, C.: Aspects Math\u00e9matiques des R\u00e9seaux de Petri, chapter 3. Collection Etudes et Recherches en Informatique. Masson, Paris (1989)"},{"key":"28_CR36","unstructured":"TReX homepage, http:\/\/www.liafa.jussieu.fr\/~sighirea\/trex\/"},{"key":"28_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 1\u201319. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:27:28Z","timestamp":1620012448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}