Reconciling Quantum Theory and Process Equivalence via Physically Admissible Schedulers

The recent development of quantum communication protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems, like process algebras have done for their classical counterparts. However, recovering the peculiar observational limitations prescribed by quantum theory has proven to be a challenging task in quantum systems expressing communication and non-determinism. The problem has been found to be in the interaction between quantum and non-determinism. We address it by resorting to schedulers, and we give behavioural equivalences for both branching and linear-time semantics that adheres to the prescriptions of quantum theory. Moreover, we show that the aforementioned difficulties occur also in simple systems that do not allow exchanging qubits via quantum channels.