zbMATH — the first resource for mathematics

Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties. (English) Zbl 1329.68119
Summary: In this paper, we study a model of quantum Markov chains that is a quantum analogue of Markov chains and is obtained by replacing probabilities in transition matrices with quantum operations. We show that this model is very suited to describe hybrid systems that consist of a quantum component and a classical one. Indeed, hybrid systems are often encountered in quantum information processing. Thus, we further propose a model called hybrid quantum automata (HQA) that can be used to describe the hybrid systems receiving inputs (actions) from the outer world. We show the language equivalence problem of HQA is decidable in polynomial time. Furthermore, we apply this result to the trace equivalence problem of quantum Markov chains, and thus it is also decidable in polynomial time. Finally, we discuss model checking linear-time properties of quantum Markov chains, and show the quantitative analysis of regular safety properties can be addressed successfully.

68Q12 Quantum algorithms and complexity in the theory of computing
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
81P68 Quantum computation
Full Text: DOI
[1] Aharonov, D.; Ambainis, A.; Kempe, J.; Vazirani, U., Quantum walks on graphs, (Proceedings of the 33rd ACM Symposium on Theory of Computing, (2001), ACM), 50-59 · Zbl 1323.81020
[2] Accardi, L.; Koroliuk, D., Stopping times for quantum Markov chains, J. Theor. Probab., 5, 251-535, (1992) · Zbl 0751.60081
[3] Ambainis, A.; Watrous, J., Two-way finite automata with quantum and classical states, Theor. Comput. Sci., 287, 299-311, (2002) · Zbl 1061.68047
[4] Baier, C.; Katoen, J.-P., Principles of model checking, (2008), The MIT Press
[5] Bertoni, A.; Mereghetti, C.; Palano, B., Quantum computing: 1-way quantum automata, (Proceedings of the 9th International Conference on Developments in Language Theory, LNCS, vol. 2710, (2003), Springer), 1-20 · Zbl 1037.68058
[6] Christoff, L.; Christoff, I., Efficient algorithms for verification of equivalences for probabilistic processes, (CAV1991, LNCS, vol. 575, (1992), Springer), 310-321
[7] Doyen, L.; Henzinger, T. A.; Raskin, J.-F., Equivalence of labeled Markov chains, Int. J. Found. Comput. Sci., 19, 3, 549-563, (2008) · Zbl 1155.68035
[8] Feng, Y.; Yu, N. K.; Ying, M. S., Model checking quantum Markov chains, J. Comput. Syst. Sci., 79, 1181-1198, (2013) · Zbl 1311.68086
[9] Gudder, S., Quantum Markov chains, J. Math. Phys., 49, 7, 072105, (2008) · Zbl 1152.81457
[10] Henzinger, T. A., The theory of hybrid automata, (LICS96, (1996)), 278-292
[11] Hirvensalo, M., Quantum automata with open time evolution, Int. J. Nat. Comput. Res., 1, 70-85, (2010)
[12] Kiefer, S.; Murawski, A. S.; Ouaknine, J.; Wachter, B.; Worrell APEX, J., An analyzer for open probabilistic programs, (CAV 2012, LNCS, vol. 7358, (2012), Springer), 693-698
[13] Kiefer, S.; Murawski, A. S.; Ouaknine, J.; Wachter, B.; Worrell, J., Language equivalence for probabilistic automata, (CAV2011, LNCS, vol. 6806, (2011), Springer), 526-540
[14] Li, L. Z.; Feng, Y., On hybrid models of quantum finite automata, J. Comput. Syst. Sci., 81, 1144-1158, (2015) · Zbl 1323.68273
[15] Li, L. Z.; Qiu, D. W., Characterizations of one-way general quantum finite automata, Theor. Comput. Sci., 419, 73-91, (2012) · Zbl 1235.68102
[16] Li, L. Z.; Qiu, D. W., Determining the equivalence for one-way quantum finite automata, Theor. Comput. Sci., 403, 42-51, (2008) · Zbl 1175.68250
[17] Liu, C.; Petulante, N., On limiting distributions of quantum Markov chains, Int. J. Math. Math. Sci., 2011, 740816, (2011) · Zbl 1225.81080
[18] Murawski, A. S.; Ouaknine, J., On probabilistic program equivalence and refinement, (CONCUR2005, LNCS, vol. 3653, (2005), Springer), 156-170 · Zbl 1134.68351
[19] Nielsen, M. A.; Chuang, I. L., Quantum computation and quantum information, (2000), Cambridge University Press Cambridge · Zbl 1049.81015
[20] Paz, A., Introduction to probabilistic automata, (1971), Academic Press New York · Zbl 0234.94055
[21] Qiu, D. W.; Li, L. Z.; Mateus, P.; Sernadas, A., Exponentially more concise quantum recognition of non-RMM regular languages, J. Comput. Syst. Sci., 81, 359-375, (2015) · Zbl 1401.81039
[22] Qiu, D. W.; Li, L. Z.; Mateus, P.; Gruska, J., Quantum finite automata, (Wang, Jiacun, Finite State Based Models and Applications, (2012)), CRC handbook
[23] Raskin, J. F., An introduction to hybrid automata, Handbook of Networked and Embedded Control Systems Control Engineering, vol. IV, 491-517, (2005), Springer
[24] Selinger, P., Towards a quantum programming language, Math. Struct. Comput. Sci., 14, 4, 527-586, (2004) · Zbl 1085.68014
[25] Tzeng, W. G., A polynomial-time algorithm for the equivalence of probabilistic automata, SIAM J. Comput., 21, 2, 216-227, (1992) · Zbl 0755.68075
[26] Watrous, J., On the complexity of simulating space-bounded quantum computations, Comput. Complex., 12, 48-84, (2003) · Zbl 1068.68066
[27] Watrous, J., Lecture notes on theory of quantum information · Zbl 1162.47308
[28] Ying, M. S.; Yu, N. K.; Feng, Y.; Duan, R. Y., Verification of quantum programs, Sci. Comput. Program., 78, 9, 1679-1700, (2013)
[29] Zheng, S. G.; Qiu, D. W.; Gruska, J., Power of the interactive proof systems with verifiers modeled by semi-quantum two-way finite automata, Inf. Comput., 241, 197-214, (2015) · Zbl 1309.68074
[30] Zheng, S. G.; Qiu, D. W.; Li, L. Z.; Gruska, J., One-way finite automata with quantum and classical states, (Dassow Festschrift 2012, LNCS, vol. 7300, (2012), Springer), 273-290 · Zbl 1330.68183
[31] Zheng, S. G.; Gruska, J.; Qiu, D. W., On the state complexity of semi-quantum finite automata, RAIRO Theor. Inform. Appl., 48, 187-207, (2014) · Zbl 1292.81027
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.