Bisimulation for quantum processes

TL;DR

This paper introduces a new probabilistic bisimulation concept for quantum processes, ensuring congruence with process algebra operations and enabling verification of complex quantum protocols.

Contribution

It presents a novel bisimulation framework for quantum processes that maintains congruence under various operations, including parallel composition, and establishes algebraic laws for verification.

Findings

Bisimulation is congruent with process algebra combinators.

Unique solutions to recursive quantum process equations are proven.

Provides a new proof technique for quantum protocol verification.

Abstract

In this paper we introduce a novel notion of probabilistic bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.