微信服务号

微信订阅号

2025年5月10日 21:05 星期六
首页 > 过刊浏览>2018年第29卷第4期 >1085-1093. DOI:10.13328/j.cnki.jos.005536
PDF HTML阅读 XML下载 导出引用 引用提醒
量子程序验证
作者:
作者简介:

冯元(1977-),男,四川西充人,博士,教授,博士生导师,主要研究领域为量子计算,程序理论,量子程序验证;应明生(1964-),男,教授,博士生导师,CCF专业会员,主要研究领域为量子计算,程序理论,人工智能基础.

通讯作者:

冯元,E-mail:Yuan.Feng@uts.edu.au

基金项目:

中国科学院前沿科学重点研究计划（QYZDJ-SSW-SYS003）；中国科学院、国家外国专家局创新团队国际合作伙伴计划


Verification of Quantum Programs
Author:
Fund Project:

Key Research Program of Frontier Sciences, CAS (QYZDJ-SSW-SYS003); CAS/SAFEA Int'l Partnership Program for Creative Research Teams

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [59]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5~10年内实现.可以想见，到那时候，量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而，由于量子信息的不可克隆性和纠缠的非局域作用等量子特征，如何设计正确、高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法，特别是模型检测技术，已在经典软件设计和系统建模方面被证明行之有效，因此量子软件的形式化验证也开始受到越来越多的关注.从量子顺序程序验证和量子通信协议验证两方面，对近年来国内外学者，尤其对University of Technology Sydney和清华大学的研究组在该研究领域取得的一些成果进行了系统的总结.最后，对未来可能的研究方向和面临的挑战进行了简单展望.

    Abstract:

    With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5 to 10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication protocols is a challenging issue. Formal verification methods, particularly model checking techniques, have proven effective in classical software design and system modelling. Therefore, formal verification of quantum software has received more and more attention recently. This article reviews recent research findings in verification of both sequential quantum programs and quantum communication protocols, with the focus placed on the work of the two authors' research groups. Future directions and challenges in this area are also discussed.

    参考文献
    [1] Wecker D, Svore KM. LIQUi|>:A software design architecture and domain-specific language for quantum computing. arXiv.org, vol. quant-ph. p. arXiv:1402.4467, 19-Feb-2014.
    [2] Häner T, Steiger DS, Svore K, Troyer M. A software methodology for compiling quantum programs. arXiv.org, vol. cs.PL. p. arXiv:1604.01401, 06-Apr-2016.
    [3] The Q# Programming Language. 2017. https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview
    [4] Green AS, Lumsdaine PL, Ross NJ, Selinger P, Valiron B. Quipper-A scalable quantum programming language. In:Proc. of the PLDI. 2013. 333-342.
    [5] JavadiAbhari A, Patil S, Kudrow D, Heckey J, Lvov A, Chong FT, Martonosi M. ScaffCC:Scalable compilation and analysis of quantum programs. arXiv.org, vol. quant-ph. pp. arXiv:1507.01902-17, 08-Jul-2015.
    [6] Lapets A, Roetteler M. Abstract resource cost derivation for logical quantum circuit descriptions. In:Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 35-42.[doi:10. 1145/2505351.2505358]
    [7] Lapets A, da Silva MP, Thome M, Adler A, Beal J, Roetteler M. QuaFL:A typed DSL for quantum programming. In:Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 19-26.[doi:10.1145/2505351.2505357]
    [8] Ying MS, Feng Y. An algebraic language for distributed quantum computing. IEEE Trans. on Computers, 2009,58(6):728-743.[doi:10.1109/TC.2009.13]
    [9] Ying MS, Feng Y. A flowchart language for quantum programming. IEEE Trans. on Software Engineering, 2011,37(4):466-485.[doi:10.1109/TSE.2010.94]
    [10] Ying MS, Feng Y. Quantum loop programs. Acta Informatica, 2010,47(4):221-250.[doi:10.1007/s00236-010-0117-4]
    [11] Ying MS, Yu N, Feng Y, Duan R. Verification of quantum programs. Science of Computer Programming, 2013,78(9):1679-1700.[doi:10.1016/j.scico.2013.03.016]
    [12] Perdrix S. Quantum entanglement analysis based on abstract interpretation. In:Proc. of the SAS. 2008. 270-282.[doi:10.1007/978-3-540-69166-2_18]
    [13] Jorrand P, Perdrix S. Abstract interpretation techniques for quantum computation. In:Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge:Cambridge University Press, 2009,(6):206-234.
    [14] Honda K. Analysis of quantum entanglement in quantum programs using stabilizer formalism. Electronic Proc. in Theoretical Computer Science, 2015,195(1):262-272.[doi:10.4204/EPTCS.195.19]
    [15] Brunet O, Jorrand P. Dynamic quantum logic for quantum programs. Int'l Journal of Quantum Information, 2011,2(1):45-54.[doi:10.1142/S0219749904000067]
    [16] Baltag A, Smets S. LQP:The dynamic logic of quantum information. Math. Struct. in Comp. Science, 2006,16(3):491-525.[doi:10. 1017/S0960129506005299]
    [17] Feng Y, Duan R, Ji Z, Ying MS. Proof rules for the correctness of quantum programs. Theoretical Computer Science, 2007,386(1):151-166.[doi:10.1016/j.tcs.2007.06.011]
    [18] Chadha R, Mateus P, Sernadas A. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science, 2006.[doi:10.1016/j.entcs.2006.04.003]
    [19] Kakutani Y. A logic for formal verification of quantum programs. In:Proc. of the ASIAN. 2009.[doi:10.1007/978-3-642-10622-4_7]
    [20] Ying MS. Floyd-Hoare logic for quantum programs. Trans. on Programming Languages and Systems, 2011,33(6):1-49.[doi:10. 1145/2049706.2049708]
    [21] Liu T, Li Y, Wang S, Ying MS, Zhan N. A theorem prover for quantum hoare logic and its applications. arXiv.org, vol. cs.LO. p. arXiv:1601.03835, 15-Jan-2016.
    [22] Hasuo I, Hoshino N. Semantics of higher-order quantum computation via geometry of interaction. Annals of Pure and Applied Logic, 2017.[doi:10.1109/LICS.2011.26]
    [23] Pagani M, Selinger P, Valiron B. Applying quantitative semantics to higher-order quantum computing. In:Proc. of the POPL. 2014.[doi:10.1145/2578855.2535879]
    [24] Jacobs B. On block structures in quantum computation. Electronic Notes in Theoretical Computer Science, 2013,298:233-255.[doi:10.1016/j.entcs.2013.09.016]
    [25] Staton S. Algebraic effects, linearity, and quantum programming languages. In:Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. New York, 2015. 395-406.[doi:10.1145/2775051.2676999]
    [26] D'Hondt E, Panangaden P. Quantum weakest preconditions. Mathematical Structures in Computer Science, 2006.[doi:10.1017/S0960129506005251]
    [27] Ying MS, Duan R, Feng Y, Ji Z. Predicate transformer semantics of quantum programs. In:Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge:Cambridge University Press, 2009,(8):311-360.
    [28] Ying S, Feng Y, Yu N, Ying MS. Reachability probabilities of quantum Markov chains. In:Proc. of the CONCUR. 2013. 334-348.[doi:10.1007/978-3-642-40184-8_24]
    [29] Yu N, Ying MS. Reachability and termination analysis of concurrent quantum programs. In:Proc. of the CONCUR. 2012. 69-83.[doi:10.1007/978-3-642-32940-1_7]
    [30] Li Y, Ying MS. (Un)deciddable problems about reachability of quantum systems. In:Proc. of the CONCUR. 2014. 482-496.[doi:10.1007/978-3-662-44584-6_33]
    [31] Feng Y, Yu N, Ying MS. Model checking quantum Markov chains. Journal of Computer and System Sciences, 2013,79(7):1181-1198.[doi:10.1016/j.jcss.2013.04.002]
    [32] Vardi YM. Automatic verification of probabilistic concurrent finite-state programs. In:Proc. of the FOCS. 1985.[doi:10.1109/SFCS.1985.12]
    [33] Diestel J, Uhl J. Vector Measures, vol. 15. Providence:American Mathematical Society, 1977.
    [34] Feng Y, Hahn EM, Turrini A, Zhang L. QPMC:A model checker for quantum programs and protocols. In:Proc. of the FM. 2015. 265-272.[doi:10.1007/978-3-319-19249-9_17]
    [35] Kwiatkowska MZ, Norman G, Parker D. PRISM 4.0-Verification of probabilistic real-time systems. In:Proc. of the CAV. 2011.[doi:10.1007/978-3-642-22110-1_47]
    [36] Anticoli L, Piazza C, Taglialegne L, Zuliani P. Towards quantum programs verification-From quipper circuits to QPMC. In:Proc. of the RC. 2016.[doi:10.1007/978-3-319-40578-0_16]
    [37] Feng Y, Hahn EM, Turrini A, Ying S. Model checking Omega-regular properties for quantum Markov chains. In:Proc. of the CONCUR. 2017. 35:1-35:16.[doi:10.1007/978-3-540-78499-9_22]
    [38] Feng Y, Yu N, Ying MS. Reachability analysis of recursive quantum Markov chains. In:Proc. of the MFCS. 2013. 385-396.[doi:10.1007/978-3-642-40313-2_35]
    [39] Etessami K, Yannakakis M. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM, 2009,1.[doi:10.1145/1462153.1462154]
    [40] Esparza J, Kiefer S, Luttenberger M. Newtonian program analysis. Journal of the ACM, 2010,57(6):1-47.[doi:10.1145/1857914. 1857917]
    [41] Advancing Quantum Information Science:National Challenges and Opportunities. 2016. https://www.whitehouse.gov/sites/whitehouse.gov/files/images/Quantum_Info_Sci_Report_2016_07_22%20final.pdf
    [42] Jorrand P, Lalire M. Toward a quantum process algebra. In:Proc. of the 1st Conf. on Computing Frontiers on Computing Frontiers. New York, 2004. 111-119.
    [43] Lalire M. Relations among quantum processes:bisimilarity and congruence. Mathematical Structures in Computer Science, 2006, 16(3):407.[doi:10.1017/S096012950600524X]
    [44] Gay S, Nagarajan R. Communicating quantum processes. In:Proc. of the POPL. 2005.[doi:10.1145/1040305.1040318]
    [45] Feng Y. Duan R. Ji Z, Ying M. Probabilistic bisimulations for quantum processes. Information and Computation, 2007,205(11):1608-1639.[doi:10.1016/j.ic.2007.08.001]
    [46] Ying MS, Feng Y, Duan R, Ji Z. An algebra of quantum processes. ACM Trans. on Computational Logic (TOCL), 2009,10(3):19-36.[doi:10.1145/1507244.1507249]
    [47] Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. In:Proc. of the POPL. New York, 2011. 523-534.[doi:10.1145/1926385.1926446]
    [48] Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. Trans. on Programming Languages and Systems, 2012,34(4):1-43.
    [49] Deng Y, Feng Y. Open bisimulation for quantum processes. In:Proc. of the IFIP TCS. 2012.[doi:10.1007/978-3-642-33475-7_9]
    [50] Feng Y, Deng Y, Ying MS. Symbolic bisimulation for quantum processes. ACM Trans. on Computational Logic, 2014,15(2):1-32.[doi:10.1145/2579818]
    [51] Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995,138(2):353-389.
    [52] Kubota T, Kakutani Y, Kato G, Kawano Y, Sakurada H. Semi-Automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation, 2016,73:192-220.[doi:10.1016/j.jsc.2015.05.001]
    [53] Feng Y, Ying MS. Toward automatic verification of quantum cryptographic protocols. In:Proc. of the CONCUR. 2015. 441-455.
    [54] Deng Y, Feng Y, Lago UD. On coinduction and quantum Lambda Calculi. In:Proc. of the CONCUR. 2015. 427-440.
    [55] Ardeshir-Larijani E, Gay SJ, Nagarajan R. Equivalence checking of quantum protocols. In:Proc. of the TACAS. Berlin, Heidelberg, 2013,7795(33):478-492.[doi:10.1007/978-3-642-36742-7_33]
    [56] Ardeshir-Larijani E, Gay SJ, Nagarajan R. Verification of concurrent quantum protocols by equivalence checking. In:Proc. of the TACAS. Berlin, Heidelberg, 2014,8413(42):500-514.[doi:10.1007/978-3-642-54862-8_42]
    [57] Altenkirch T, Grattage J. A functional quantum programming language. In:Proc. of the LICS. 2005. 249-258.
    [58] Bădescu C, Panangaden P. Quantum alternation:Prospects and problems. Electronic Proc. in Theoretical Computer Science, 2015, 195(1):33-42.[doi:10.4204/EPTCS.195.3]
    [59] Ying MS. Foundations of Quantum Programming. Elsevier Science, 2016.
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

冯元,应明生.量子程序验证.软件学报,2018,29(4):1085-1093

复制
相关视频

分享
文章指标
  • 点击次数:4579
  • 下载次数: 8267
  • HTML阅读次数: 4689
  • 引用次数: 0
历史
  • 收稿日期:2017-12-24
  • 最后修改日期:2018-01-03
  • 在线发布日期: 2018-01-09
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19920949位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号