{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T14:25:06Z","timestamp":1725978306079},"publisher-location":"Cham","reference-count":89,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_32","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"1149-1195","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Process Algebra and Model Checking"],"prefix":"10.1007","author":[{"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"5","key":"32_CR1","first-page":"1157","volume":"104","author":"M. Abdel-Rohman","year":"1978","unstructured":"Abdel-Rohman, M., Leipholz, H.H.E.: Structural control by pole assignment method. Eng. Mech. 104(5), 1157\u20131175 (1978)","journal-title":"Eng. Mech."},{"issue":"3","key":"32_CR2","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1002\/eqe.4290220304","volume":"22","author":"A.K. Agrawal","year":"1993","unstructured":"Agrawal, A.K., Fujino, Y., Bhartia, B.K.: Instability due to time delay and its compensation in active control of structures. Earthq. Eng. Struct. Dyn. 22(3), 211\u2013224 (1993)","journal-title":"Earthq. Eng. Struct. Dyn."},{"key":"32_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/978-3-642-31424-7_52","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Armstrong","year":"2012","unstructured":"Armstrong, P., Goldsmith, M.H., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Madhusudan, P., Seshia, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a0699\u2013704. Springer, Heidelberg (2012)"},{"key":"32_CR4","first-page":"13","volume-title":"HOWARD-60. A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday","author":"P. Armstrong","year":"2014","unstructured":"Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking timed CSP. In: Voronkov, A., Korovina, M. (eds.) HOWARD-60. A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday, pp.\u00a013\u201333. EasyChair, Manchester (2014)"},{"issue":"2","key":"32_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/BF01898401","volume":"3","author":"J.C.M. Baeten","year":"1991","unstructured":"Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Form. Asp. Comput. 3(2), 142\u2013188 (1991)","journal-title":"Form. Asp. Comput."},{"issue":"2","key":"32_CR6","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.1995.1135","volume":"121","author":"J.C.M. Baeten","year":"1995","unstructured":"Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput. 121(2), 234\u2013255 (1995)","journal-title":"Inf. Comput."},{"key":"32_CR7","series-title":"Cambridge Tracts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624193","volume-title":"Process Algebra","author":"J.C.M. Baeten","year":"1990","unstructured":"Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Computer Science, vol.\u00a018. Cambridge University Press, Cambridge (1990)"},{"issue":"3","key":"32_CR8","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1243987.1243990","volume":"16","author":"Samik Basu","year":"2007","unstructured":"Basu, S., Smolka, S.A.: Model checking the Java metalocking algorithm. ACM Trans. Softw. Eng. Methodol. 16(3) (2007)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"J.A. Bergstra","year":"1985","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77\u2013121 (1985)","journal-title":"Theor. Comput. Sci."},{"volume-title":"Handbook of Process Algebra","year":"2001","key":"32_CR10","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)"},{"key":"32_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a0354\u2013359. Springer, Heidelberg (2010)"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"key":"32_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-15670-4_14","volume-title":"Proceedings of the Pittsburgh Seminar on Concurrency","author":"S.D. Brookes","year":"1985","unstructured":"Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) Proceedings of the Pittsburgh Seminar on Concurrency. LNCS, vol.\u00a0197, pp.\u00a0281\u2013305. Springer, Heidelberg (1985)"},{"key":"32_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of the Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Proceedings of the Workshop on Logic of Programs, Yorktown Heights. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"key":"32_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/BFb0023750","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Cleaveland","year":"1991","unstructured":"Cleaveland, R.: On automatically explaining bisimulation inequivalence. In: Clarke, E.M., Kurshan, R.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0531, pp.\u00a0364\u2013372. Springer, Heidelberg (1991)"},{"key":"32_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/3-540-52148-8_2","volume-title":"Automatic Verification Methods for Finite State Systems","author":"R. Cleaveland","year":"1989","unstructured":"Cleaveland, R., Hennessy, M.C.B.: Testing equivalence as a bisimulation equivalence. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp.\u00a011\u201323. Springer, Heidelberg (1989)"},{"issue":"1","key":"32_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Hennessy, M.C.B.: Testing equivalence as a bisimulation equivalence. Form. Asp. Comput. 5(1), 1\u201320 (1993)","journal-title":"Form. Asp. Comput."},{"key":"32_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-61474-5_88","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Cleaveland","year":"1996","unstructured":"Cleaveland, R., Lewis, P.M., Smolka, S.A., Sokolsky, O.: The Concurrency Factory: a development environment for concurrent systems. In: Alur, R., Henzinger, T.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01102, pp.\u00a0398\u2013401. Springer, Heidelberg (1996)"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.U.: The Concurrency Workbench: a\u00a0semantics-based tool for the verification of finite-state systems. Tech. Rep. ECS-LFCS-89-83, Department of Computer Science, University of Edinburgh (1989)","DOI":"10.1007\/3-540-52148-8_3"},{"key":"32_CR20","volume-title":"Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification","author":"R. Cleaveland","year":"1989","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.U.: A semantics-based tool for the verification of finite-state systems. In: Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification. North-Holland, Amsterdam (1989)"},{"issue":"1","key":"32_CR21","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.U.: The Concurrency Workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"32_CR22","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0167-6423(01)00033-8","volume":"42","author":"R. Cleaveland","year":"2002","unstructured":"Cleaveland, R., Sims, S.: Generic tools for verifying concurrent systems. Sci. Comput. Program. 42(1), 39\u201347 (2002)","journal-title":"Sci. Comput. Program."},{"key":"32_CR23","volume-title":"Distributed Systems, Concepts and Design","author":"G. Colouris","year":"1994","unstructured":"Colouris, G., Dollimore, J., Kindberg, T.: Distributed Systems, Concepts and Design. Addison-Wesley, Reading (1994)"},{"key":"32_CR24","unstructured":"Creese, S.J., Roscoe, A.W.: TTP: a case study in combining induction and data independence. Tech. Rep. PRG-TR-1-99, Oxford University Computing Laboratory (1999)"},{"key":"32_CR25","first-page":"437","volume-title":"Proceedings of FORTE\/PSTV\u201999","author":"S.J. Creese","year":"1999","unstructured":"Creese, S.J., Roscoe, A.W.: Verifying an infinite family of inductions simultaneously using data independence and FDR. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Proceedings of FORTE\/PSTV\u201999, pp.\u00a0437\u2013452. Springer, Heidelberg (1999)"},{"key":"32_CR26","volume-title":"Proceedings of PDPTA 2000. CSREA","author":"S.J. Creese","year":"2000","unstructured":"Creese, S.J., Roscoe, A.W.: Data independent induction over stuctured networks. In: Arabnia, H.R. (ed.) Proceedings of PDPTA 2000. CSREA (2000)"},{"key":"32_CR27","volume-title":"Handbook of Model Checking","author":"D. Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"32_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BFb0000471","volume-title":"Proceedings of the Sixth Internationaal Conference on Algebraic Methodology and Software Technology (AMAST)","author":"X. Du","year":"1997","unstructured":"Du, X., McDonnell, K.T., Nanos, E., Ramakrishna, Y.S., Smolka, S.A.: Software design, specification, and verification: lessons learned from the Rether Case Study. In: Johnson, M. (ed.) Proceedings of the Sixth Internationaal Conference on Algebraic Methodology and Software Technology (AMAST). LNCS, vol.\u00a01349, pp.\u00a0185\u2013198. Springer, Heidelberg (1997)"},{"issue":"1\u20132","key":"32_CR29","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0167-6423(96)00031-7","volume":"29","author":"W.M. Elseaidy","year":"1997","unstructured":"Elseaidy, W.M., Cleaveland, R., Baugh, J.W. Jr.: Modeling and verifying active structural control systems. Sci. Comput. Program. 29(1\u20132), 99\u2013122 (1997)","journal-title":"Sci. Comput. Program."},{"key":"32_CR30","first-page":"267","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0267\u2013278. IEEE, Piscataway (1986)"},{"issue":"1","key":"32_CR31","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/TC.1982.1675885","volume":"31","author":"H. Garcia-Molina","year":"1982","unstructured":"Garcia-Molina, H.: Elections in a distributed computing system. IEEE Trans. Comput. 31(1), 48\u201359 (1982)","journal-title":"IEEE Trans. Comput."},{"key":"32_CR32","series-title":"LNCS","first-page":"187","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T. Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a modern refinement checker for CSP. In: Abraham, E., Mavelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0187\u2013201 (2014)"},{"key":"32_CR33","volume-title":"Proceedings of Communicating Process Architectures (CPA). Open Channel Publishing","author":"T. Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In: Welch, P.H., et al. (eds.) Proceedings of Communicating Process Architectures (CPA). Open Channel Publishing (2014)"},{"issue":"3","key":"32_CR34","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J.V. Glabbeek","year":"1996","unstructured":"Glabbeek, R.J.V., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"32_CR35","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"J.F. Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"32_CR36","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/REAL.1990.128759","volume-title":"Proceedings 11th Real-Time Systems Symposium (RTSS)","author":"H. Hansson","year":"1990","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings 11th Real-Time Systems Symposium (RTSS), pp.\u00a0278\u2013287. IEEE, Piscataway (1990)"},{"issue":"1","key":"32_CR37","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M.C.B. Hennessy","year":"1985","unstructured":"Hennessy, M.C.B., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"32_CR38","first-page":"453","volume-title":"36th Annual Symposium on Foundations of Computer Science","author":"M.R. Henzinger","year":"1995","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th Annual Symposium on Foundations of Computer Science, pp.\u00a0453\u2013462. IEEE, Piscataway (1995)"},{"key":"32_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0623, pp.\u00a0545\u2013558. Springer, Heidelberg (1992)"},{"issue":"8","key":"32_CR40","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"32_CR41","unstructured":"Hoare, C.A.R.: A model for communicating sequential processes, tech. monograph PRG-22, Programming Research Group, Oxford University Computing Laboratory (1981)"},{"key":"32_CR42","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, New York (1985)"},{"key":"32_CR43","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/298595.298864","volume-title":"Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP)","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J.: Designing executable abstractions. In: Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP), pp.\u00a0103\u2013108. ACM, New York (1998)"},{"issue":"6","key":"32_CR44","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2005.04.008","volume":"128","author":"P.J. Hopcroft","year":"2005","unstructured":"Hopcroft, P.J., Broadfoot, G.: Combining the box structure development method and CSP for software development. Electron. Notes Theor. Comput. Sci. 128(6), 127\u2013144 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"32_CR45","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1016\/S0022-0000(76)80038-4","volume":"12","author":"H.B. Hunt","year":"1976","unstructured":"Hunt, H.B., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. Syst. Sci. 12(2), 222\u2013268 (1976)","journal-title":"J. Comput. Syst. Sci."},{"issue":"12","key":"32_CR46","doi-asserted-by":"publisher","first-page":"2435","DOI":"10.1016\/j.scico.2012.11.009","volume":"78","author":"Y.L. Hwong","year":"2013","unstructured":"Hwong, Y.L., Keiren, J.J.A., Kusters, V.J.J., Leemans, S., Willemse, T.A.C.: Formalising and analysing the control software of the Compact Muon Solenoid experiment at the Large Hadron Collider. Sci. Comput. Program. 78(12), 2435\u20132452 (2013)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"32_CR47","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"issue":"3","key":"32_CR48","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc$\\mu$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR49","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11423348_9","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"J. Lawrence","year":"2005","unstructured":"Lawrence, J.: Practical application of CSP and FDR in software design. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol.\u00a03525, pp.\u00a0151\u2013175. Springer, Heidelberg (2005)"},{"key":"32_CR50","unstructured":"Lazic, R.S.: A semantic study of data independence with applications to model checking. Ph.D. thesis, University of Oxford (1999)"},{"key":"32_CR51","volume-title":"Occam Programming Manual","author":"I. Limited","year":"1984","unstructured":"Limited, I.: Occam Programming Manual. Prentice Hall, New York (1984)"},{"key":"32_CR52","first-page":"190","volume-title":"Proceedings of the 22nd International IEEE Symposium on Software Reliability Engineering (ISSRE)","author":"Y. Liu","year":"2011","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: Proceedings of the 22nd International IEEE Symposium on Software Reliability Engineering (ISSRE), pp.\u00a0190\u2013199. IEEE, Piscataway (2011)"},{"issue":"2","key":"32_CR53","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(94)00171-E","volume":"138","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci. 138(2), 315\u2013352 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"32_CR54","series-title":"LNCS","first-page":"147","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01055, pp.\u00a0147\u2013166. Springer, Heidelberg (1996)"},{"key":"32_CR55","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/CSFW.1997.596779","volume-title":"Proceedings of the 10th Computer Security Foundations Workshop (CSFW)","author":"G. Lowe","year":"1997","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. In: Proceedings of the 10th Computer Security Foundations Workshop (CSFW), pp.\u00a018\u201330. IEEE, Piscataway (1997)"},{"key":"32_CR56","first-page":"358","volume-title":"Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS)","author":"S. Lu","year":"1999","unstructured":"Lu, S., Smolka, S.: Model checking the secure electronic transaction (SET) protocol. In: Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), pp.\u00a0358\u2013364. IEEE, Piscataway (1999)"},{"key":"32_CR57","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"227","volume-title":"Proceedings of the Workshop \u201cEssays on Algebraic Process Calculi\u201d (APC 25)","author":"B. Luttik","year":"2006","unstructured":"Luttik, B.: What is algebraic in process theory? In: Proceedings of the Workshop \u201cEssays on Algebraic Process Calculi\u201d (APC 25). Electronic Notes in Theoretical Computer Science, vol.\u00a0162, pp.\u00a0227\u2013231 (2006)"},{"key":"32_CR58","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"32_CR59","series-title":"International Series in Computer Science","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, New York (1989)"},{"issue":"1","key":"32_CR60","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.J.: A calculus of mobile processes. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"32_CR61","unstructured":"Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. thesis, University of Oxford (2000)"},{"key":"32_CR62","series-title":"LNCS","first-page":"389","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"J. Ouaknine","year":"2011","unstructured":"Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Static livelock analysis in CSP. In: Katoen, J.P., K\u00f6nig, B. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a06901, pp.\u00a0389\u2013403. Springer, Heidelberg (2011)"},{"issue":"6","key":"32_CR63","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"issue":"10","key":"32_CR64","doi-asserted-by":"publisher","first-page":"1178","DOI":"10.1016\/j.scico.2011.07.008","volume":"77","author":"H. Palikareva","year":"2012","unstructured":"Palikareva, H., Ouaknine, J., Roscoe, A.W.: SAT-solving in CSP trace refinement. Sci. Comput. Program. 77(10), 1178\u20131197 (2012)","journal-title":"Sci. Comput. Program."},{"key":"32_CR65","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11423348_19","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"J. Peleska","year":"2005","unstructured":"Peleska, J.: Applied formal methods\u2014from CSP to executable hybrid specifications. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol.\u00a03525, pp.\u00a0293\u2013320. Springer, Heidelberg (2005)"},{"key":"32_CR66","unstructured":"Ploeger, B.: Analysis of ACS using mCRL2. Tech. Rep. CS\u201309\u201311, Technische Universiteit Eindhoven (2009)"},{"key":"32_CR67","unstructured":"Plotkin, G.: A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University (1981)"},{"key":"32_CR68","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-63141-0_2","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Smolka, S.A.: Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01243, pp.\u00a05\u201324. Springer, Heidelberg (1997)"},{"key":"32_CR69","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/10722167_48","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C.R. Ramakrishnan","year":"2000","unstructured":"Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., et al.: XMC: a logic-programming-based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0576\u2013580. Springer, Heidelberg (2000)"},{"issue":"1\u20133","key":"32_CR70","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"G.M. Reed","year":"1988","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58(1\u20133), 249\u2013261 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"32_CR71","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/logcom\/3.2.131","volume":"3","author":"A.W. Roscoe","year":"1993","unstructured":"Roscoe, A.W.: Unbounded non-determinism in CSP. J. Log. Comput. 3(2), 131\u2013172 (1993)","journal-title":"J. Log. Comput."},{"key":"32_CR72","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, New York (1997)"},{"key":"32_CR73","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/11423348_2","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"A.W. Roscoe","year":"2005","unstructured":"Roscoe, A.W.: Seeing beyond divergence. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol.\u00a03525, pp.\u00a015\u201335. Springer, Heidelberg (2005)"},{"key":"32_CR74","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-1-84882-912-1_16","volume-title":"Reflections on the Work of C.A.R. Hoare","author":"A.W. Roscoe","year":"2010","unstructured":"Roscoe, A.W.: CSP is expressive enough for \u03c0$\\pi$. In: Jones, C.B., Roscoe, A.W., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp.\u00a0371\u2013404. Springer, Heidelberg (2010)"},{"key":"32_CR75","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"A.W. Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)"},{"key":"32_CR76","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-39698-4_20","volume-title":"Theories of Programming and Formal Methods","author":"A.W. Roscoe","year":"2013","unstructured":"Roscoe, A.W., Hopcroft, P.J.: Slow abstraction through priority. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol.\u00a08051, pp.\u00a0326\u2013345. Springer, Heidelberg (2013)"},{"issue":"1","key":"32_CR77","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-012-0251-6","volume":"25","author":"A.W. Roscoe","year":"2013","unstructured":"Roscoe, A.W., Huang, J.: Checking noninterference in timed CSP. Form. Asp. Comput. 25(1), 3\u201335 (2013)","journal-title":"Form. Asp. Comput."},{"key":"32_CR78","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/11901433_18","volume-title":"Proceedings of Formal Methods and Software Engineering (FMSE)","author":"A.W. Roscoe","year":"2006","unstructured":"Roscoe, A.W., Wu, Z.: Verifying statemate statecharts using CSP and FDR. In: Liu, Z., He, J. (eds.) Proceedings of Formal Methods and Software Engineering (FMSE). LNCS, vol.\u00a04260, pp.\u00a0324\u2013341. Springer, Heidelberg (2006)"},{"key":"32_CR79","volume-title":"The pi-Calculus: A Theory of Mobile Processes","author":"D. Sangiorgi","year":"2003","unstructured":"Sangiorgi, D., Walker, D.J.: The pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2003)"},{"key":"32_CR80","unstructured":"Scattergood, J.: The semantics and implementation of machine-readable CSP. Ph.D. thesis, University of Oxford (1998)"},{"key":"32_CR81","volume-title":"Concurrent and Real-Time Systems","author":"S.A. Schneider","year":"2000","unstructured":"Schneider, S.A.: Concurrent and Real-Time Systems. Wiley, New York (2000)"},{"key":"32_CR82","volume-title":"Active Structural Control","author":"T.T. Soong","year":"1990","unstructured":"Soong, T.T.: Active Structural Control. Longman, New York (1990)"},{"key":"32_CR83","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/BFb0035794","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP)","author":"B. Steffen","year":"1989","unstructured":"Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0372, pp.\u00a0723\u2013732. Springer, Heidelberg (1989)"},{"key":"32_CR84","first-page":"186","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"D.J. Walker","year":"1988","unstructured":"Walker, D.J.: Bisimulation and divergence in CCS. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0186\u2013192. IEEE, Piscataway (1988)"},{"key":"32_CR85","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/11423348_10","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"P.H. Welch","year":"2005","unstructured":"Welch, P.H., Barnes, F.R.M.: Communicating mobile processes. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol.\u00a03525, pp.\u00a0175\u2013210. Springer, Heidelberg (2005)"},{"issue":"9","key":"32_CR86","doi-asserted-by":"publisher","first-page":"1369","DOI":"10.1061\/(ASCE)0733-9399(1987)113:9(1369)","volume":"113","author":"J.N. Yang","year":"1987","unstructured":"Yang, J.N., Akbarpour, A., Ghaemmaghami, P.: New control algorithms for structural control. Eng. Mech. 113(9), 1369\u20131386 (1987)","journal-title":"Eng. Mech."},{"key":"32_CR87","first-page":"68","volume-title":"IEEE Second Int. Conf. on Algorithms and Architectures for Parallel Processing (ICAPP)","author":"J.T. Yantchev","year":"1996","unstructured":"Yantchev, J.T.: ARC\u2014a tool for efficient refinement and equivalence checking for CSP. In: IEEE Second Int. Conf. on Algorithms and Architectures for Parallel Processing (ICAPP), pp.\u00a068\u201375. IEEE, Piscataway (1996)"},{"key":"32_CR88","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-54233-7_136","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"W. Yi","year":"1991","unstructured":"Yi, W.: CCS + time = an interleaving model for real-time systems. In: Albert, J.L., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0510, pp.\u00a0217\u2013228. Springer, Heidelberg (1991)"},{"key":"32_CR89","unstructured":"Zakiuddin, M.I., Moffat, N., O\u2019Halloran, C.M., Ryan, P.Y.A.: Chasing events to certify a critical system. Tech. rep., UK Defence Evaluation and Research Agency (1998)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T21:59:13Z","timestamp":1661291953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_32","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}