Exogenous Quantum Markov Chains and Reachability Analysis
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (11271237, 61228305); Natural Science Foundation of Fujian Province of China (2016J01283); The Young and Middle-Aged Education and Scientific Research Foundation of Fujian Educational Committee(JA13115)

  • Article
  • | |
  • Metrics
  • |
  • Reference [24]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    In order to describe quantum properties of open quantum system, it is necessary to extend the existing quantum Markov chains. In this paper, Exogenous quantum Markov chains is introduced through building Exogenous quantum operator logic. For this new type of quantum Markov chain, the paper focuses on four reachability formulas, gives the solution of their satisfiability problems, and analyzes their decidability problems. As an application, an example is provided to show that the termination of the generalized quantum loop program corresponds to the future reachability of Exogenous quantum Markov chains, and therefore can be decided by checking satisfaction of quantum formulas.

    Reference
    [1] Engesser K, Gabbay DM, Lehmann D. Handbook of Quantum Logic and Quantum Structures:Quantum Logic. Amsteldam:Elsevier Science Ltd., 2009. 1-22.
    [2] Ying MS, Li YJ, Yu NK, Feng Y. Model checking linear time properties of quantum systems. ACM Trans. on Computational Logic, 2014,15(3):Article 22.[doi:10.1145/2629680]
    [3] Feng Y, Yu NK, Ying MS. Model checking quantum Markov chains. Journal of Computer and System Sciences, 2013,79:1181-1198.[doi:10.1016/j.jcss.2013.04.002]
    [4] Ardeshir-Larijani E, Gay SJ, Nagarajan R. Equivalence checking of quantum protocols. In:Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2013. 478-492.[doi:10.1007/978-3-642-36742-7_33]
    [5] Mateus P, Sernadas A. Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation, 2006,204(5):771-794.[doi:10.1016/j.ic.2006.02.001]
    [6] Chadha R, Mateus P, Sernadas A, Sernadas C. Extending classical logic for reasoning about quantum systems. In:Handbook of Quantum Logic and Quantum Structures:Quantum Logic. Amsteldam:Elsevier Science Ltd., 2009. 325-372.
    [7] Baier C, Katoen JP. Principles of Model Checking, Cambridge:MIT Press, 2008. 89-142.
    [8] Clarke EM, Emerson EA. Design and synthesis of synronization skeletons using branching time temporal logic. In:Proc. of the 25 Years of Model Checking. Berlin, Heidelberg:Springer-Verlag, 2008. 196-215.[doi:10.1007/978-3-540-69850-0_12]
    [9] Ying SG, Feng Y, Yu NK, Ying MS. Reachability probabilities of quantum Markov chains. 2013. http://arXiv.org/abs/Quantph/arXiv:\quad1304.0060
    [10] Li YJ, Ying MS. (Un) decidable problems about reachability of quantum systems. 2014. http://arxiv.org/abs/1401.6249
    [11] Feng Y, Yu NK, Ying MS. Reachability analysis of recursive quantum Markov chains. In:Proc. of the Mathematical Foundations of Computer Science. 2013. 385-396.[doi:10.1007/978-3-642-40313-2_35]
    [12] Accardi L. Nonrelativistic quantum mechanics as a noncommutative markov process. Advances in Mathematics, 1976,20:329-366.[doi:10.1016/0001-8708(76)90201-2]
    [13] Accardi L. Topics in quantum probability. Physics Reports, 1981,77(3):169-192.[doi:10.1016/0370-1573(81)90070-3]
    [14] Ohno H. Extendability of generalized quantum Markov chains on gauge invariant C*-algebras. Infinite Dimensional Analysis, Quantum Probability and Related Topics, 2005,8:141-152.[doi:10.1142/S0219025705001901]
    [15] Ambainis A. Quantum walks and their algorithmic applications. Int'l Journal of Quantum Information, 2003,1(4):507-518.[doi:10.1142/S0219749903000383]
    [16] Attal S, Petruccione F, Sabot C, Sinayskiy I. Open quantum random walks. 2014. http://arxiv.org/abs/1402.3253
    [17] Gudder S. Quantum Markov chains. Journal of Mathematical Physics, 2008,49(7):072105.[doi:10.1063/1.2953952]
    [18] Baltazar P, Chadha R, Mateus P. Quantum computation tree logic-model checking and complete calculus. Int'l Journal of Quantum Information, 2008,6(2):219-236.[doi:10.1142/S0219749908003530]
    [19] Akshay S, Antonopoulos T, Ouaknine J, Worrell J. Reachability problems for Markov chains. Information Processing Letters, 2015,115:155-158.[doi:10.1016/j.ipl.2014.08.013]
    [20] Beauquier D, Rabinovich A, Slissenko A. A logic of probability with decidable model checking. In:Proc. of the Computer Science Logic. Berlin, Heidelberg:Springer-Verlag, 2002. 306-321.[doi:10.1007/3-540-45793-3_21]
    [21] Chonev V, Ouaknine J, Worrell J. The orbit problem in higher dimensions. In:Proc. of the 45th Annual ACM Symp. on Theory of Computing. 2013. 941-950.[doi:10.1145/2488608.2488728]
    [22] Chonev V, Ouaknine J, Worrell J. On the complexity of the orbit problem. 2014. http://arxiv.org/abs/1303.2981
    [23] Kannan R, Lipton RJ. Polynomial-Time algorithm for the orbit problem. Journal of the ACM, 1986,33(4):808-821.[doi:10.1145/6490.6496]
    [24] Ying MS, Feng Y. Quantum loop programs. Acta Informatica, 2010,47(4):221-250.[doi:10.1145/6490.6496]
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

林运国,李永明. Exogenous量子马尔可夫链及其可达性分析.软件学报,2016,27(12):2994-3002

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 08,2014
  • Online: November 12,2015
You are the first2049976Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063