Verifying Quantum Circuits with Level-Synchronized Tree Automata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0193377" target="_blank" >RIV/00216305:26230/26:0193377 - isvavai.cz</a>
Result on the web
<a href="https://dl.acm.org/doi/10.1145/3704868" target="_blank" >https://dl.acm.org/doi/10.1145/3704868</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3704868" target="_blank" >10.1145/3704868</a>
Alternative languages
Result language
angličtina
Original language name
Verifying Quantum Circuits with Level-Synchronized Tree Automata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Proceedings of the ACM on Programming Languages-PACMPL
ISSN
—
e-ISSN
2475-1421
Volume of the periodical
9
Issue of the periodical within the volume
1
Country of publishing house
US - UNITED STATES
Number of pages
31
Pages from-to
923-953
UT code for WoS article
001471014100019
EID of the result in the Scopus database
2-s2.0-85215979053