{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T13:56:58Z","timestamp":1789999018345,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_54","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"690-705","source":"Crossref","is-referenced-by-count":14,"title":["A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yan","family":"Jurski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"54_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: General decidability theorems for infinite-state systems. In: Proc. of LICS\u201996, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"54_CR2","unstructured":"Abdulla, P.A., Delzanno, G.: On the Coverability Problem for Constrained Multiset Rewriting. In: Proc. of AVIS\u201906, Satellite workshop of ETAPS\u201906, Vienna, Austria (2006)"},{"key":"54_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., et al.: A Survey of Regular Model Checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, Springer, Heidelberg (2004)"},{"key":"54_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying Networks of Timed Processes (Extended Abstract). In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 298\u2013312. Springer, Heidelberg (1998)"},{"key":"54_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2000)"},{"key":"54_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., et al.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"54_CR7","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Space. PhD thesis, Facult\u00e9 des Sciences, Universit\u00e9 de Li\u00e8ge, vol. 189 (1999)"},{"key":"54_CR8","volume-title":"Proc. of PODS\u201906","author":"M. Bojanczyk","year":"2006","unstructured":"Bojanczyk, M., et al.: Two-variable logic on data trees and XML reasoning. In: Proc. of PODS\u201906, ACM Press, New York (2006)"},{"key":"54_CR9","volume-title":"Proc. of LICS\u201906","author":"M. Bojanczyk","year":"2006","unstructured":"Bojanczyk, M., et al.: Two-variable logic on words with data. In: Proc. of LICS\u201906, IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"54_CR10","series-title":"Universitext","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"2001","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem, 2nd edn. Universitext. Springer, Heidelberg (2001)","edition":"2"},{"key":"54_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"54_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"54_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., et al.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"54_CR14","unstructured":"Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. Technical Report 2007-01, LIAFA lab (January 2007), Available at http:\/\/www.liafa.jussieu.fr\/~abou\/publis.html"},{"key":"54_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, Springer, Heidelberg (2005)"},{"key":"54_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Touili, T.: On computing reachability sets of process rewrite systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, Springer, Heidelberg (2005)"},{"key":"54_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_3","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2001","unstructured":"Bouajjani, A.: Languages, Rewriting systems, and Verification of Infinte-State Systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, Springer, Heidelberg (2001)"},{"key":"54_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Beyond Parameterized Verification. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, Springer, Heidelberg (2002)"},{"key":"54_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"key":"54_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. TOPLAS\u00a019(5) (1997)","DOI":"10.1145\/265943.265960"},{"key":"54_CR21","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: An assertional language for the verification of systems parametric in several dimensions. Electr. Notes Theor. Comput. Sci.\u00a050(4) (2001)","DOI":"10.1016\/S1571-0661(04)00189-6"},{"key":"54_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"key":"54_CR23","volume-title":"Proc. of LICS\u201906","author":"S. Demri","year":"2006","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. In: Proc. of LICS\u201906, IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"54_CR24","volume-title":"LICS\u201998","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS\u201998, IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"54_CR25","first-page":"352","volume-title":"Proceedings of LICS \u201999","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of LICS \u201999, pp. 352\u2013359. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"54_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2002)"},{"issue":"1-2","key":"54_CR27","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(1-2), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"54_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le M\u00e9tayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol.\u00a02305, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"54_CR29","doi-asserted-by":"crossref","unstructured":"German, S.M., Sistla, P.A.: Reasoning about systems with many processes. JACM\u00a039(3) (1992)","DOI":"10.1145\/146637.146681"},{"key":"54_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"54_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:57Z","timestamp":1605763017000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_54","relation":{},"subject":[]}}