{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T19:18:38Z","timestamp":1789845518053,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028766","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"452-463","source":"Crossref","is-referenced-by-count":10,"title":["Verification of a parameterized bus arbitration protocol"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T., Vardi, M. Parametric Real-Time Reasoning, STOC, 1993.","DOI":"10.1145\/167088.167242"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"Apt, K., Kozen, D. Limits for automatic verification of finite-state concurrent systems. IPL 15, pp. 307\u2013309.","DOI":"10.1016\/0020-0190(86)90071-2"},{"issue":"1","key":"41_CR3","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M. C. Browne","year":"1989","unstructured":"Browne, M. C., Clarke, E. M., Grumberg, O. Reasoning about Networks with Many Identical Finite State Processes, Information and Computation, vol. 81, no. 1, pp. 13\u201331, April 1989.","journal-title":"Information and Computation"},{"key":"41_CR4","unstructured":"Clarke, E. M., Emerson, E. A. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. in Workshop on Logics of Programs, Springer-Verlag LNCS 131."},{"issue":"2","key":"41_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite-State Concurrent Systems using Temporal Logic, ACM Trans. Prog. Lang. and Syst., vol. 8, no. 2, pp. 244\u2013263, April 1986.","journal-title":"ACM Trans. Prog. Lang. and Syst."},{"key":"41_CR6","unstructured":"Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th CAV, Springer-Verlag LNCS 697."},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O. Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms, PODC, 1987.","DOI":"10.1145\/41840.41865"},{"key":"41_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S. Verifying Parameterized Networks using Abstraction and Regular Languages, CONCUR, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"41_CR9","unstructured":"Emerson, E. A. Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier\/North-Holland, 1991."},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Namjoshi, K. S. Reasoning about Rings, POPL, 1995.","DOI":"10.1145\/199448.199468"},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Namjoshi, K. S. Automatic Verification of Parameterized Synchronous Systems, CAV 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"41_CR12","unstructured":"Emerson, E. A., Sistla, A. P. Symmetry and Model Checking, 5th CAV Springer-Verlag LNCS 697."},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"German, S. M., Sistla, A. P. Reasoning about Systems with Many Processes. .ACM, Vol. 39, Number 3, July 1992.","DOI":"10.1145\/146637.146681"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"Havelund, K., Shankar, N. Experiments in Theorem Proving and Model Checking for Protocol Verification, FME, 1996.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"Ip, N., Dill, D. Verifying systems with replicated components in Mur\u03c6, CAV, 1996.","DOI":"10.1007\/3-540-61474-5_65"},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Kurshan, R. P., McMillan, K. A Structural Induction Theorem for Processes, PODC, 1989.","DOI":"10.1145\/72981.72998"},{"key":"41_CR17","doi-asserted-by":"crossref","unstructured":"Li, J., Suzuki, I., Yamashita, M. A New Structural Induction Theorem for Rings of Temporal Petri Nets. IEEE Trans. Soft. Engg., vol. 20, No. 2, February 1994.","DOI":"10.1109\/32.265633"},{"key":"41_CR18","doi-asserted-by":"crossref","unstructured":"Lubachevsky, B. An Approach to Automating the Verification of Compact Parallel Coordination Programs I. Acta Informatica 21, 1984.","DOI":"10.1007\/BF00289237"},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie-Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"Misra, J., Chandy, K. M. Parallel Program Design: A Foundation, Addison-Wesley Publishers, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"41_CR21","unstructured":"Manna, Z., Pnueli, A. Verification of Parameterized Programs. In Specification and Validation Methods (E. Borger, ed.), Oxford University Press, pp. 167\u2013230, 1994."},{"key":"41_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A. The Temporal Logic of Programs. FOCS, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"Pong, F., Dubois, M. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, August 1995.","DOI":"10.1109\/71.406955"},{"key":"41_CR24","doi-asserted-by":"crossref","unstructured":"Queille, J.P., J. Sifakis, Specification and Verification of Concurrent Systems in CESAR, Proc. of the 5th International Symposium on Programming, ] LNCS#137, Springer-Verlag, pp. 337\u2013350, April 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"41_CR25","doi-asserted-by":"crossref","unstructured":"Reif, J., Sistla, A. P. A multiprocess network logic with temporal and spatial modalities. JCSS 30(1), 1985.","DOI":"10.1016\/0022-0000(85)90003-0"},{"key":"41_CR26","doi-asserted-by":"crossref","unstructured":"Rho, J. K., Somenzi, F. Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems, CAV, 1993.","DOI":"10.1007\/3-540-56922-7_11"},{"key":"41_CR27","unstructured":"SAE J1850 Class B data communication network interface. Society of Automotive Engineers, Inc., 1992."},{"key":"41_CR28","unstructured":"Shtadler, Z., Grumberg, O. Network Grammars, Communication Behaviours and Automatic Verification. In J.Sifakis (ed), Automatic Verification Methods for Finite State Systems, Springer-Verlag, LNCS 407."},{"key":"41_CR29","unstructured":"Vardi, M., Wolper, P. An Automata-theoretic Approach to Automatic Program Verification, LICS, 1986."},{"key":"41_CR30","unstructured":"Vernier, I. Specification and Verification of Parameterized Parallel Programs. Proc. 8th Intl. Symp. on Computer and Information Sciences, Istanbul, Turkey, pp. 622\u2013625."},{"key":"41_CR31","doi-asserted-by":"crossref","unstructured":"Wolper, P., Lovinfosse, V. Verifying Properties of Large Sets of Processes with Network Invariants. In J.Sifakis (ed), Automatic Verification Methods for Finite State Systems, Springer-Verlag, LNCS 407.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:24:17Z","timestamp":1586593457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028766"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/bfb0028766","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}