Model Checking for Verification of Quantum Circuits
- Publisher:
- Springer
- Publication Type:
- Conference Proceeding
- Citation:
- Formal Methods, 2021, 13047 LNCS, pp. 23-39
- Issue Date:
- 2021-01-01
Closed Access
| Filename | Description | Size | |||
|---|---|---|---|---|---|
| Ying2021_Chapter_ModelCheckingForVerificationOf.pdf | Published version | 396.15 kB |
Copyright Clearance Process
- Recently Added
- In Progress
- Closed Access
This item is closed access and not available.
In this survey paper, we describe a framework for assertion-based verification of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks.Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the following design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements);Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.
Please use this identifier to cite or link to this item: