Verification of Quantum Systems Using Barrier Certificates

被引：0
作者：
Lewis, Marco [1 ]
Zuliani, Paolo [1 ,2 ]
Soudjani, Sadegh [1 ,3 ]
机构：
[1] Newcastle Univ, Newcastle Upon Tyne, Tyne & Wear, England
[2] Univ Roma La Sapienza, Rome, Italy
[3] Max Planck Inst Software Syst, Kaiserslautern, Germany
来源：
QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2023 | 2023年 / 14287卷
基金：
英国工程与自然科学研究理事会;
关键词：
barrier certificates; dynamical systems; quantum systems;
D O I：
10.1007/978-3-031-43835-6_24
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification of correctness. Barrier certificates are a recent novel concept developed for verifying properties of dynamical systems. In this article, we investigate the usage of barrier certificates as a means for verifying behaviours of quantum systems. To do this, we extend the notion of barrier certificates from real to complex variables. We then develop a computational technique based on linear programming to automatically generate polynomial barrier certificates with complex variables taking real values. Finally, we apply our technique to several simple quantum systems to demonstrate their usage.
引用
收藏
页码：346 / 362
页数：17
相关论文
共 33 条
  • [1] FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks
    Abate, Alessandro
    Ahmed, Daniele
    Edwards, Alec
    Giacobbe, Mirco
    Peruffo, Andrea
    [J]. HSCC2021: PROCEEDINGS OF THE 24TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS-IOT WEEK), 2021,
  • [2] Set Propagation Techniques for Reachability Analysis
    Althoff, Matthias
    Frehse, Goran
    Girard, Antoine
    [J]. ANNUAL REVIEW OF CONTROL, ROBOTICS, AND AUTONOMOUS SYSTEMS, VOL 4, 2021, 2021, 4 : 369 - 395
  • [3] Ames AD, 2019, 2019 18TH EUROPEAN CONTROL CONFERENCE (ECC), P3420, DOI [10.23919/ECC.2019.8796030, 10.23919/ecc.2019.8796030]
  • [4] t-Barrier Certificates: A Continuous Analogy to k-Induction
    Bak, Stanley
    [J]. IFAC PAPERSONLINE, 2018, 51 (16): : 145 - 150
  • [5] Advanced Equivalence Checking for Quantum Circuits
    Burgholzer, Lukas
    Wille, Robert
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2021, 40 (09) : 1810 - 1824
  • [6] An Automated Deductive Verification Framework for Circuit-building Quantum Programs
    Chareton, Christophe
    Bardin, Sebastien
    Bobot, Francois
    Perrelle, Valentin
    Valiron, Benoit
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2021, 2021, 12648 : 148 - 177
  • [7] Clarke Jr Edmund M., 2018, Model checking
  • [8] Quantum feedback for rapid state preparation in the presence of control imperfections
    Combes, Joshua
    Wiseman, Howard M.
    [J]. JOURNAL OF PHYSICS B-ATOMIC MOLECULAR AND OPTICAL PHYSICS, 2011, 44 (15)
  • [9] Cousot P, 2001, LECT NOTES COMPUT SC, V2000, P138
  • [10] Cousot P., 1977, 4 ANN ACM SIGPLAN SI, P238, DOI [DOI 10.1145/512950.512973, 10.1145/512950.512973]
1234