{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214379},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_14","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"188-203","source":"Crossref","is-referenced-by-count":29,"title":["Abstracting WS1S Systems to Verify Parameterized Networks"],"prefix":"10.1007","author":[{"given":"Kai","family":"Baukus","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[]},{"given":"Karsten","family":"Stahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"CAV\u2019 99","author":"P.A. Abdulla","year":"1999","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\u2019 99, volume 1633 of LNCS, pages 134\u2013145. Springer, 1999. 189, 191, 202"},{"issue":"6","key":"14_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. Apt","year":"1986","unstructured":"K. Apt and D. Kozen. Limits for Automatic Verification of Finit-State Concurrent Systems. Information Processing Letters, 22(6):307\u2013309, 1986. 188","journal-title":"Information Processing Letters"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. Information and Computation, 1989. 188","DOI":"10.1016\/0890-5401(89)90026-6"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J.R. B\u00fcchi","year":"1960","unstructured":"J.R. B\u00fcchi. Weak Second-Order Arithmetic and Finite Automata. Z. Math. Logik Grundl. Math., 6:66\u201392, 1960. 190","journal-title":"Z. Math. Logik Grundl. Math."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0016951","volume-title":"CONCUR\u2019 95: Concurrency Theory","author":"E. Clarke","year":"1995","unstructured":"E. Clarke, O. Grumberg, and S. Jha. Verifying Parameterized Networks using Abstraction and Regular Languages. In I. Lee and S. Smolka, editors, CONCUR\u2019 95: Concurrency Theory, LNCS. Springer, 1995. 188"},{"issue":"5","key":"14_CR6","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994. 189, 195","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR7","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In E.-R. Olderog, editor, Proceedings of PROCOMET\u2019 94. North-Holland, 1994. 189, 195"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.2307\/1993511","volume":"98","author":"C.C. Elgot","year":"1961","unstructured":"C.C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21\u201352, 1961. 190","journal-title":"Trans. Amer. Math. Soc."},{"key":"14_CR9","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. 188","DOI":"10.1145\/199448.199468"},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"8th Conference on Computer Aided Verification","author":"E. A. Emerson","year":"1996","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. 188"},{"key":"14_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u2019 97","year":"1997","unstructured":"O. Grumberg, editor. Proceedings of CAV\u2019 97, volume 1256 of LNCS. Springer, 1997. 203"},{"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. 188","journal-title":"Journal of the ACM"},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u2019 97","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In Grumberg [Gru97]. 194"},{"key":"14_CR14","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u2019 95","author":"H.J.J.+.9.6._.J.G. Henriksen","year":"1996","unstructured":"HJJ+96._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\u2019 95, volume 1019 of LNCS. Springer, 1996. 190, 194, 198"},{"issue":"6\/7","key":"14_CR15","first-page":"188","volume":"22","author":"N. Halbwachs","year":"1992","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 22(6\/7), 1992. 188","journal-title":"Acta Informatica"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In ACM Symp. on Principles of Distributed Computing, Canada, pages 239\u2013247, Edmonton, Alberta, 1989. 188","DOI":"10.1145\/72981.72998"},{"key":"14_CR17","unstructured":"N. Klarlund and A. M\u00f8ller. MONA Version 1.3 User Manual. BRICS, 1998. 190, 194, 198"},{"key":"14_CR18","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Proceedings of CAV\u2019 97","author":"K.M.M.+.9.7._.Y. Kesten","year":"1997","unstructured":"KMM+97._Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Grumberg [Gru97], pages 424\u2013435. 189"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"LGS+95._C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995. 189, 195","DOI":"10.1007\/BF01384313"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL\u2019 97, Paris, 1997. 188","DOI":"10.1145\/263699.263747"},{"key":"14_CR21","unstructured":"Z. Manna and A. Pnueli. Verification of parameterized programs. In E. Borger, editor, Specification and Validation Methods, pages 167\u2013230, Oxford University Press, 1994. 189"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems, Safety. Springer Verlag, 1995. 191","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"14_CR23","series-title":"Lect Notes Comput Sci","first-page":"151","volume-title":"Proc. Workshop on Automatic Verification Methods for Finite State Systems","author":"Z. Stadler","year":"1989","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. 188"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"B.K. Szymanski. A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In Proceedings of International Conference on Supercomputing Systems 1988, pages 621\u2013626, St. Malo, France, July 1988. 191","DOI":"10.1145\/55364.55425"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics, pages 134\u2013191. Elsevier Science Publishers B. V., 1990. 190","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"14_CR26","series-title":"Lect Notes Comput Sci","first-page":"68","volume-title":"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, Workshop on Computer Aided Verification, LNCS 407, pages 68\u201380, 1989. 188"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T21:07:13Z","timestamp":1556744833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}