Publication Details

Verifying Quantum Circuits with Level-Synchronized Tree Automata

ABDULLA Parosh A., CHEN Yo-ga, CHEN Yu-Fang, HOLÍK Lukáš, LENGÁL Ondřej, LIN Jyun-ao, LO Fang-yi and TSAI Wei-lun. Verifying Quantum Circuits with Level-Synchronized Tree Automata. Proceedings of the ACM on Programming Languages, vol. 9, no. 1, 2024, p. 31. ISSN 2475-1421.
Czech title
Verifikace kvantových obvodů s pomocí úrovňově synchronizovaných stromových automatů
Type
journal article
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Chen Yo-ga (ASIN)
Chen Yu-Fang (ASIN)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Lin Jyun-ao (ASIN)
Lo Fang-yi (ASIN)
Tsai Wei-lun (ASIN)
Keywords

quantum circuits,tree automata, verification

Abstract

We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices, which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification, i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches. We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.

Published
2024 (in print)
Pages
31
Journal
Proceedings of the ACM on Programming Languages, vol. 9, no. 1, ISSN 2475-1421
Book
Proceedings of POPL'25
Publisher
Association for Computing Machinery
DOI
10.1145/3704868
BibTeX 
@ARTICLE{FITPUB13304,
   author = "A. Parosh Abdulla and Yo-ga Chen and Yu-Fang Chen and Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Jyun-ao Lin and Fang-yi Lo and Wei-lun Tsai",
   title = "Verifying Quantum Circuits with Level-Synchronized Tree Automata",
   pages = 31,
   booktitle = "Proceedings of POPL'25",
   journal = "Proceedings of the ACM on Programming Languages",
   volume = 9,
   number = 1,
   year = 2024,
   ISSN = "2475-1421",
   doi = "10.1145/3704868",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13304"
}
Back to top