• quantum computing
• qCCS
• barbed bisimilarity
• probabilistic bisimilarity
• process calculus

With the development of quantum communication protocols, numerous quantum process
calculi have been proposed, but none as emerged has an accepted standard. Moreover,
an established notion of behavioural equivalence is still missing. In this work we present
a new asynchronous calculus, Linear qCCS, featuring a linear type system and two novel
bisimilarity relations. Our language allows to directly compare the semantics of previous
proposals, and investigate which notion of behavioural equivalence is most consistent
with the quantum mechanical rules. One of the main result is that the usual and
well-accepted definition of probabilistic bisimilarity is not appropriate for the quantum
setting. Hence we introduce quantum saturated bisimilarity, which adequately formalize
the observable properties of quantum system. Finally, we also explore a foundational
approach, presenting a Minimal Quantum Process Algebra, in order to investigate, in
a minimal framework, the essential characteristics of communicating quantum systems.
For this model we define a symbolic semantics, where the probabilistic behaviour of each
process is ‘parametric’ with respect to its input quantum values.