Verifying Repeat-until-Success Protocols using Automata

Abstract

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.