Document Open Access Logo

Model Checking Quantum Continuous-Time Markov Chains

Authors Ming Xu , Jingyi Mei , Ji Guan , Nengkun Yu

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2021.13.pdf
  • Filesize: 0.94 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Computing methodologies → Symbolic and algebraic algorithms
  • Theory of computation → Quantum computation theory
Keywords
  • Model Checking
  • Formal Logic
  • Quantum Computing
  • Computer Algebra

Metrics

Abstract

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel’s conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

Cite As Get BibTex

Ming Xu, Jingyi Mei, Ji Guan, and Nengkun Yu. Model Checking Quantum Continuous-Time Markov Chains. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.13

Author Details

Ming Xu
  • Shanghai Key Lab of Trustworthy Computing, MoE Engineering Research Center of Software/Hardware Co-design Technology and Application, East China Normal University, Shanghai, China
Jingyi Mei
  • Shanghai Key Lab of Trustworthy Computing, East China Normal University, Shanghai, China
Ji Guan
  • State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Nengkun Yu
  • Centre for Quantum Software and Information, Faculty of Engineering and Information Technology, University of Technology, Sydney, Australia

Funding

  • Xu, Ming: The corresponding author M. X. is supported by the National Natural Science Foundation of China (No. 11871221), the National Key R&D Program of China (No. 2018YFA0306704), the Fundamental Research Funds for the Central Universities, and the Research Funds of Happiness Flower ECNU (No. 2020ECNU-XFZH005).
  • Guan, Ji: The corresponding author J. G. is supported by the National Key R&D Program of China (No. 2018YFA0306701) and the National Natural Science Foundation of China (No. 61832015).
  • Yu, Nengkun: N. Y. is supported by ARC Discovery Early Career Researcher Award (No. DE180100156) and ARC Discovery Program (No. DP210102449).

