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.
Verification of Quantum Systems Using Barrier Certificates / Lewis, Marco; Zuliani, Paolo; Soudjani, Sadegh. - 14287 LNCS:(2023), pp. 346-362. ( QEST 2023: 20th International Conference on Quantitative Evaluation of SysTems Antwerp, Belgium ) [10.1007/978-3-031-43835-6_24].
Verification of Quantum Systems Using Barrier Certificates
Paolo ZulianiCo-primo
;
2023
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.


