{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T16:26:51Z","timestamp":1776011211005,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains. To specify qualitative temporal properties, a subspace-based quantum temporal logic is used, which is built on Birkhoff-von Neumann atomic propositions. These propositions determine whether a quantum state is within a subspace of the entire state space. In this paper, we propose the measurement-based linear-time temporal logic MLTL to check quantitative properties. MLTL builds upon classical linear-time temporal logic (LTL) but introduces quantum atomic propositions that reason about the probability distribution after measuring a quantum state. To facilitate verification, we extend the symbolic dynamics-based techniques for stochastic matrices described by Agrawal et al. (JACM 2015) to handle more general quantum linear operators (super-operators) through eigenvalue analysis. This extension enables the development of an efficient algorithm for approximately model checking a quantum Markov chain against an MLTL formula. To demonstrate the utility of our model-checking algorithm, we use it to simultaneously verify linear-time properties of both quantum and classical random walks. Through this verification, we confirm the previously established advantages discovered by Ambainis et al. (STOC 2001) of quantum walks over classical random walks and discover new phenomena unique to quantum walks.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_24","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"533-554","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Measurement-Based Verification of\u00a0Quantum Markov Chains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3490-0029","authenticated-orcid":false,"given":"Ji","family":"Guan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3097-3896","authenticated-orcid":false,"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-9323","authenticated-orcid":false,"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"24_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT press (2008)"},{"issue":"1","key":"24_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1093\/nsr\/nwy106","volume":"6","author":"M Ying","year":"2019","unstructured":"Ying, M., Feng, Y.: Model-checking quantum systems. Nat. Sci. Rev. 6(1), 28\u201331 (2019)","journal-title":"Nat. Sci. Rev."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Ying, M., Feng, Y.: Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press (2021)","DOI":"10.1017\/9781108613323"},{"issue":"9","key":"24_CR4","doi-asserted-by":"publisher","first-page":"2048","DOI":"10.1109\/TAC.2008.929399","volume":"53","author":"F Ticozzi","year":"2008","unstructured":"Ticozzi, F., Viola, L.: Quantum Markovian subsystems: invariance, attractivity, and control. IEEE Trans. Autom. Control 53(9), 2048\u20132063 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"key":"24_CR5","unstructured":"Guan, J., Feng, Y., Ying, M.: The structure of decoherence-free subsystems. arXiv preprint arXiv:1802.04904 (2018)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann (2016)","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"24_CR7","unstructured":"Wolf, M.M.: Quantum channels & operations: guided tour. Lecture notes available at. https:\/\/mediatum.ub.tum.de\/doc\/1701036\/document.pdf (2012)"},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1142\/S0219749903000383","volume":"1","author":"A Ambainis","year":"2003","unstructured":"Ambainis, A.: Quantum walks and their algorithmic applications. Inter. J. Quantum Inform. 1, 507\u2013518 (2003)","journal-title":"Inter. J. Quantum Inform."},{"issue":"4","key":"24_CR9","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1080\/00107151031000110776","volume":"44","author":"J Kempe","year":"2003","unstructured":"Kempe, J.: Quantum random walks: an introductory overview. Contemp. Phys. 44(4), 307\u2013327 (2003)","journal-title":"Contemp. Phys."},{"issue":"4","key":"24_CR10","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1007\/s10955-012-0491-0","volume":"147","author":"S Attal","year":"2012","unstructured":"Attal, S., Petruccione, F., Sabot, C., Sinayskiy, I.: Open quantum random walks. J. Stat. Phys. 147(4), 832\u2013852 (2012)","journal-title":"J. Stat. Phys."},{"issue":"7","key":"24_CR11","doi-asserted-by":"publisher","first-page":"1181","DOI":"10.1016\/j.jcss.2013.04.002","volume":"79","author":"Y Feng","year":"2013","unstructured":"Feng, Y., Nengkun, Yu., Ying, M.: Model checking quantum Markov chains. J. Comput. Syst. Sci. 79(7), 1181\u20131198 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"24_CR12","doi-asserted-by":"publisher","first-page":"823","DOI":"10.2307\/1968621","volume":"37","author":"G Birkhoff","year":"1936","unstructured":"Birkhoff, G., von Neumann, J.: The logic of quantum mechanics. Annals Math. 37, 823\u2013843 (1936)","journal-title":"Annals Math."},{"issue":"1\u20132","key":"24_CR13","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0304-3975(98)00191-1","volume":"237","author":"C Moore","year":"2000","unstructured":"Moore, C., Crutchfield, J.P.: Quantum automata and quantum grammars. Theoretical Comput. Sci. 237(1\u20132), 275\u2013306 (2000)","journal-title":"Theoretical Comput. Sci."},{"issue":"3","key":"24_CR14","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2629680","volume":"15","author":"M Ying","year":"2014","unstructured":"Ying, M., Li, Y., Nengkun, Yu., Feng, Y.: Model-checking linear-time properties of quantum systems. ACM Trans. Comput. Logic (TOCL) 15(3), 22 (2014)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-662-44584-6_33","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"Y Li","year":"2014","unstructured":"Li, Y., Ying, M.: (Un)decidable problems about reachability of quantum systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 482\u2013496. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_33"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In : 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"24_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2629417","volume":"62","author":"M Agrawal","year":"2015","unstructured":"Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of Markov chains. J. ACM (JACM) 62(1), 2 (2015)","journal-title":"J. ACM (JACM)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Ambainis, A., Bach, E., Nayak, A., Vishwanath, A., Watrous, J.: One-dimensional quantum walks. In: Proceedings of the Thirty-third Annual ACM Symposium on Theory of computing (STOC), pp 37\u201349. ACM (2001)","DOI":"10.1145\/380752.380757"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-319-19249-9_17","volume-title":"FM 2015: Formal Methods","author":"Y Feng","year":"2015","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Zhang, L.: QPMC: a model checker for quantum programs and protocols. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 265\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_17"},{"key":"24_CR20","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Ying, S.: Model checking omega-regular properties for quantum Markov chains. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 85. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-40184-8_24","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"S Ying","year":"2013","unstructured":"Ying, S., Feng, Y., Yu, N., Ying, M.: Reachability probabilities of quantum Markov chains. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 334\u2013348. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_24"},{"issue":"5","key":"24_CR22","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1007\/s11128-012-0432-5","volume":"11","author":"SE Venegas-Andraca","year":"2012","unstructured":"Venegas-Andraca, S.E.: Quantum walks: a comprehensive review. Quantum Inf. Process. 11(5), 1015\u20131106 (2012)","journal-title":"Quantum Inf. Process."},{"key":"24_CR23","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2010)"},{"issue":"3","key":"24_CR24","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0024-3795(75)90075-0","volume":"10","author":"M-D Choi","year":"1975","unstructured":"Choi, M.-D.: Completely positive linear maps on complex matrices. Linear Algebra Appl. 10(3), 285\u2013290 (1975)","journal-title":"Linear Algebra Appl."},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Guan, J., Feng, Y., Turrini, A., Ying, M.: Measurement-based verification of quantum markov chains. arXiv preprint arXiv:2405.05825 (2024)","DOI":"10.1007\/978-3-031-65633-0_24"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-99527-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Guan","year":"2022","unstructured":"Guan, J., Yu, N.: A probabilistic logic for verifying continuous-time Markov chains. In: TACAS 2022. LNCS, vol. 13244, pp. 3\u201321. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_1"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-48778-6_16","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"MY Vardi","year":"1999","unstructured":"Vardi, M.Y.: Probabilistic linear-time model checking: an overview of the automata-theoretic approach. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 265\u2013276. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_16"},{"issue":"02","key":"24_CR28","doi-asserted-by":"publisher","first-page":"1250001","DOI":"10.1142\/S0129055X12500018","volume":"24","author":"B Baumgartner","year":"2012","unstructured":"Baumgartner, B., Narnhofer, H.: The structures of state space concerning quantum dynamical semigroups. Rev. Math. Phys. 24(02), 1250001 (2012)","journal-title":"Rev. Math. Phys."},{"key":"24_CR29","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.jcss.2018.01.005","volume":"95","author":"J Guan","year":"2018","unstructured":"Guan, J., Feng, Y., Ying, M.: Decomposition of quantum Markov chains and its applications. J. Comput. Syst. Sci. 95, 55\u201368 (2018)","journal-title":"J. Comput. Syst. Sci."},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Gallager, R.G.: Discrete Stochastic Processes, vol. 321. Springer Science & Business Media, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4615-2329-1","DOI":"10.1007\/978-1-4615-2329-1"},{"key":"24_CR31","unstructured":"Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers. Oxford university press (1979)"},{"key":"24_CR32","doi-asserted-by":"publisher","first-page":"1679","DOI":"10.1016\/j.scico.2013.03.016","volume":"78","author":"M Ying","year":"2013","unstructured":"Ying, M., Nengkun, Yu., Feng, Y., Duan, R.: Verification of quantum programs. Sci. Comput. Program. 78, 1679\u20131700 (2013)","journal-title":"Sci. Comput. Program."},{"key":"24_CR33","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Proceedings of the 34th International Conference on Computer Aided Verification (CAV 2022), vol. 13372 LNCS, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:15:21Z","timestamp":1732479321000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}