{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:53:54Z","timestamp":1773615234832,"version":"3.50.1"},"reference-count":27,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T00:00:00Z","timestamp":1291161600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T00:00:00Z","timestamp":1291161600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Conrol Comp. Sci."],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.3103\/s0146411610070035","type":"journal-article","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T11:08:02Z","timestamp":1295003282000},"page":"378-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On application of weaker simulations to parameterized model checking by network invariants technique"],"prefix":"10.3103","volume":"44","author":[{"given":"I. V.","family":"Konnov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2011,1,15]]},"reference":[{"key":"6110_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Jonsson, B., Nilsson, M., and Saksena, M., A Survey of Regular Model Checking, Proc. 15th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, 2004, pp. 35\u201348.","DOI":"10.1007\/978-3-540-28644-8_3"},{"issue":"6","key":"6110_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R. and Kozen, D., Limits for Automatic Program Verification of Finite-State Concurrent Systems, Information Processing Letters, 1986, vol. 22, no. 6, pp. 307\u2013309.","journal-title":"Information Processing Letters"},{"key":"6110_CR3","unstructured":"Calder, M. and Miller, A., Five Ways to Use Induction and Symmetry in the Verification of Networks of Processes by Model-Checking, Proc. AvoCS 2002 (Automated Verification of Critical Systems), 2002, pp. 29\u201342."},{"key":"6110_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., and Jha, S., Verifying Parameterized Networks Using Abstraction and Regular Languages, Proc. 6th International Conference on Concurrency Theory, 1995, pp. 395\u2013407.","DOI":"10.1007\/3-540-60218-6_30"},{"issue":"5","key":"6110_CR5","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., and Jha, S., Verifying Parameterized Networks, ACM Transactions on Programming Languages and Systems, 1997, vol. 19, no. 5, pp. 726\u2013750.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6110_CR6","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D., Model Checking, MIT Press, 2000."},{"key":"6110_CR7","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume":"3170","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Touili, T., and Veith, H., Verification by Network Decomposition, Proc. CONCUR\u201904, Lecture Notes in Computer Science, 2004, vol. 3170, pp. 276\u2013291.","journal-title":"Proc. CONCUR\u201904, Lecture Notes in Computer Science"},{"key":"6110_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E.A. and Namjoshi, K.S., Reasoning about Rings, Proc. 22th ACM Conf. on Principles of Programming Languages, POPL\u201995, 1995, pp. 85\u201394.","DOI":"10.1145\/199448.199468"},{"issue":"1\/2","key":"6110_CR9","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A. and Sistla, A.P., Symmetry and Model Checking, Formal Methods in System Design, 1996, vol. 9, no. 1\/2, pp. 105\u2013131.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"6110_CR10","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1006\/inco.1998.2778","volume":"150","author":"R. Gerth","year":"1999","unstructured":"Gerth, R., Kuiper, R., Peled, D., and Penczek, W., A Partial Order Approach to Branching Time Logic Model Checking, Information and Computation, 1999, vol. 150, no. 2, pp. 132\u2013152.","journal-title":"Information and Computation"},{"issue":"3","key":"6110_CR11","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J. and Weijland, W.P., Branching Time and Abstraction in Bisimulation Semantics, Journal of the ACM, 1996, vol. 43, no. 3, pp. 555\u2013600.","journal-title":"Journal of the ACM"},{"issue":"1","key":"6110_CR12","first-page":"270","volume":"3","author":"G. Holzmann","year":"1998","unstructured":"Holzmann, G. and Puri, A., A Minimized Automaton Representation of Reachable States, in Software Tools for Technology Transfer, 1998, vol. 3, no. 1, pp. 270\u2013278.","journal-title":"Software Tools for Technology Transfer"},{"key":"6110_CR13","unstructured":"Holzmann, G., The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003."},{"key":"6110_CR14","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C.N. Ip","year":"1999","unstructured":"Ip, C.N. and Dill, D.L., Verifing Systems with Replicating Components in Murphi, Formal Methods in System Design, 1999, vol. 14, pp. 273\u2013310.","journal-title":"Formal Methods in System Design"},{"key":"6110_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y. and Pnueli, A., Verification by Finitary Abstraction, Information and Computation, 2000, vol. 163, pp. 203\u2013243.","journal-title":"Information and Computation"},{"key":"6110_CR16","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P. and MacMillan, K.L., Structural Induction Theorem for Processes, Proc. the 8th International Symposium on Principles of Distributed Computing, PODC\u201989, 1989, pp. 239\u2013247.","DOI":"10.1145\/72981.72998"},{"issue":"5","key":"6110_CR17","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s11086-005-0034-4","volume":"31","author":"I.V. Konnov","year":"2005","unstructured":"Konnov, I.V. and Zakharov, V.A., An Approach to the Verification of Symmetric Parameterized Distributed Systems, Programming and Computer Software, 2005, vol. 31, no. 5, pp. 225\u2013236.","journal-title":"Programming and Computer Software"},{"key":"6110_CR18","series-title":"RISC-Linz Report Series","first-page":"41","volume-title":"International Workshop on Invariant Generation (WING\u201907)","author":"V. Zakharov","year":"2007","unstructured":"Zakharov, V. and Konnov, I., An Invariant-Based Approach to the Verification of Asynchronous Parameterized Networks, International Workshop on Invariant Generation (WING\u201907), RISC-Linz Report Series no. 07-07. RISC, Hagenberg, Austria, 2007, pp. 41\u201355."},{"key":"6110_CR19","doi-asserted-by":"crossref","unstructured":"Lesens, D., Invariants of Parameterized Binary Tree Networks as Greatest Fixpoints, Proc. Sixth International Conference on Algebraic Methodology and Software Technology, AMAST\u201997, 1997, pp. 337\u2013350.","DOI":"10.1007\/BFb0000481"},{"key":"6110_CR20","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/263699.263747","volume-title":"Proc. the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"D. Lesens","year":"1997","unstructured":"Lesens, D., Halbwachs, N., and Raymond, P., Automatic Verification of Parameterized Linear Networks of Processes, POPL\u201997, Proc. the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (ACM, New York, NY, USA, 1997), pp. 346\u2013357."},{"key":"6110_CR21","doi-asserted-by":"crossref","unstructured":"Manku, G.S., Hojati, R., and Brayton, R.K., Structural Symmetries and Model Checking, Proc. International Conference on Computer-Aided Verification (CAV\u201998), 1998, pp. 159\u2013171.","DOI":"10.1007\/BFb0028742"},{"key":"6110_CR22","unstructured":"Marelly, R. and Grumberg, O., Gormel-Grammar Oriented Model Checker, Technical Report 697, The Technion, 1991."},{"key":"6110_CR23","volume-title":"Regular Model Checking","author":"M. Nilsson","year":"2005","unstructured":"Nilsson, M., Regular Model Checking, PhD Thesis, Uppsala, Sweden: Uppsala University, 2005."},{"key":"6110_CR24","unstructured":"Penczek, W., Gerth, R., Kuiper, R., and Szreter, M., Partial Order Reductions Preserving Simulations, 1999."},{"key":"6110_CR25","unstructured":"Braden, R., Resource Reservation Protocol (RSVP), 1997, http:\/\/tools.ietf.org\/html\/rfc2205."},{"key":"6110_CR26","unstructured":"Shahar, E., Tools and Techniques for Verifying Parameterized Systems, PhD Thesis Weizmann Institute of Science, 2001."},{"key":"6110_CR27","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume":"407","author":"P. Wolper","year":"1989","unstructured":"Wolper, P. and Lovinfosse, V., Properties of Large Sets of Processes with Network Invariants, Lecture Notes in Computer Science, 1989, vol. 407, pp. 68\u201380.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610070035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411610070035","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610070035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411610070035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:13Z","timestamp":1773611833000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411610070035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":27,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["6110"],"URL":"https:\/\/doi.org\/10.3103\/s0146411610070035","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12]]},"assertion":[{"value":"2 June 2008","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 January 2011","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}