微信里点“发现”，扫一下
二维码便可将本文分享至朋友圈
演讲摘要：In this talk, we describe a framework for assertion-based verification of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks; Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the following design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimization techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.
讲者简介：早年从事数理逻辑及其在人工智能中的应用以及软件理论方面的研究。近20年来致力于系统地创建量子程序设计的理论基础，建立了量子Hoare逻辑并证明了其（相对）完备性定理，定义了量子程序的不变量这个基本概念，并开辟了量子模型检测及其在量子电路验证与测试中的应用这一新方向。出版专著"Model Checking Quantum Systems: Principles and Algorithms" (Cambridge University Press, 2021)，“Foundations of Quantum Programming”（Elsevier - Morgan Kaufmann, 2016）及“Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs”（Springer-Verlag, 2001）。
本期嘉宾
第二届CCF量子计算大会暨中国量子计算产业峰会（CQCC 2023）
京公网安备11010802032778号