{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T11:57:31Z","timestamp":1694433451261},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540606307","type":"print"},{"value":"9783540485094","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60630-0_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:49:59Z","timestamp":1330289399000},"page":"133-152","source":"Crossref","is-referenced-by-count":56,"title":["Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock"],"prefix":"10.1007","author":[{"given":"A. W.","family":"Roscoe","sequence":"first","affiliation":[]},{"given":"P. H. B.","family":"Gardiner","sequence":"additional","affiliation":[]},{"given":"M. H.","family":"Goldsmith","sequence":"additional","affiliation":[]},{"given":"J. R.","family":"Hulance","sequence":"additional","affiliation":[]},{"given":"D. M.","family":"Jackson","sequence":"additional","affiliation":[]},{"given":"J. B.","family":"Scattergood","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-15670-4_14","volume":"197","author":"S.D. Brookes","year":"1985","unstructured":"S.D. Brookes and A.W. Roscoe, An improved failures model for communicating processes, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281\u2013305.","journal-title":"Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS"},{"key":"7_CR2","unstructured":"J.R. Burch, E.M. Clarke, D.L. Dill and L.J. Hwang, Symbolic model checking: 1020 states and beyond, Proc. 5th IEEE Annual Symposium on Logic in Computer Science, IEEE Press (1990)."},{"key":"7_CR3","unstructured":"E.M. Clarke, D.E. Long and K.L.MacMillan, Compositional Model Checker, Proceedings of LICS 1989."},{"key":"7_CR4","first-page":"1","volume":"5","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland and M.C.B. Hennessy, Testing Equivalence as a Bisimulation Equivalence, FAC 5 (1993) pp 1\u201320.","journal-title":"FAC"},{"issue":"N.1","key":"7_CR5","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow and B. Steffen, The Concurrency Workbench: A semantics-based verification tool for finite state systems, ACM TOPLAS Vol. 15, N. 1, 1993, pp. 36\u201372.","journal-title":"ACM TOPLAS"},{"key":"7_CR6","unstructured":"Formal Systems (Europe) Ltd., Failures Divergence Refinement User Manual and Tutorial, version 1.4 1994."},{"key":"7_CR7","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"J.-C. Fernandez","year":"1989\/1990","unstructured":"J.-C. Fernandez An implementation of an efficient algorithm for bisimulation equivalence., Science of Computer Programming 13: 219\u2013236, 1989\/1990.","journal-title":"Science of Computer Programming"},{"key":"7_CR8","unstructured":"S.Graf and B. Steffen, Compositional Minimisation of Finite-State Systems, Proceedings of CAV1990 (LNCS 531)."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"J.F. Groote and F. Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, Proc. 17th ICALP, Springer-Verlag LNCS 443, 1990.","DOI":"10.1007\/BFb0032063"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"7_CR11","unstructured":"L. Jategoankar, A Meyer and A.W. Roscoe, Separating failures from divergence, in preparation."},{"key":"7_CR12","unstructured":"R. Kaivola and A Valmari The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic in Proc CONCUR. '92 (LNCS 630)."},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"P.C. Kanellakis and S.A. Smolka, CCS expressions, Finite state processes and three problems of equivalence, Information and Computation 86, 43\u201368 (1990).","journal-title":"Information and Computation"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"7_CR15","volume-title":"Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems","author":"J. Malhotra","year":"1988","unstructured":"Malhotra, J., Smolka, S.A., Giacalone, A. and Shapiro, R., Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems., In Proceedings of the Workshop on Specification and Verification of Concurrent Systems, University of Stirling, Scotland, 1988."},{"key":"7_CR16","unstructured":"K. Melhorn Graph Algorithms and NP Completeness, EATCS Monographs on Theoretical Computer Science, Springer-Verlag 1984."},{"key":"7_CR17","volume-title":"Verification in XE-SAR of the Sliding Window Protocol","author":"J. Richier","year":"1987","unstructured":"J. Richier, C. Rodriguez, J. Sifakis and J. Voiron, Verification in XE-SAR of the Sliding Window Protocol, Proc. of the 7th IFIP Symposium on Protocol Specification, Testing, and Verification, North-Holland, Amsterdam, 1987."},{"issue":"2","key":"7_CR18","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1093\/logcom\/3.2.131","volume":"3","author":"A.W. Roscoe","year":"1993","unstructured":"A.W. Roscoe, Unbounded Nondeterminism in CSP, in \u2018Two Papers on CSP', PRG Monograph PRG-67. Also Journal of Logic and Computation 3, 2 pp. 131\u2013172 (1993).","journal-title":"Also Journal of Logic and Computation"},{"key":"7_CR19","unstructured":"A.W. Roscoe, Model-checking CSP, in A Classical Mind: Essays in Honour of C.A.R. Hoare, A.W. Roscoe (ed.) Prentice-Hall 1994."},{"key":"7_CR20","unstructured":"A.W. Roscoe, CSP and determinism in security modelling to ap pear in the proceedings of 1995 IEEE Symposium on Security and Privacy."},{"key":"7_CR21","unstructured":"A.W. Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, to appear in the proceedings of CSFW8 (1995), IEEE Press."},{"key":"7_CR22","unstructured":"A.W. Roscoe, J.C.P. Woodcock and L. Wulf, Non-interference t hrough determinism, Proc. ESORICS 94, Springer LNCS 875, pp 33\u201353."},{"key":"7_CR23","volume-title":"Proc. Computer-Aided Verification '90","author":"V. Roy","year":"1991","unstructured":"V. Roy and R. de Simone, Auto\/Autograph, In Proc. Computer-Aided Verification '90, American Mathematical Society, Providence, 1991."},{"key":"7_CR24","unstructured":"J.B. Scattergood, A basis for CSP tools, To appear as Oxford University Computing Laboratory technical monograph, 1993."},{"key":"7_CR25","unstructured":"A. Valmari and M. Tienari An improved failures equivalence for finitestate systems with a reduction algorithm, in Protocol Specification, Testing and Verification XI, North-Holland 1991."}],"container-title":["Tools and Algorithms for the Construction and Analysis of Systems","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60630-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:00:58Z","timestamp":1640944858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60630-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540606307","9783540485094"],"references-count":25,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-60630-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1995]]}}}