On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914783129763840 |
|---|---|
| author | Sun, Xin Su, Xingchi Bian, Xiaoning Wu, Huiwen |
| author_facet | Sun, Xin Su, Xingchi Bian, Xiaoning Wu, Huiwen |
| contents | Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_01940 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On the Relative Completeness of Satisfaction-based Quantum Hoare Logic Sun, Xin Su, Xingchi Bian, Xiaoning Wu, Huiwen Logic in Computer Science 03B70 Logic in computer science F.3 Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation. |
| title | On the Relative Completeness of Satisfaction-based Quantum Hoare Logic |
| topic | Logic in Computer Science 03B70 Logic in computer science F.3 |
| url | https://arxiv.org/abs/2405.01940 |