References

  1. M. Achatz, S. McCallum, and V. Weispfenning. Deciding polynomial-exponential problems. In Proc. 33rd International Symposium on Symbolic and Algebraic Computation, ISSAC 2008, pages 215-222. ACM Press, 2008. Google Scholar
  2. J. Ax. On Schanuel’s conjectures. Annals of Mathematics, 93(2):252-268, 1971. Google Scholar
  3. A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In Computer Aided Verification: 8th International Conference, CAV'96, volume 1102 of LNCS, pages 269-276. Springer, 1996. Google Scholar
  4. A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model-checking continous-time Markov chains. ACM Transactions on Computational Logic, 1(1):162-170, 2000. Google Scholar
  5. C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(6):524-541, 2003. Google Scholar
  6. C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR'99 Concurrency Theory, volume 1664 of LNCS, pages 146-161. Springer, 1999. Google Scholar
  7. A. Baker. Transcendental Number Theory. Cambridge University Press, 1975. Google Scholar
  8. B. Baumgartner and H. Narnhofer. The structures of state space concerning quantum dynamical semigroups. Reviews in Mathematical Physics, 24(02):article no. 1250001, 2012. Google Scholar
  9. V. Chonev, J. Ouaknine, and J. Worrell. On the Skolem problem for continuous linear dynamical systems. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, volume 55 of LIPIcs, pages 100:1-100:13. Schloss Dagstuhl, 2016. Google Scholar
  10. G. I. Cirillo and F. Ticozzi. Decompositions of Hilbert spaces, stability analysis and convergence probabilities for discrete-time quantum dynamical semigroups. Journal of Physics A: Mathematical and Theoretical, 48(8):article no. 085302, 2015. Google Scholar
  11. H. Cohen. A Course in Computational Algebraic Number Theory. Springer, 1996. Google Scholar
  12. G. E. Collins and R. Loos. Polynomial real root isolation by differentiation. In Proc. SYMSAC 1976, pages 15-25. ACM Press, 1976. Google Scholar
  13. C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk. A Storm is coming: A modern probabilistic model checker. In Computer Aided Verification - 29th International Conference, CAV 2017, Part II, volume 10427 of LNCS, pages 592-600. Springer, 2017. Google Scholar
  14. Y. Feng, E. M. Hahn, A. Turrini, and S. Ying. Model checking ω-regular properties for quantum Markov chains. In 28th International Conference on Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 35:1-35:16. Schloss Dagstuhl, 2017. Google Scholar
  15. Y. Feng, N. Yu, and M. Ying. Model checking quantum Markov chains. Journal of Computer and System Sciences, 79(7):1181-1198, 2013. Google Scholar
  16. S. J. Gay, R. Nagarajan, and N. Papanikolaou. Probabilistic model-checking of quantum protocols. In Proc. 2nd International Workshop on Developments in Computational Models, 2006. available at URL: https://arxiv.org/abs/quant-ph/0504007.
  17. S. J. Gay, R. Nagarajan, and N. Papanikolaou. QMC: A model checker for quantum systems. In Computer Aided Verification, 20th International Conference, CAV 2008, volume 5123 of LNCS, pages 543-547. Springer, 2008. Google Scholar
  18. S. Goldstein, J. L. Lebowitz, R. Tumulka, and N. Zanghì. Long-time behavior of macroscopic quantum systems. The European Physical Journal H, 35(2):173-200, 2010. Google Scholar
  19. V. Gorini, A. Kossakowski, and E. C. G. Sudarshan. Completely positive dynamical semigroups of n-level systems. Journal of Mathematical Physics, 17(5):821-825, 1976. Google Scholar
  20. J. Guan, Y. Feng, A. Turrini, and M. Ying. Model checking applied to quantum physics. CoRR, abs/1902.03218, 2019. URL: http://arxiv.org/abs/1902.03218.
  21. J. Guan, Y. Feng, and M. Ying. Decomposition of quantum Markov chains and its applications. Journal of Computer and System Sciences, 95:55-68, 2018. Google Scholar
  22. J. Guan, Q. Wang, and M. Ying. An HHL-based algorithm for computing hitting probabilities of quantum walks. Quantum Information and Computation, 2021(5&6):0395-0408, 2021. Google Scholar
  23. J. Guan and N. Yu. Verification of continuous-time Markov chains. CoRR, abs/2004.08059, 2020. URL: http://arxiv.org/abs/2004.08059.
  24. E. M. Hahn, Y. Li, S. Schewe, A. Turrini, and L. Zhang. iscasMc: A web-based probabilistic model checker. In FM 2014: Formal Methods - 19th International Symposium, volume 8442 of LNCS, pages 312-317. Springer, 2014. Google Scholar
  25. A. W. Harrow, A. Hassidim, and S. Lloyd. Quantum algorithm for linear systems of equations. Physical Review Letters, 103(15):article no. 150502, 2009. Google Scholar
  26. C.-C. Huang, J.-C. Li, M. Xu, and Z.-B. Li. Positive root isolation for poly-powers by exclusion and differentiation. Journal of Symbol Computation, 85:148-169, 2018. Google Scholar
  27. T. Kailath. Linear Systems. Prentice Hall, 1980. Google Scholar
  28. E. Kaltofen. Polynomial-time reductions from multivariate to bi- and univariate integral polynomial factorization. SIAM Journal on Computing, 14(2):469-489, 1985. Google Scholar
  29. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Computer Aided Verification: 23rd International Conference, CAV 2011, volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  30. L. Li and Y. Feng. Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Information and Computation, 244:229-244, 2015. Google Scholar
  31. G. Lindblad. On the generators of quantum dynamical semigroups. Communications in Mathematical Physics, 48(2):119-130, 1976. Google Scholar
  32. R. Loos. Computing in algebraic extensions. In Computer Algebra: Symbolic and Algebraic Computation, pages 173-187. Springer, 1983. Google Scholar
  33. O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, volume 3253 of LNCS, pages 152-166. Springer, 2004. Google Scholar
  34. M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2000. Google Scholar
  35. C. Pellegrini. Continuous time open quantum random walks and non-Markovian Lindblad master equations. Journal of Statistical Physics, 154:838-865, 2014. Google Scholar
  36. I. Sinayskiy and F. Petruccione. Microscopic derivation of open quantum walks. Physical Review A, 92(3):article no. 032105, 2015. Google Scholar
  37. W. J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994. Google Scholar
  38. A. Strzeboński. Real root isolation for exp-log functions. In Proc. 33rd. International Symposium on Symbolic and Algebraic Computation, ISSAC 2008, pages 303-313. ACM Press, 2008. Google Scholar
  39. A. Strzeboński. Real root isolation for tame elementary functions. In Proc. 34th International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pages 341-350. ACM Press, 2009. Google Scholar
  40. M. M. Wolf. Quantum channels & operations: Guided tour. Lecture notes available at http://www-m5.ma.tum.de/foswiki/pubM, 5, 2012.
  41. M. Xu, C.-C. Huang, and Y. Feng. Measuring the constrained reachability in quantum Markov chains. Acta Informatica, online first, 2021. Google Scholar
  42. M. Xu, L. Zhang, D. N. Jansen, H. Zhu, and Z. Yang. Multiphase until formulas over Markov reward models: An algebraic approach. Theoretical Computer Science, 611:116-135, 2016. Google Scholar
  43. M. Ying and Y. Feng. Model-checking quantum systems. National Science Review, 6(1):28-31, 2019. Google Scholar
  44. M. Ying and Y. Feng. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, 2021. Google Scholar
  45. S. Ying, Y. Feng, N. Yu, and M. Ying. Reachability probabilities of quantum Markov chains. In CONCUR 2013: Concurrency Theory - 24th International Conference, volume 8052 of LNCS, pages 334-348. Springer, 2013. Google Scholar
  46. N. Yu. Quantum temporal logic. CoRR, abs/1908.00158, 2019. URL: http://arxiv.org/abs/1908.00158.
  47. N. Yu and M. Ying. Reachability and termination analysis of concurrent quantum programs. In M. Koutny and I. Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, volume 7454 of LNCS, pages 69-83. Springer, 2012. Google Scholar
  48. L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns. Automata-based CSL model checking. In Automata, Languages and Programming: 38th International Colloquium, ICALP 2011, Part II, volume 6756 of LNCS, pages 271-282. Springer, 2011. Google Scholar
  49. L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns. Efficient CSL model checking using stratification. Logical Methods in Computer Science, 8(2:17):1-18, 2012. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact