Quantum Bisimilarity via Barbs, Contexts and Schedulers

We carry out an in-depth investigation of the relationship between equivalences for process algebras and quantum observability. We introduce a new calculus, lqCCS, which shares the basic functionalities of the previous proposals but resolves ambiguities concerning the visibility of the quantum state. Through the use of classical barbs and contexts, we trace several issues that plague standard equivalences and propose desiderata that make a behavioural equivalence suitable for dealing with quantum protocols. We identify non-determinism as a major cause for the excessive discriminating power, as it indirectly allows us to observe the quantum state without making measurements, which is impossible according to quantum theory. We weaken non-determinism in contexts to prevent them from making choices that are not physically realizable, and we check that non-determinism is still able to simulate choices motivated by known classical observables. This admittedly simple solution allows us to prove faithfulness with the prescriptions of quantum theory, by lifting a defining indistinguishability result from quantum values to lqCCS processes. Then, we enrich lqCCS with explicit schedulers that characterize the physically admissible choices of processes, and we make observables explicit by giving a labelled equivalence that is a congruence for the parallel operator.