TY - GEN
T1 - Bounded Quantum Regular Language Generator
AU - Kwon, Young Min
AU - Agha, Gul
N1 - This work was supported by NRF of MSIT, Korea (2021R1F1A104859812) and by the MSIT, Korea, under the ICTCCP(IITP-2020-2011-1-00783) supervised by the IITP.
PY - 2023
Y1 - 2023
N2 - We develop a quantum algorithm to verify the correctness of systems modeled by nondeterministic finite-state automata-a problem that is computationally intractable on conventional computers. Specifically, our algorithm solves the language containment problem in three steps. First, we translate a nondeterministic finite-state automaton into a quantum finite state automaton (QFA) circuit. Second, the QFA is embedded into a larger circuit which generates a superposed set of all bounded strings that are marked to indicate whether they are accepted or not. Finally, we amplify the amplitudes of accepted strings so that they are measured more frequently. The last step may be done either by using Grover's algorithm, or by using FnR, a custom algorithm that we have developed for the cases where Grover's algorithm is not effective. Our work represents the first proposal to apply quantum computing to the problem of verifying conventional systems; our approach would facilitate software verification, program analysis, protocol design, and verification of circuits, among other applications.
AB - We develop a quantum algorithm to verify the correctness of systems modeled by nondeterministic finite-state automata-a problem that is computationally intractable on conventional computers. Specifically, our algorithm solves the language containment problem in three steps. First, we translate a nondeterministic finite-state automaton into a quantum finite state automaton (QFA) circuit. Second, the QFA is embedded into a larger circuit which generates a superposed set of all bounded strings that are marked to indicate whether they are accepted or not. Finally, we amplify the amplitudes of accepted strings so that they are measured more frequently. The last step may be done either by using Grover's algorithm, or by using FnR, a custom algorithm that we have developed for the cases where Grover's algorithm is not effective. Our work represents the first proposal to apply quantum computing to the problem of verifying conventional systems; our approach would facilitate software verification, program analysis, protocol design, and verification of circuits, among other applications.
KW - QFA Synthesis
KW - Quantum Finite-state Automata
KW - Quantum Language Containment Problem
KW - Quantum Regular Language Generator
UR - http://www.scopus.com/inward/record.url?scp=85180010961&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85180010961&partnerID=8YFLogxK
U2 - 10.1109/QCE57702.2023.00072
DO - 10.1109/QCE57702.2023.00072
M3 - Conference contribution
AN - SCOPUS:85180010961
T3 - Proceedings - 2023 IEEE International Conference on Quantum Computing and Engineering, QCE 2023
SP - 580
EP - 590
BT - Proceedings - 2023 IEEE International Conference on Quantum Computing and Engineering, QCE 2023
A2 - Muller, Hausi
A2 - Alexev, Yuri
A2 - Delgado, Andrea
A2 - Byrd, Greg
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 4th IEEE International Conference on Quantum Computing and Engineering, QCE 2023
Y2 - 17 September 2023 through 22 September 2023
ER -