Symbolic bisimulation for quantum processes

Association for Computing Machinery
Publication Type:
Journal Article
ACM Transactions on Computational Logic, 2014, 15 (2), pp. 1 - 35
Issue Date:
Full metadata record
Files in This Item:
Filename Description Size
Thumbnailqsb.pdf845.2 kB
Adobe PDF
With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.
Please use this identifier to cite or link to this item: