{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T18:24:00Z","timestamp":1693851840260},"reference-count":25,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2001,8,1]],"date-time":"2001-08-01T00:00:00Z","timestamp":996624000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4859,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,8]]},"DOI":"10.1016\/s1571-0661(04)00190-2","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"386-400","source":"Crossref","is-referenced-by-count":4,"title":["Networks of Processes with Parameterized State Space"],"prefix":"10.1016","volume":"50","author":[{"given":"K.","family":"Baukus","sequence":"first","affiliation":[]},{"given":"K.","family":"Stahl","sequence":"additional","affiliation":[]},{"given":"S.","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Y.","family":"Lakhnech","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling Global Conditions in Parameterized System Verification. In N. Halbwachs and D. Peled, editors, CAV '99, volume 1633 of LNCS, pages 134\u2013145. Springer, 1999.","DOI":"10.1007\/3-540-48683-6_14"},{"issue":"6","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB2","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","article-title":"Limits for Automatic Verification of Finit-State Concurrent Systems","volume":"22","author":"Apt","year":"1986","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB3","first-page":"188","article-title":"Abstracting WS1S Systems to Verify Parameterized Networks","volume":"volume 1785","author":"Baukus","year":"2000"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB4","first-page":"291","article-title":"Verifying Universal Properties of Parameterized Networks","volume":"volume 1926","author":"Baukus","year":"2000"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB5","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(89)90026-6","article-title":"Reasoning about networks with many identical finite state processes","author":"Browne","year":"1989","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB6","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","article-title":"Weak Second-Order Arithmetic and Finite Automata","volume":"6","author":"B\u00fcchi","year":"1960","journal-title":"Z. Math. Logik Grundl. Math"},{"issue":"5","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB7","doi-asserted-by":"crossref","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB8","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL\u2217, ECTL\u2217 and CTL\u2217. In E.-R. Olderog, editor, Proceedings of PROCOMET '94. North-Holland, 1994."},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB9","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","article-title":"Decision problems of finite automata design and related arithmetics","volume":"98","author":"Elgot","year":"1961","journal-title":"Trans. Amer. Math. Soc"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In 22nd ACM Symposium on Principles of Programming Languages, pages 85\u201394, 1995.","DOI":"10.1145\/199448.199468"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB11","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In 8th Conference on Computer Aided Verification, LNCS 1102, pages 87\u201398, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB12","doi-asserted-by":"crossref","unstructured":"K. Fisler and C. Girault. Modelling and Model Checking a Distributed Shared Memory Consistency Protocol. In ICATPN'98. Springer, 1998.","DOI":"10.1007\/3-540-69108-1_6"},{"issue":"3","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB13","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","article-title":"Reasoning about systems with many processes","volume":"39","author":"German","year":"1992","journal-title":"Journal of the ACM"},{"issue":"6\/7","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB14","article-title":"An experience in proving regular networks of processes by modular model checking","volume":"22","author":"Halbwachs","year":"1992","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB15","doi-asserted-by":"crossref","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic Second-Order Logic in Practice. In TACAS '95, volume 1019 of LNCS. Springer, 1996.","DOI":"10.7146\/brics.v2i21.19923"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB16","doi-asserted-by":"crossref","unstructured":"B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In S. Graf and M. Schwartzbach, editors, TACAS'00, volume 1785. Lecture Notes in Computer Science, 2000.","DOI":"10.1007\/3-540-46419-0_16"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In O. Grumberg, editor, Proceedings of CAV '97, volume 1256 of LNCS, pages 424\u2013435. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_41"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB18","series-title":"ACM Symp. on Principles of Distributed Computing, Canada","first-page":"239","article-title":"A structural induction theorem for processes","author":"Kurshan","year":"1989"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB19","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL '97, Paris, 1997.","DOI":"10.1145\/263699.263747"},{"issue":"4","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB20","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/75104.75105","article-title":"Memory Coherence in Shared Virtual Memory Systems","volume":"7","author":"Li","year":"1989","journal-title":"ACM Trans. on Computer Systems"},{"issue":"1","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB21","doi-asserted-by":"crossref","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for the verification of concurrent systems","volume":"6","author":"Loiseaux","year":"1995","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"10.1016\/S1571-0661(04)00190-2_NEWBIB22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","article-title":"\u201dformal verification for fault-tolerant architectures: Prolegomena to the design of PVS\u201d","volume":"21","author":"Owre","year":"1995","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB23","doi-asserted-by":"crossref","unstructured":"Z. Stadler and O. Grumberg. Network grammars, communication behaviours and automatic verification. In Proc. Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, pages 151\u2013165, Grenoble, France, 1989. Springer Verlag.","DOI":"10.1007\/3-540-52148-8_13"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB24","series-title":"Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics","first-page":"134","article-title":"Automata on infinite objects","author":"Thomas","year":"1990"},{"key":"10.1016\/S1571-0661(04)00190-2_NEWBIB25","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants (extended abstract). In Sifakis, editor, on Computer Aided Verification Workshop, LNCS 407, pages 68\u201380, 1989","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001902?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001902?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:28:23Z","timestamp":1585484903000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,8]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2001,8]]}},"alternative-id":["S1571066104001902"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00190-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,8]]}}}