{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T11:30:46Z","timestamp":1776684646397,"version":"3.51.2"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:00:00Z","timestamp":1604448000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:00:00Z","timestamp":1604448000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["11871221"],"award-info":[{"award-number":["11871221"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Key R&D Program of China","award":["2018YFA0306704"],"award-info":[{"award-number":["2018YFA0306704"]}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","award":["DP180100691"],"award-info":[{"award-number":["DP180100691"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012245","name":"Science and Technology Planning Project of Guangdong Province","doi-asserted-by":"publisher","award":["2019A1515011689"],"award-info":[{"award-number":["2019A1515011689"]}],"id":[{"id":"10.13039\/501100012245","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s00236-020-00392-5","type":"journal-article","created":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T03:02:46Z","timestamp":1604458966000},"page":"653-674","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Measuring the constrained reachability in quantum Markov chains"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9906-5677","authenticated-orcid":false,"given":"Ming","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cheng-Chao","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,4]]},"reference":[{"key":"392_CR1","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Proceedings of the 8th CAV, Volume 1102 of LNCS, pp. 269\u2013276. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"key":"392_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"392_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, 2nd edn. Springer, Berlin (2006)","edition":"2"},{"key":"392_CR4","volume-title":"Introductory Combinatorics","author":"RA Brualdi","year":"2009","unstructured":"Brualdi, R.A.: Introductory Combinatorics, 5th edn. Pearson, New York (2009)","edition":"5"},{"key":"392_CR5","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"392_CR6","doi-asserted-by":"publisher","DOI":"10.1090\/surv\/015","volume-title":"Vector Measures","author":"J Diestel","year":"1977","unstructured":"Diestel, J., Uhl, J.J.: Vector Measures. American Mathematical Society, New York (1977)"},{"key":"392_CR7","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Ying, S.: Model checking $$\\omega $$-regular properties for quantum Markov chains. In: Proceedings of the 28th CONCUR, Volume\u00a085 of LIPIcs, pp. 35:1\u201335:16 (2017)"},{"key":"392_CR8","doi-asserted-by":"crossref","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Zhang, L.: QPMC: a model checker for quantum programs and protocols. In: Proceedings of the 20th FM, Volume 9109 of LNCS, pp. 265\u2013272. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-19249-9_17"},{"issue":"7","key":"392_CR9","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., Yu, N., Ying, M.: Model checking quantum Markov chains. J. Comput. Syst. Sci. 79(7), 1181\u20131198 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"392_CR10","doi-asserted-by":"crossref","unstructured":"Feng, Y., Yu, N., Ying, M.: Reachability analysis of recursive quantum Markov chains. In: Proceedings of the 38th MFCS, Volume 8087 of LNCS, pp. 385\u2013396. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40313-2_35"},{"key":"392_CR11","unstructured":"Gay, S.J., Nagarajan, R., Papanikolaou, N.: Probabilistic model-checking of quantum protocols. In: Proceedings of the 2nd International Workshop on Developments in Computational Models (2006). arXiv:quant-ph\/0504007"},{"key":"392_CR12","unstructured":"Hansson, H., Jonsson, B.: A framework for reasoning about time and reliability. In: Proceedings of the 10th RTSS, pp. 102\u2013111. IEEE Computer Society, New York (1989)"},{"key":"392_CR13","volume-title":"States, Effects and Operations: Fundamental Notions of Quantum Theory","year":"1983","unstructured":"Kraus, K., B\u00f6hm, A., Dollard, J.D., Wootters, W.H. (eds.): States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin (1983)"},{"key":"392_CR14","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd CAV, Volume 6806 of LNCS, pp. 585\u2013591. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"392_CR15","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.ic.2015.07.001","volume":"244","author":"L Li","year":"2015","unstructured":"Li, L., Feng, Y.: Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Inf. Comput. 244, 229\u2013244 (2015)","journal-title":"Inf. Comput."},{"key":"392_CR16","volume-title":"Quantum Computation and Quantum Information","author":"MA Nielsen","year":"2000","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, London (2000)"},{"key":"392_CR17","unstructured":"Papanikolaou, N.K.: Model checking quantum protocols. Ph.D. Thesis, University of Warwick (2008)"},{"key":"392_CR18","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th FOCS, pp. 46\u201357. IEEE Computer Society, New York (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"392_CR19","volume-title":"Orbital Mechanics","author":"JE Prussing","year":"2012","unstructured":"Prussing, J.E., Conway, B.A.: Orbital Mechanics, 2nd edn. Oxford University Press, London (2012)","edition":"2"},{"issue":"3\u20134","key":"392_CR20","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1006\/jsco.1996.0142","volume":"24","author":"A Steel","year":"1997","unstructured":"Steel, A.: A new algorithm for the computation of canonical forms of matrices over fields. J. Symb. Comput. 24(3\u20134), 409\u2013432 (1997)","journal-title":"J. Symb. Comput."},{"key":"392_CR21","doi-asserted-by":"publisher","first-page":"113026","DOI":"10.1088\/1367-2630\/12\/11\/113026","volume":"12","author":"F Xu","year":"2010","unstructured":"Xu, F., Qi, B., Lo, H.-K.: Experimental demonstration of phase-remapping attack in a practical quantum key distribution system. New J. Phys. 12, 113026 (2010)","journal-title":"New J. Phys."},{"key":"392_CR22","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.jsc.2012.05.005","volume":"50","author":"M Xu","year":"2013","unstructured":"Xu, M., Li, Z.-B.: Symbolic termination analysis of solvable loops. J. Symb. Comput. 50, 28\u201349 (2013)","journal-title":"J. Symb. Comput."},{"key":"392_CR23","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.tcs.2015.07.047","volume":"611","author":"M Xu","year":"2016","unstructured":"Xu, M., Zhang, L., Jansen, D.N., Zhu, H., Yang, Z.: Multiphase until formulas over Markov reward models: an algebraic approach. Theoret. Comput. Sci. 611, 116\u2013135 (2016)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"392_CR24","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2629680","volume":"15","author":"M Ying","year":"2014","unstructured":"Ying, M., Li, Y., Yu, N., Feng, Y.: Model-checking linear-time properties of quantum systems. ACM Trans. Comput. Log. 15(3), 22:1\u201322:31 (2014)","journal-title":"ACM Trans. Comput. Log."},{"issue":"9","key":"392_CR25","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., Yu, N., Feng, Y., Duan, R.: Verification of quantum programs. Sci. Comput. Program. 78(9), 1679\u20131700 (2013)","journal-title":"Sci. Comput. Program."},{"key":"392_CR26","doi-asserted-by":"crossref","unstructured":"Ying, S., Feng, Y., Yu, N., Ying, M.: Reachability probabilities of quantum Markov chains. In: Proceedings of the 24th CONCUR, Volume 8052 of LNCS, pp. 334\u2013348. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40184-8_24"},{"key":"392_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-based CSL model checking. In: Proceedings of the 38th ICALP, Part II, Volume 6756 of LNCS, pp. 271\u2013282. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22012-8_21"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00392-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00392-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00392-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T03:42:15Z","timestamp":1634787735000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00392-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,4]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["392"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00392-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,4]]},"assertion":[{"value":"22 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 November 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}