Verifying Repeat-until-Success Protocols using Automata
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...