{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T14:30:13Z","timestamp":1780065013271,"version":"3.54.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,7,8]],"date-time":"2014-07-08T00:00:00Z","timestamp":1404777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP110103473 and DP130102764"],"award-info":[{"award-number":["DP110103473 and DP130102764"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,7,8]]},"abstract":"<jats:p>We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and \u03c9--properties recognizable by reversible B\u00fcchi automata.<\/jats:p>","DOI":"10.1145\/2629680","type":"journal-article","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T13:03:31Z","timestamp":1409317411000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Model-Checking Linear-Time Properties of Quantum Systems"],"prefix":"10.1145","volume":"15","author":[{"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"University of Technology, Sydney, Australia, Tsinghua University and Academy of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yangjia","family":"Li","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Waterloo, Ontario, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[{"name":"University of Technology, Sydney, Australia and Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,8,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_1","volume-title":"Principles of Model Checking","author":"Baier C.","unstructured":"C. Baier and J.-P. Katoen . 2008. Principles of Model Checking . MIT Press , Cambridge, Massachusetts . C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, Massachusetts."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICQNM.2007.21"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749908003530"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of International Conference on Computers, Systems and Signal Processing. 175--179","author":"Bennett C. H.","unstructured":"C. H. Bennett and G. Brassard . 1984. Quantum cryptography: Public key distribution and coin tossing . In: Proceedings of International Conference on Computers, Systems and Signal Processing. 175--179 . C. H. Bennett and G. Brassard. 1984. Quantum cryptography: Public key distribution and coin tossing. In: Proceedings of International Conference on Computers, Systems and Signal Processing. 175--179."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"H.-P. Breuer and F. Petruccione. 2002. The Theory of Open Quantum Systems. Oxford University Press Oxford.  H.-P. Breuer and F. Petruccione. 2002. The Theory of Open Quantum Systems. Oxford University Press Oxford.","DOI":"10.1007\/3-540-44874-8_4"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1119\/1.1475328"},{"key":"e_1_2_1_9_1","volume-title":"In: B","author":"Bruns G.","year":"2000","unstructured":"G. Bruns and J. Harding . 2000 . Algebraic aspects of orthomodular lattices. In: B . Coecke, D. Moore and A. Wilce (eds.), Current Research in Operational Quantum Logic: Algebras, Categories, Languages, Kluwer , Dordrecht, 37--65. G. Bruns and J. Harding. 2000. Algebraic aspects of orthomodular lattices. In: B. Coecke, D. Moore and A. Wilce (eds.), Current Research in Operational Quantum Logic: Algebras, Categories, Languages, Kluwer, Dordrecht, 37--65."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1038\/nphys2275"},{"key":"e_1_2_1_12_1","first-page":"73","article-title":"Model checking for communicating quantum processes","volume":"8","author":"Davidson T.","year":"2012","unstructured":"T. Davidson , S. J. Gay , H. Mlnarik , R. Nagarajan , and N. Papanikolaou . 2012 . Model checking for communicating quantum processes . International Journal of Unconventional Computing 8 , 73 -- 98 . T. Davidson, S. J. Gay, H. Mlnarik, R. Nagarajan, and N. Papanikolaou. 2012. Model checking for communicating quantum processes. International Journal of Unconventional Computing 8, 73--98.","journal-title":"International Journal of Unconventional Computing"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.95.7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2003.1227"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.08.001"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926446"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2400676.2400680"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005263"},{"key":"e_1_2_1_20_1","unstructured":"S. J. Gay R. Nagarajan and N. Papanikolaou. 2005. Probabilistic model-checking of quantum protocols arXiv:quant-ph\/0504007.  S. J. Gay R. Nagarajan and N. Papanikolaou. 2005. Probabilistic model-checking of quantum protocols arXiv:quant-ph\/0504007."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_2_1_22_1","volume-title":"In: I","author":"Gay S. J.","year":"2010","unstructured":"S. J. Gay , R. Nagarajan , and N. Panaikolaou . 2010 . Specification and verification of quantum protocols. In: I . Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press , 414--472. S. J. Gay, R. Nagarajan, and N. Panaikolaou. 2010. Specification and verification of quantum protocols. In: I. Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 414--472."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11885191_3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.54.2759"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/977091.977108"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"B. Kraus. 2010. Local unitary equivalence of multipartite pure states. Physical Review Letters 104 art. no. 020504.  B. Kraus. 2010. Local unitary equivalence of multipartite pure states. Physical Review Letters 104 art. no. 020504.","DOI":"10.1103\/PhysRevLett.104.020504"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Physics 190","volume-title":"States, Effects, and Operations: Fundamental Notions of Quantum Theory","author":"Kraus K.","unstructured":"K. Kraus . 1983. States, Effects, and Operations: Fundamental Notions of Quantum Theory . Lecture Notes in Physics 190 , Springer . K. Kraus. 1983. States, Effects, and Operations: Fundamental Notions of Quantum Theory. Lecture Notes in Physics 190, Springer."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 38th Symposium on Foundation of Computer Science (FOCS\u201997)","author":"Kondacs A.","unstructured":"A. Kondacs and J. Watrous . 1997. On the power of quantum finite state automata . In: Proceedings of the 38th Symposium on Foundation of Computer Science (FOCS\u201997) . 66--75. A. Kondacs and J. Watrous. 1997. On the power of quantum finite state automata. In: Proceedings of the 38th Symposium on Foundation of Computer Science (FOCS\u201997). 66--75."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600524X"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_34_1","unstructured":"Y. J. Li N. K. Yu and M. S. Ying. Termination of nondeterministic quantum programs. Short presentation of LICS\u00d512 (For full paper see arXiv: 1201.0891).  Y. J. Li N. K. Yu and M. S. Ying. Termination of nondeterministic quantum programs. Short presentation of LICS\u00d512 (For full paper see arXiv: 1201.0891)."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.273.5278.1073"},{"key":"e_1_2_1_36_1","unstructured":"Z. Manna and A. Pnueli. 1995. The Temporal Logic of Reactive and Concurrent Systems: Safety Springer.   Z. Manna and A. Pnueli. 1995. The Temporal Logic of Reactive and Concurrent Systems: Safety Springer."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.02.001"},{"key":"e_1_2_1_38_1","unstructured":"R. Nagarajan and S. J. Gay. 2002. Formal verification of quantum protocols. arXiv: quant-ph\/0203086.  R. Nagarajan and S. J. Gay. 2002. Formal verification of quantum protocols. arXiv: quant-ph\/0203086."},{"key":"e_1_2_1_39_1","unstructured":"M. A. Nielsen and I. L. Chuang. 2000. Quantum Computation and Quantum Information Cambridge University Press.   M. A. Nielsen and I. L. Chuang. 2000. Quantum Computation and Quantum Information Cambridge University Press."},{"key":"e_1_2_1_41_1","series-title":"Lecture Notes in Computer Science 267","volume-title":"Proceedings of the 14th International Colloquium on Automata, Languages and Programming (ICALP\u201987)","author":"Pin J.-E.","unstructured":"J.-E. Pin . 1987. On the languages recognised by finite reversible automata . In: Proceedings of the 14th International Colloquium on Automata, Languages and Programming (ICALP\u201987) . Lecture Notes in Computer Science 267 , Springer , 237--249. J.-E. Pin. 1987. On the languages recognised by finite reversible automata. In: Proceedings of the 14th International Colloquium on Automata, Languages and Programming (ICALP\u201987). Lecture Notes in Computer Science 267, Springer, 237--249."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the First Latin American Theoretical Informatics Symposium (LATIN\u201992)","author":"Pin J.-E.","year":"2001","unstructured":"J.-E. Pin . 2001 . On reversible automata . In: Proceedings of the First Latin American Theoretical Informatics Symposium (LATIN\u201992) , Lecture Notes in Computer Science 583, Springer. 401--416. J.-E. Pin. 2001. On reversible automata. In: Proceedings of the First Latin American Theoretical Informatics Symposium (LATIN\u201992), Lecture Notes in Computer Science 583, Springer. 401--416."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"R. Raussendorf D. E. Browne and H. J. Briegel. 2003. Measurement-based quantum computation with cluster states. Physical Review A 68 art. No. 022312.  R. Raussendorf D. E. Browne and H. J. Briegel. 2003. Measurement-based quantum computation with cluster states. Physical Review A 68 art. No. 022312.","DOI":"10.1103\/PhysRevA.68.022312"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"G. M. Wang and M. S. Ying. 2008. Perfect many-to-one teleportation with stabilizer states. Physical Review A 77 art. No. 032324.  G. M. Wang and M. S. Ying. 2008. Perfect many-to-one teleportation with stabilizer states. Physical Review A 77 art. No. 032324.","DOI":"10.1103\/PhysRevA.77.032324"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"G. M. Wang and M. S. Ying. 2008. Deterministic distributed dense coding with stabilizer states. Physical Review A 77 art. No. 032306.  G. M. Wang and M. S. Ying. 2008. Deterministic distributed dense coding with stabilizer states. Physical Review A 77 art. No. 032306.","DOI":"10.1103\/PhysRevA.77.032306"},{"key":"e_1_2_1_47_1","volume-title":"Handbook of Quantum Logic and Quantum Structures","author":"Ying M. S.","unstructured":"M. S. Ying . 2007. Quantum logic and automata theory . In: D. Gabbay, D. Lehmann, and K. Engesser (eds.), Handbook of Quantum Logic and Quantum Structures , Elsevier , Amsterdam , 619--754. M. S. Ying. 2007. Quantum logic and automata theory. In: D. Gabbay, D. Lehmann, and K. Engesser (eds.), Handbook of Quantum Logic and Quantum Structures, Elsevier, Amsterdam, 619--754."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.13"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"key":"e_1_2_1_50_1","volume-title":"In: I","author":"Ying M. S.","year":"2010","unstructured":"M. S. Ying , R. Y. Duan , Y. Feng , and Z. F. Ji . 2010 . Predicate transformer semantics of quantum programs. In: I . Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press , 311--360. M. S. Ying, R. Y. Duan, Y. Feng, and Z. F. Ji. 2010. Predicate transformer semantics of quantum programs. In: I. Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 311--360."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629680","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:30Z","timestamp":1750227210000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629680"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,8]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,7,8]]}},"alternative-id":["10.1145\/2629680"],"URL":"https:\/\/doi.org\/10.1145\/2629680","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7,8]]},"assertion":[{"value":"2010-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-08-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}