{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T23:12:42Z","timestamp":1768259562014,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662020","type":"print"},{"value":"9783540486831","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_14","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"134-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":48,"title":["Handling Global Conditions in Parametrized System Verification"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Nilsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"14_CR1","first-page":"305","volume":"1427","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 305\u2013318, 1998.","journal-title":"Proc. 10th Int. Conf. on Computer Aided Verification"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, pages 414\u2013425, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"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":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91\u2013101, 1996.","journal-title":"Information and Computation"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed processes. In Bernhard Steffen, editor, Proc. TACAS\u2019 98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 298\u2013312, 1998.","DOI":"10.1007\/BFb0054179"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. 8th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1\u201312. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Fourth International Static Analysis Symposium","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. of the Fourth International Static Analysis Symposium, Lecture Notes in Computer Science. Springer Verlag, 1997."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ICALP\u2019 97","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifochannel systems with nonregular sets of configurations. In Proc. ICALP\u2019 97, number 1256 in Lecture Notes in Computer Science, 1997."},{"issue":"2","key":"14_CR8","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"O. Burkart and B. Steffen. Composition, decomposition, and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89\u2013125, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"K. \u010cer\u0101ns. Deciding properties of integral relational automata. In Abiteboul and Shamir, editors, Proc. ICALP\u2019 94, volume 820 of Lecture Notes in Computer Science, pages 35\u201346. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58201-0_56"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In Lee and Smolka, editors, Proc. CONCUR\u2019 95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 395\u2013407. Springer Verlag, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"14_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-60249-6_54","volume-title":"Proc. Fundementals of Computation Theory","author":"J. Esparza","year":"1995","unstructured":"J. Esparza. Petri nets, commutative context-free grammers, and basic parallel processes. In Proc. Fundementals of Computation Theory, number 965 in Lecture Notes in Computer Science, pages 221\u2013232, 1995."},{"issue":"3","key":"14_CR12","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675\u2013735, 1992.","journal-title":"Journal of the ACM"},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/BFb0054187","volume-title":"Proc. TACAS\u2019 98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"E.P. Gribomont","year":"1998","unstructured":"E.P. Gribomont and G. Zenner. Automated verification of Szymanski\u2019s algorithm. In Proc. TACAS\u2019 98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 424\u2013438, 1998."},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(90)90006-4","volume":"74","author":"P. Jan_car","year":"1990","unstructured":"P. Jan_car. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 74:71\u201393, 1990.","journal-title":"Theoretical Computer Science"},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BFb0054186","volume-title":"Proc. TACAS\u2019 98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Jensen","year":"1998","unstructured":"E. Jensen and N. A. Lynch. A proof of Burn\u2019s n-process mutual exclusion algorithm using abstraction. In Proc. TACAS\u2019 98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 409\u2013423, 1998."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In Proc. 8th ACM Symp. on Principles of Distributed Computing, Canada, pages 239\u2013247, Edmonton, Alberta, 1989.","DOI":"10.1145\/72981.72998"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"[KMM+97]_ Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254, pages 424\u2013435, Haifa, Israel, 1997. Springer Verlag.","DOI":"10.1007\/3-540-63166-6_41"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"[MAB+94]_ Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. chang, M. Col_on, L. de Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STEP: the stanfor temporal prover. Draft Manuscript, June 1994.","DOI":"10.21236\/ADA324036"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. An exercise in the verification of multi-process programs. In W.H.J. Feijen, A.J.M van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, pages 289\u2013301. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-4476-9_34"},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","first-page":"68","volume-title":"Proc. Workshop on Computer Aided Verification","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants (extended abstract). In Sifakis, editor, Proc. Workshop on Computer Aided Verification, number 407 in Lecture Notes in Computer Science, pages 68\u201380, 1989."},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184\u2013193, Jan. 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T12:37:01Z","timestamp":1737463021000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}