一句话：提出基于层同步树自动机的全自动框架，验证 RUS 量子协议的功能正确性并发现文献中的新 bug。
Repeat-until-Success（RUS）协议通过测量、经典控制和无界循环实现单量子比特酉操作，其功能正确性验证需同时处理概率分支、无界循环、全输入态量化以及输入-输出对应关系。本文提出全自动验证框架：将量子态视为树、量子态集合视为树语言，并用层同步树自动机（LSTA）表示；借助 LSTA 中标记选择引入的非确定性，以选择序列语义追踪输入态到输出态的映射，从而支持关系式验证。为处理无限多量子态，作者证明三测试定理，将 RUS 协议正确性归约为有限多个输入上的测试，实现自动不变式合成与可判定验证。原型实现发现了 RUS 文献中此前未报告的错误。
Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice . Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature.
@article{paperbot12132,
title = {Verifying Repeat-until-Success Protocols using Automata},
author = {Jyun-Ao Lin and Yu-Fang Chen and Jakub Havlík and Ondřej Lengál and Fang-Yi Lo and Wei-Lun Tsai and You-Jie Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839506}
}