{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:54:21Z","timestamp":1773654861518,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540002253","type":"print"},{"value":"9783540362067","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36206-1_14","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T07:23:08Z","timestamp":1187248988000},"page":"145-156","source":"Crossref","is-referenced-by-count":81,"title":["How to Compose Presburger-Accelerations: Applications to Broadcast Protocols"],"prefix":"10.1007","author":[{"given":"Alain","family":"Finkel","sequence":"first","affiliation":[]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-49059-0_15","volume-title":"(TACAS\u201999)","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In (TACAS\u201999), volume 1579 of LNCS, pages 208\u2013222. Springer-Verlag, 1999."},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"(CAV\u201900)","author":"A. Annichini","year":"2000","unstructured":"A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In (CAV\u201900), volume 1855 of LNCS, pages 419\u2013434. Springer-Verlag, 2000."},{"issue":"2","key":"14_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P. A. Abdulla","year":"1996","unstructured":"P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91\u2013101, june 1996.","journal-title":"Information and Computation"},{"key":"14_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"(CONCUR\u201997)","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In (CONCUR\u201997), volume 1243 of LNCS, pages 135\u2013150. Springer-Verlag, June 1997."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"(CONCUR\u201999)","author":"B. B\u00e9rard","year":"1999","unstructured":"B. B\u00e9rard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In (CONCUR\u201999), volume 1664 of LNCS, pages 178\u2013193. Springer-Verlag, 1999."},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/3-540-46419-0_15","volume-title":"(TACAS\u201900)","author":"J.-P. Bodeveix","year":"2000","unstructured":"J.-P. Bodeveix and M. Filali. Fmona: a tool for expressing validation techniques over infinite state systems. In (TACAS\u201900), volume 1785 of LNCS, pages 204\u2013219. Springer-Verlag, march 2000."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"(CAV\u201997)","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic model checking of infinite state systems using presburger arithmetic. In (CAV\u201997), volume 1254 of LNCS, pages 400\u2013411. Springer-Verlag, 1997."},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/BFb0032741","volume-title":"(SAS\u201997)","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In (SAS\u201997), volume 1302 of LNCS, pages 172\u2013186. Springer-Verlag, 1997."},{"issue":"1\u20132","key":"14_CR9","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A. Bouajjani","year":"1999","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFOchannel systems with nonregular sets of configurations. Theoretical Computer Science, 221(1\u20132):211\u2013250, June 1999.","journal-title":"Theoretical Computer Science"},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"(CAV\u201900)","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In (CAV\u201900), volume 1855 of LNCS, pages 403\u2013418. Springer-Verlag, July 2000."},{"key":"14_CR11","unstructured":"B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge, 1998."},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"(CAV\u201994)","author":"B. Boigelot","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In (CAV\u201994), volume 818 of LNCS, pages 55\u201367. Springer-Verlag, 1994."},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"(CAV\u201998)","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In (CAV\u201998), volume 1427 of LNCS, pages 268\u2013279. Springer-Verlag, 1998."},{"key":"14_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"(CAV\u201900)","author":"G. Delzann","year":"2000","unstructured":"Giorgio Delzann. Automatic verification of parameterized cache coherence protocols (extended and revised version). In (CAV\u201900), volume 1855 of LNCS, pages 53\u201368. Springer-Verlag, 2000."},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"(ICALP\u201998)","author":"C. Dufourd","year":"1998","unstructured":"C. Dufourd, A. Finkel, and P. Schnoebelen. Reset nets between decidability and undecidability. In (ICALP\u201998), volume 1443 of LNCS, pages 103\u2013115. Springer-Verlag, July 1998."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In (LICS\u201999), pages 352\u2013359. IEEE Computer Society, July 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"A. Emerson and K. Namjoshi. On model checking for non-deterministic infinite-state systems. In (LICS\u201998), pages 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"14_CR18","unstructured":"R. Floyd and R. W Beigel. Le langage des machines: introduction a la calculabilite et aux langages formels, chapter 7, page 433. (ITP 1995), 1995."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. Technical report, Laboratoire Sp\u00e9cification et V\u00e9rification, CNRS UMR 8643 amp; ENS de Cachan, 2002.","DOI":"10.1007\/3-540-36206-1_14"},{"issue":"3\/4","key":"14_CR20","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"L. Fribourg and H. Ols\u00e9n. A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints, 2(3\/4):305\u2013335, 1997.","journal-title":"Constraints"},{"key":"14_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-63141-0_15","volume-title":"(CONCUR\u201997)","author":"L. Fribourg","year":"1997","unstructured":"L. Fribourg and H. Ols\u00e9n. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In (CONCUR\u201997), volume 1243 of LNCS, pages 213\u2013227. Springer-Verlag, 1997."},{"key":"14_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1007\/3-540-44618-4_40","volume-title":"(CONCUR\u20192000)","author":"A. Finkel","year":"2000","unstructured":"A. Finkel, S. Purushothaman Iyer, and G. Sutre. Well-abstracted transition systems. In (CONCUR\u20192000), volume 1877 of LNCS, pages 566\u2013580. Springer-Verlag, 2000."},{"key":"14_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-44612-5_31","volume-title":"(MFCS\u20192000)","author":"A. Finkel","year":"2000","unstructured":"A. Finkel and G. Sutre. An algorithm constructing the semilinear post* for 2-dim reset\/transfer vass. In (MFCS\u20192000), volume 1893 of LNCS, pages 353\u2013362. Springer-Verlag, 2000."},{"key":"14_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-46541-3_29","volume-title":"(STACS\u20192000)","author":"A. Finkel","year":"2000","unstructured":"A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. In (STACS\u20192000), volume 1770 of LNCS, pages 346\u2013357. Springer-Verlag, Feb 2000."},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems (extended abstract). In (INFINITY\u2019 97), volume 9 of Electronical Notes in Theoretical Computer Science. Elsevier Science, July 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"issue":"2","key":"14_CR26","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285\u2013296, 1966.","journal-title":"Pacific Journal of Mathematics"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0021-8693(78)90249-1","volume":"52","author":"G. Jacob","year":"1978","unstructured":"G. Jacob. La finitude des representations lineaires des semi-groupes est decidable. J. Algebra, 52:437\u2013459, 1978.","journal-title":"J. Algebra"},{"issue":"2","key":"14_CR28","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(77)90001-9","volume":"5","author":"A. Mandel","year":"1977","unstructured":"A. Mandel and I. Simon. On finite semigroups of matrices. Theoretical Computer Science, 5(2):101\u2013111, October 1977.","journal-title":"Theoretical Computer Science"},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1016\/0021-8693(75)90184-2","volume":"34","author":"R. McNaughton","year":"1975","unstructured":"R. McNaughton and Y. Zalcstein. The burnside theorem for semi-groups. J. Algebra, 34:292\u2013299, 1975.","journal-title":"J. Algebra"},{"key":"14_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"(CAV\u201900)","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verication. In (CAV\u201900), volume 1855 of LNCS, pages 328\u2013343. Springer-Verlag, July 2000."},{"key":"14_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-53507-1_77","volume-title":"A closed form for Datalog queries with integer order","author":"P. Z. Revesz","year":"1990","unstructured":"P. Z. Revesz. A closed form for Datalog queries with integer order. In ICDT\u201990, Third International Conference on Database Theory, volume 470 of LNCS, pages 187\u2013201. Springer-Verlag, December 1990."},{"key":"14_CR32","series-title":"Lect Notes Comput Sci","first-page":"106","volume-title":"(AMAST\u201998)","author":"G. Sutre","year":"1999","unstructured":"G. Sutre, A. Finkel, O. Roux, and F. Cassez. Effective recognizability and model checking of reactive fiffo automata. In (AMAST\u201998), volume 1548 of LNCS, pages 106\u2013123. Springer-Verlag, 1999."},{"key":"14_CR33","unstructured":"G. Sutre. Abstraction et acc\u00e9l\u00e9ration de syst\u00e8mes infinis. PhD thesis, Ecole Normale Sup\u00e9rieure de Cachan, Laboratoire Sp\u00e9cification et V\u00e9rification. CNRS UMR 8643, october 2000."},{"key":"14_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"(CAV\u201998)","author":"P. Wolper","year":"1998","unstructured":"P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In (CAV\u201998), volume 1427 of LNCS, pages 88\u201397, June 1998."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36206-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T11:23:26Z","timestamp":1737372206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36206-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540002253","9783540362067"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-36206-1_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}