{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:21:16Z","timestamp":1725560476021},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_14","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"182-197","source":"Crossref","is-referenced-by-count":1,"title":["Polynomial Time Image Computation with Interval-Definable Counters Systems"],"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":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2000","unstructured":"Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 419\u2013434. Springer, Heidelberg (2000)"},{"key":"14_CR2","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-the-fly 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":"14_CR3","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":"14_CR4","unstructured":"Alv homepage, \n                    \n                      http:\/\/www.cs.ucsb.edu\/~bultan\/composite\/"},{"key":"14_CR5","unstructured":"Babylon homepage, \n                    \n                      http:\/\/www.ulb.ac.be\/di\/ssd\/lvbegin\/CST\/-index.html"},{"key":"14_CR6","unstructured":"Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. Technical Report ucsb cs:TR-2002-16, University of California, Santa Barbara, Computer Science (2002)"},{"key":"14_CR7","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. Bartzis","year":"2003","unstructured":"Bartzis, 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":"14_CR8","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":"14_CR9","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":"14_CR10","doi-asserted-by":"crossref","unstructured":"Berman, L.: Precise bounds for Presburger arithmetic and the reals with addition: Preliminary report. In: Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS 1977), Providence, Rhode Island, November-31, October-2, pp. 95\u201399. IEEE, USA (1977)","DOI":"10.1109\/SFCS.1977.23"},{"key":"14_CR11","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":"14_CR12","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":"14_CR13","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 model-checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"issue":"1-2","key":"14_CR14","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-2), 211\u2013250 (1999)","journal-title":"Theoretical Computer Science"},{"key":"14_CR15","unstructured":"Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science (to appear)"},{"key":"14_CR16","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"14_CR17","unstructured":"Brain homepage, \n                    \n                      http:\/\/www.cs.man.ac.uk\/~voronkov\/BRAIN\/index.html"},{"key":"14_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":"14_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":"14_CR20","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., Begin, L.V.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 298\u2013310. Springer, Heidelberg (2001)"},{"key":"14_CR21","unstructured":"Fast homepage, \n                    \n                      http:\/\/www.lsv.ens-cachan.fr\/fast\/"},{"key":"14_CR22","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":"14_CR23","unstructured":"Finkel, A., McKenzie, P., Picaronny, C.: 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":"14_CR24","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":"14_CR25","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., Purushothaman Iyer, S., 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":"14_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! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"key":"14_CR27","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/B978-0-12-417750-5.50022-1","volume-title":"Theory of Machines and Computations","author":"J.E. Hopcroft","year":"1971","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing the states in a finite-automaton. In: Kohavi, Z. (ed.) Theory of Machines and Computations, pp. 189\u2013196. Academic Press, London (1971)"},{"issue":"4","key":"14_CR28","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":"14_CR29","unstructured":"Lash homepage, \n                    \n                      http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"14_CR30","unstructured":"Leroux, J.: The affine hull of a binary automaton is computable in polynomial time. In: 5th Int. Workshop on Verification of Infinite-State Systems, Electronic Notes in Theor. Comp. Sci. (2003) (to appear)"},{"key":"14_CR31","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":"14_CR32","unstructured":"Mona homepage, \n                    \n                      http:\/\/www.brics.dk\/mona\/index.html"},{"issue":"5","key":"14_CR33","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"P. Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters\u00a083(5), 251\u2013261 (2002)","journal-title":"Information Processing Letters"},{"key":"14_CR34","unstructured":"Strehl, K.: Using interval diagram techniques for the symbolic verification of timed automata. Technical Report 53, Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH) Zurich, Gloriastrasse 35, CH-8092 Zurich (July 1998)"},{"key":"14_CR35","unstructured":"TReX homepage, \n                    \n                      http:\/\/www.liafa.jussieu.fr\/~sighirea\/trex\/"},{"key":"14_CR36","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","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:38:49Z","timestamp":1558298329000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}