{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T19:32:51Z","timestamp":1793129571531,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"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":[[1996]]},"DOI":"10.1007\/3-540-61474-5_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:41:57Z","timestamp":1330292517000},"page":"87-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":52,"title":["Automatic verification of parameterized synchronous systems"],"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,3]]},"reference":[{"key":"8_CR1","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":"no.1","key":"8_CR2","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":"8_CR3","unstructured":"Clarke, E.M., Emerson, E.A. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Workshop on Logics of Programs, Springer-Verlag LNCS 131."},{"issue":"no.2","key":"8_CR4","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 Sys., vol. 8, no. 2, pp. 244\u2013263, April 1986.","journal-title":"ACM Trans. Prog. Lang. and Sys."},{"key":"8_CR5","unstructured":"Clarke, E.M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th CAV, Springer-Verlag LNCS 697."},{"key":"8_CR6","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":"8_CR7","unstructured":"Clarke, E.M., Grumberg, O., Jha, S. Verifying Parameterized Networks using Abstraction and Regular Languages. CONCUR 95."},{"key":"8_CR8","volume-title":"Handbook of Theoretical Computer Science, vol. B","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. B, (J. van Leeuwen, ed.), Elsevier\/North-Holland, 1991."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S. Reasoning about Rings. Proc. ACM Symposium on Principles of Programming Languages, 1995.","DOI":"10.1145\/199448.199468"},{"key":"8_CR10","unstructured":"Emerson, E.A., Sistla, A.P. Symmetry and Model Checking, 5th CAV, Springer-Verlag LNCS 697."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic approach. CAV 1995.","DOI":"10.1007\/3-540-60045-0_59"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Srinivasan, J. A decidable temporal logic to reason about many processes. PODC 1990.","DOI":"10.1145\/93385.93425"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"German, S.M., Sistla, A.P. Reasoning about Systems with Many Processes. J.ACM, Vol. 39, Number 3, July 1992.","DOI":"10.1145\/146637.146681"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Hojati, R., Brayton, R. Automatic Datapath Abstraction in Hardware Systems, CAV 1995.","DOI":"10.1007\/3-540-60045-0_43"},{"key":"8_CR15","unstructured":"Ip, C., Dill, D. Better verification through symmetry. Proc. 11th Intl. Symp. on Computer Hardware Description Languages and their Applications."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, K. A Structural Induction Theorem for Processes, PODC 1989.","DOI":"10.1145\/72981.72998"},{"issue":"2","key":"8_CR17","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(94)90113-9","volume":"135","author":"J. Li","year":"1994","unstructured":"Li, J., Suzuki, I., Yamashita, M. Fair Petri Nets and structural induction for rings of processes. Theoretical Computer Science, vol. 135(2), 1994. pp. 337\u2013404.","journal-title":"Theoretical Computer Science"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL 85, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"8_CR19","unstructured":"Long, D. Model Checking, Abstraction, and Compositional Verification. Ph.D. Thesis, Carnegie-Mellon University, 1993."},{"key":"8_CR20","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":"8_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A. Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"8_CR22","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":"8_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A. The Temporal Logic of Programs. FOCS 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR24","unstructured":"Pong, F., Dubois, M. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, August 1995."},{"key":"8_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":"8_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, LNCS 697.","DOI":"10.1007\/3-540-56922-7_11"},{"key":"8_CR27","unstructured":"SAE J1850 Class B data communication network interface. Society of Automotive Engineers, Inc., 1992."},{"key":"8_CR28","unstructured":"Shtadler, Z., Grumberg, O. Network Grammars, Communication Behaviours and Automatic Verification. Springer-Verlag, LNCS 407."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Suzuki, I. Proving properties of a ring of finite state machines. IPL 28, pp. 213\u2013214.","DOI":"10.1016\/0020-0190(88)90211-6"},{"key":"8_CR30","unstructured":"Vardi, M. An Automata-theoretic Approach to Linear Temporal Logic, Proceedings of Banff Higher Order Workshop on Logics for Concurrency, F. Moller, ed., Springer-Verlag LNCS, to appear."},{"key":"8_CR31","unstructured":"Vardi, M., Wolper, P. An Automata-theoretic Approach to Automatic Program Verification, Proc. IEEE LICS, pp. 332\u2013344, 1986."},{"key":"8_CR32","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":"8_CR33","unstructured":"Wolper, P., Lovinfosse, V. Verifying Properties of Large Sets of Processes with Network Invariants. Springer-Verlag, LNCS 407."}],"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-61474-5_60","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:19:38Z","timestamp":1742599178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_60"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}