Verification of Quantum Systems using Barrier Certificates
arXiv:2307.07307 · doi:10.1007/978-3-031-43835-6_24
Abstract
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.
arXiv comment18 pages, 5 figures
References in corpus (10)
- Quantum-state preparation with universal gate decompositions
- Formal Synthesis of Stochastic Systems via Control Barrier Certificates
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Quantum feedback for rapid state preparation in the presence of control imperfections
- Preparing Valence-Bond-Solid states on noisy intermediate-scale quantum computers
- Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions
- Proving Quantum Programs Correct
- Quantum gates by inverse engineering of a Hamiltonian
- Optimal Hamiltonian simulation for time-periodic systems
- Design of gates for quantum computation: the NOT gate