This is a benchmark for equivalence checking of quantum circuits using quantum Mealy machine [WLY21].
A quantum Mealy machine (QMM) is a 5-tuple , where:
- is a finite input alphabet;
- is a finite output alphabet;
- is a finite-dimensional Hilbert space;
- is a set of unitary operators. For each , is a unitary operator on ; and
- is a quantum measurement in , that is, is a linear operator on for each and .
See [WLY21] for more details.
The benchmark is for equivalence checking of two states in a QMM. That is, given a QMM and two states and , decide whether and for some .
testXXX.data is a binary file, whose contents are listed below:
<dim, int>
<sigma, int>
<gamma, int>
<limit, int>
<eps, double>
for a in 0..sigma-1:
for i in 0..dim-1:
for j in 0..dim-1:
<unitary[a][i][j].real, double>
<unitary[a][i][j].imag, double>
for b in 0..sigma-1:
for i in 0..dim-1:
for j in 0..dim-1:
<measure[b][i][j].real, double>
<measure[b][i][j].imag, double>
for i in 0..dim-1:
for j in 0..dim-1:
<rho1[i][j].real, double>
<rho1[i][j].imag, double>
for i in 0..dim-1:
for j in 0..dim-1:
<rho2[i][j].real, double>
<rho2[i][j].imag, double>
The offsets of the first few data are shown below for calibration:
offset <content, type>
0000 <dim, int>
0004 <sigma, int>
0008 <gamma, int>
000c <limit, int>
0010 <eps, double>
....
We select test002 as an illustrative example, in which case:
“limit” denotes . It is noted that for the case “limit = -1”, it means that no such is required, or equivalently holds.
The implementation of checking equivalence of QMM is the file "qmm.h".
The hard-coded data is seen in "datafactory.h".
[WLY21] Qisheng Wang, Junyi Liu and Mingsheng Ying. Equivalence checking of quantum finite-state machines. Journal of Computer and System Sciences, 116: 1-21, 2021. arXiv:1901.02173. doi:10.1016/j.jcss.2020.08.004.