{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T03:16:32Z","timestamp":1773717392270,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642381638","type":"print"},{"value":"9783642381645","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38164-5_18","type":"book-chapter","created":{"date-parts":[[2013,4,30]],"date-time":"2013-04-30T17:59:00Z","timestamp":1367344740000},"page":"264-276","source":"Crossref","is-referenced-by-count":1,"title":["Techniques for Formal Modelling and Analysis of Quantum Systems"],"prefix":"10.1007","author":[{"given":"Simon J.","family":"Gay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajagopal","family":"Nagarajan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"052328","DOI":"10.1103\/PhysRevA.70.052328","volume":"70","author":"S. Aaronson","year":"2004","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A\u00a070, 052328 (2004)","journal-title":"Physical Review A"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: Broy, M. (ed.) Deductive Program Design: Proceedings of the 1994 Marktoberdorf International Summer School. NATO ASI Series F: Computer and Systems Sciences. Springer (1995)","DOI":"10.1007\/978-3-642-61455-2_10"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Interaction Categories (Extended Abstract). In: Burn, G.L., Gay, S.J., Ryan, M.D. (eds.) Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods. Workshops in Computer Science, pp. 57\u201370. Springer (1993)","DOI":"10.1007\/978-1-4471-3503-6_5"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 415\u2013425. IEEE Computer Society (2004); Also arXiv:quant-ph\/0402130","DOI":"10.1109\/LICS.2004.1319636"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-36742-7_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Ardeshir-Larijani","year":"2013","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 478\u2013492. Springer, Heidelberg (2013)"},{"issue":"2","key":"18_CR6","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1142\/S0219749908003530","volume":"6","author":"P. Baltazar","year":"2008","unstructured":"Baltazar, P., Chadha, R., Mateus, P.: Quantum computation tree logic \u2013 model checking and complete calculus. International Journal of Quantum Information\u00a06(2), 219\u2013236 (2008)","journal-title":"International Journal of Quantum Information"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Baltazar, P., Chadha, R., Mateus, P., Sernadas, A.: Towards model-checking quantum security protocols. In: First International Conference on Quantum, Nano, and Micro Technologies, ICQNM. IEEE Computer Society (2007)","DOI":"10.1109\/ICQNM.2007.21"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"1895","DOI":"10.1103\/PhysRevLett.70.1895","volume":"70","author":"C.H. Bennett","year":"1993","unstructured":"Bennett, C.H., Brassard, G., Cr\u00e9peau, C., Jozsa, R., Peres, A., Wootters, W.K.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters\u00a070, 1895\u20131899 (1993)","journal-title":"Physical Review Letters"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: 42nd IEEE Symposium on Foundations of Computer Science, FOCS, pp. 136\u2013145. IEEE Computer Society (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"issue":"1","key":"18_CR10","first-page":"73","volume":"8","author":"T. Davidson","year":"2012","unstructured":"Davidson, T., Gay, S.J., Mlna\u0159\u00edk, H., Nagarajan, R., Papanikolaou, N.: Model checking for Communicating Quantum Processes. International Journal of Unconventional Computing\u00a08(1), 73\u201398 (2012)","journal-title":"International Journal of Unconventional Computing"},{"key":"18_CR11","unstructured":"Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. PhD thesis, University of Warwick (2011)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic, vol. B: Formal Models and Semantics, pp. 995\u20131072. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages, POPL. ACM (2011)","DOI":"10.1145\/1926385.1926446"},{"key":"18_CR14","unstructured":"Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph] (2012)"},{"issue":"6-7","key":"18_CR15","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/BF02650179","volume":"21","author":"R.P. Feynman","year":"1982","unstructured":"Feynman, R.P.: Simulating physics with computers. International Journal of Theoretical Physics\u00a021(6-7), 467\u2013488 (1982)","journal-title":"International Journal of Theoretical Physics"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Mackie, I.C. (eds.): Semantic Techniques in Quantum Computation. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139193313"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: 32nd ACM Symposium on Principles of Programming Languages, POPL, pp. 145\u2013157 (2005); Also arXiv:quant-ph\/0409052","DOI":"10.1145\/1040305.1040318"},{"key":"18_CR18","unstructured":"Gay, S.J.: Stabilizer states as a basis for density matrices. arXiv:1112.2156 (2011)"},{"issue":"3","key":"18_CR19","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0960129506005263","volume":"16","author":"S.J. Gay","year":"2006","unstructured":"Gay, S.J., Nagarajan, R.: Types and typechecking for Communicating Quantum Processes. Mathematical Structures in Computer Science\u00a016(3), 375\u2013406 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-70545-1_51","volume-title":"Computer Aided Verification","author":"S.J. Gay","year":"2008","unstructured":"Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: A model checker for quantum systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 543\u2013547. Springer, Heidelberg (2008)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Papanikolaou, N., Nagarajan, R.: Specification and verification of quantum protocols. In: Semantic Techniques in Quantum Computation. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139193313.012"},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"1862","DOI":"10.1103\/PhysRevA.54.1862","volume":"54","author":"D. Gottesman","year":"1996","unstructured":"Gottesman, D.: Class of quantum error-correcting codes saturating the quantum Hamming bound. Physical Review A\u00a054, 1862 (1996)","journal-title":"Physical Review A"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Grover, L.: A fast quantum mechanical algorithm for database search. In: 28th ACM Symposium on the Theory of Computation, STOC, pp. 212\u2013219. ACM Press (1996)","DOI":"10.1145\/237814.237866"},{"issue":"3","key":"18_CR24","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1017\/S096012950600524X","volume":"16","author":"M. Lalire","year":"2006","unstructured":"Lalire, M.: Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science\u00a016(3), 407\u2013428 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"5","key":"18_CR25","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1016\/j.ic.2006.02.001","volume":"204","author":"P. Mateus","year":"2006","unstructured":"Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation\u00a0204(5), 771\u2013794 (2006)","journal-title":"Information and Computation"},{"issue":"3","key":"18_CR26","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/382780.382781","volume":"48","author":"D. Mayers","year":"2001","unstructured":"Mayers, D.: Unconditional Security in Quantum Cryptography. Journal of the ACM\u00a048(3), 351\u2013406 (2001)","journal-title":"Journal of the ACM"},{"key":"18_CR27","unstructured":"Nagarajan, R., Gay, S.J.: Formal verification of quantum protocols. arXiv:quant-ph\/0203086 (March 2002)"},{"key":"18_CR28","unstructured":"Papanikolaou, N.K.: Model Checking Quantum Protocols. PhD thesis, University of Warwick (2009)"},{"issue":"4","key":"18_CR29","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129504004256","volume":"14","author":"P. Selinger","year":"2004","unstructured":"Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science\u00a014(4), 527\u2013586 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR30","unstructured":"Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: 35th IEEE Symposium on Foundations of Computer Science, FOCS (1994)"},{"issue":"3","key":"18_CR31","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.entcs.2008.11.023","volume":"220","author":"N. Tr\u010dka","year":"2008","unstructured":"Tr\u010dka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. Electronic Notes in Theoretical Computer Science\u00a0220(3), 129\u2013143 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"3","key":"18_CR32","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1507244.1507249","volume":"10","author":"M. Ying","year":"2009","unstructured":"Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Transactions on Computational Logic\u00a010(3), 19 (2009)","journal-title":"ACM Transactions on Computational Logic"}],"container-title":["Lecture Notes in Computer Science","Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38164-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,1]],"date-time":"2023-07-01T10:48:20Z","timestamp":1688208500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38164-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642381638","9783642381645"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38164-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}