Branching bisimulation semantics for quantum processes. (English) Zbl 1541.68262
Summary: The qCCS model proposed by Feng et al. provides a powerful framework to describe and reason about quantum communication systems that could be entangled with the environment. However, they only studied weak bisimulation semantics. In this paper we propose a new branching bisimilarity for qCCS and show that it is a congruence. The new bisimilarity is based on the concept of \(\epsilon\)-tree and preserves the branching structure of concurrent processes where both quantum and classical components are allowed. Furthermore, we present a polynomial time equivalence checking algorithm for the ground version of our branching bisimilarity.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q55 | Semantics in the theory of computing |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 81P68 | Quantum computation |
References:
| [1] | Basten, T., Branching bisimilarity is an equivalence indeed!, Inf. Process. Lett., 58, 3, 141-147, 1996 · Zbl 0875.68624 |
| [2] | Castiglioni, V.; Tini, S., Raiders of the lost equivalence: probabilistic branching bisimilarity, Inf. Process. Lett., 159-160, Article 105947 pp., 2020 · Zbl 1441.68145 |
| [3] | Davidson, T. A.S., Formal Verification Techniques Using Quantum Process Calculus, 2012, University of Warwick, Ph.D. thesis |
| [4] | Deng, Y.; Feng, Y., Open bisimulation for quantum processes, (Baeten, J. C.M.; Ball, T.; de Boer, F. S., Theoretical Computer Science. Theoretical Computer Science, Lecture Notes in Computer Science, 2012, Springer: Springer Berlin, Heidelberg), 119-133 · Zbl 1362.68210 |
| [5] | Deng, Y.; Feng, Y., Open bisimulation for quantum processes, 2012, (full version) |
| [6] | Feng, Y.; Deng, Y.; Ying, M., Symbolic bisimulation for quantum processes, ACM Trans. Comput. Log., 15, 2, Article 14 pp., 2014 · Zbl 1291.68237 |
| [7] | Feng, Y.; Duan, R.; Ji, Z.; Ying, M., Probabilistic bisimulations for quantum processes, Inf. Comput., 205, 11, 1608-1639, 2007 · Zbl 1130.68079 |
| [8] | Feng, Y.; Duan, R.; Ying, M., Bisimulation for quantum processes, (Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’11, 2011, Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 523-534 · Zbl 1284.68425 |
| [9] | Feynman, R. P., Simulating physics with computers, Int. J. Theor. Phys., 21, 6, 467-488, 1982 |
| [10] | Fu, Y., Theory of interaction, Theor. Comput. Sci., 611, 1-49, 2016 · Zbl 1353.68082 |
| [11] | Fu, Y., Model independent approach to probabilistic models, Theor. Comput. Sci., 869, 181-194, 2021 · Zbl 1497.68338 |
| [12] | Gay, S. J.; Nagarajan, R., Communicating quantum processes, (Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’05, 2005, Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 145-157 · Zbl 1369.68207 |
| [13] | Graf, S.; Sifakis, J., Readiness semantics for regular processes with silent actions, (Ottmann, T., Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, 1987, Springer: Springer Berlin, Heidelberg), 115-125 · Zbl 0646.68019 |
| [14] | Hennessy, M., A proof system for communicating processes with value-passing, Form. Asp. Comput., 3, 4, 346-366, 1991 · Zbl 0736.68057 |
| [15] | Hennessy, M.; Ingolfsdottir, A., A theory of communicating processes with value passing, Inf. Comput., 107, 2, 202-236, 1993 · Zbl 0794.68098 |
| [16] | Jorrand, P.; Lalire, M., Toward a quantum process algebra, (Proceedings of the 1st Conference on Computing Frontiers, CF’04, 2004, Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 111-119 |
| [17] | Lalire, M., Relations among quantum processes: bisimilarity and congruence, Math. Struct. Comput. Sci., 16, 3, 407-428, 2006 · Zbl 1122.68060 |
| [18] | Milner, R., Communication and Concurrency, 1989, Prentice-Hall, Inc. · Zbl 0683.68008 |
| [19] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I, Inf. Comput., 100, 1, 1-40, 1992 · Zbl 0752.68036 |
| [20] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, II, Inf. Comput., 100, 1, 41-77, 1992 · Zbl 0752.68037 |
| [21] | Nielsen, M. A.; Chuang, I. L., Quantum Computation and Quantum Information, 2010, Cambridge University Press, Cambridge: Cambridge University Press, Cambridge New York, 10th anniversary ed edn · Zbl 1288.81001 |
| [22] | Qin, X.; Deng, Y.; Du, W., Verifying quantum communication protocols with ground bisimulation, (Biere, A.; Parker, D., Tools and Algorithms for the Construction and Analysis of Systems. Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 2020, Springer International Publishing: Springer International Publishing Cham), 21-38 · Zbl 1473.68115 |
| [23] | Segala, R., Modeling and Verification of Randomized Distributed Real-Time Systems, 1995, Massachusetts Institute of Technology, Thesis |
| [24] | Turrini, A.; Hermanns, H., Polynomial time decision algorithms for probabilistic automata, Inf. Comput., 244, 134-171, 2015 · Zbl 1329.68168 |
| [25] | van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600, 1996 · Zbl 0882.68085 |
| [26] | Wootters, W. K.; Zurek, W. H., A single quantum cannot be cloned, Nature, 299, 5886, 802-803, 1982 · Zbl 1369.81022 |
| [27] | Wu, H.; Long, H., Probabilistic weak bisimulation and axiomatization for probabilistic models, Inf. Process. Lett., 182, Article 106399 pp., 2023 · Zbl 07691958 |
| [28] | Ying, M.; Feng, Y.; Duan, R., An algebra of quantum processes, ACM Trans. Comput. Log., 10, 3, 36, 2009 · Zbl 1351.68187 |
| [29] | Zhang, W.; Long, H.; Xu, X., Uniform random process model revisited, (Lin, A. W., Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, 2019, Springer International Publishing: Springer International Publishing Cham), 388-404 · Zbl 1542.68108 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
