Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach

TL;DR

This paper introduces a scenario-based method for synthesizing barrier certificates to verify quantum circuits, effectively handling uncertainties and applicable to both finite and infinite time horizons.

Contribution

It presents a novel scenario approach for barrier certificate synthesis in quantum circuit verification, accommodating uncertainties and diverse time horizons.

Findings

Effective verification of quantum circuits demonstrated through case studies.

Comparison of barrier certificate types identifies most suitable methods for different scenarios.

Method handles uncertainties in initial states and system dynamics.

Abstract

In recent years, various techniques have been explored for the verification of quantum circuits, including the use of barrier certificates, mathematical tools capable of demonstrating the correctness of such systems. These certificates ensure that, starting from initial states and applying the system's dynamics, the system will never reach undesired states. In this paper, we propose a methodology for synthesizing such certificates for quantum circuits using a scenario-based approach, for both finite and infinite time horizons. In addition, our approach can handle uncertainty in the initial states and in the system's dynamics. We present several case studies on quantum circuits, comparing the performance of different types of barrier certificate and analyzing which one is most suitable for each case.