Document Open Access Logo

Model Checking Omega-regular Properties for Quantum Markov Chains

Authors Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Shenggang Ying

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.35.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Yuan Feng
Ernst Moritz Hahn
Andrea Turrini
Shenggang Ying

Cite AsGet BibTex

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.35

Abstract

Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.
Keywords
  • Quantum Markov chains
  • model checking
  • omega-regular properties
  • bottom strongly connected component

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ebrahim Ardeshir-Larijani, Simon J. Gay, and Rajagopal Nagarajan. Equivalence checking of quantum protocols. In TACAS, volume 7795 of LNCS, pages 478-492, 2013. Google Scholar
  2. Ebrahim Ardeshir-Larijani, Simon J. Gay, and Rajagopal Nagarajan. Verification of concurrent quantum protocols by equivalence checking. In TACAS, volume 8413 of LNCS, pages 500-514, 2014. Google Scholar
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  4. Bernhard Baumgartner and Heide Narnhofer. The structures of state space concerning Quantum Dynamical Semigroups. Reviews in Mathematical Physics, 24(02):1250001, 2012. Google Scholar
  5. Charles H. Bennett. Quantum cryptography using any two nonorthogonal states. Physical Review Letters, 68:3121, 1992. Google Scholar
  6. Charles H. Bennett and Gilles Brassard. Quantum cryptography: Public-key distribution and coin tossing. In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, pages 175-179, 1984. Google Scholar
  7. Charles H. Bennett and Stephen J. Wiesner. Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Physical Review Letters, 69(20):2881-2884, 1992. Google Scholar
  8. Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, and Marco Roveri. Spacecraft early design validation using formal methods. Reliability Engineering and System Safety, 132:20-35, 2014. Google Scholar
  9. Doron Bustan, Sasha Rubin, and Moshe Y Vardi. Verifying omega-regular properties of Markov chains. In CAV, volume 4, pages 189-201, 2004. Google Scholar
  10. Taolue Chen, Marco Diciolla, Marta Kwiatkowska, and Alexandru Mereacre. Quantitative verification of implantable cardiac pacemakers. In Real-Time Systems Symposium, pages 263-272, 2012. Google Scholar
  11. Edmund M Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT press, 1999. Google Scholar
  12. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. JACM, 42(4):857-907, 1995. Google Scholar
  13. Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997. Google Scholar
  14. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In FOCS, SFCS, pages 368-377. IEEE CS, 1991. Google Scholar
  15. Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Lijun Zhang. QPMC: A model checker for quantum programs and protocols. In FM'15, volume 9109 of Lecture Notes in Computer Science, pages 265-272. Springer, 2015. Google Scholar
  16. Yuan Feng, Nengkun Yu, and Mingsheng Ying. Model checking quantum Markov chains. Journal of Computer and System Sciences, 79(7):1181-1198, 2013. Google Scholar
  17. Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. Probabilistic model-checking of quantum protocols. In Proceedings of the 2nd International Workshop on Developments in Computational Models, 2006. Google Scholar
  18. Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: A model checker for quantum systems. In CAV 08, pages 543-547. Springer, 2008. Google Scholar
  19. Stanley Gudder. Quantum Markov chains. Journal of Mathematical Physics, 49(7):072105, 14, 2008. Google Scholar
  20. Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. IscasMC: A web-based probabilistic model checker. In FM'14, volume 8442 of Lecture Notes in Computer Science, pages 312-317. Springer, 2014. Google Scholar
  21. Khaza Anuarul Hoque, Otmane Aït Mohamed, and Yvon Savaria. Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In Design, Automation & Test in Europe, pages 1635-1640, 2015. Google Scholar
  22. Lvzhou Li and Yuan 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
  23. Andrzej Wlodzimierz Mostowski. Regular expressions for infinite trees and a standard form of automata. In Computation Theory, volume 208 of LNCS, pages 157-168. Springer, 1984. Google Scholar
  24. Michael A. Nielsen and Isaac L. Chuang. Quantum computation and quantum information. Cambridge university press, 2000. Google Scholar
  25. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. JLMCS, 3(3:5), 2007. Google Scholar
  26. Shmuel Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. Google Scholar
  27. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In FoSSaCS, volume 5504 of LNCS, pages 167-181, 2009. Google Scholar
  28. Peter Selinger. A brief survey of quantum programming languages. Functional and Logic Programming, 2998:1-6, 2004. Google Scholar
  29. Wolfgang Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B), pages 133-191. MIT Press, Cambridge, MA, USA, 1990. Google Scholar
  30. Michael M Wolf. Quantum channels &operations: Guided tour. https://www-m5.ma.tum.de/foswiki/pub/M5/Allgemeines/MichaelWolf/QChannelLecture.pdf, 2012. Google Scholar
  31. Mingsheng Ying, Yangjia Li, Nengkun Yu, and Yuan Feng. Model-checking linear-time properties of quantum systems. ACM Transactions on Computational Logic (TOCL), 15(3):22, 2014. Google Scholar
  32. Shenggang Ying, Yuan Feng, Nengkun Yu, and Mingsheng Ying. Reachability probabilities of quantum markov chains. In CONCUR'13, pages 334-348. Springer, 2013. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact