Volume 33 Issue 6
Nov.  2024
Turn off MathJax
Article Contents
Wuniu LIU, Junmei WANG, Qing HE, et al., “Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques,” Chinese Journal of Electronics, vol. 33, no. 6, pp. 1399–1411, 2024 doi: 10.23919/cje.2021.00.333
Citation: Wuniu LIU, Junmei WANG, Qing HE, et al., “Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques,” Chinese Journal of Electronics, vol. 33, no. 6, pp. 1399–1411, 2024 doi: 10.23919/cje.2021.00.333

Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques

doi: 10.23919/cje.2021.00.333
More Information
  • Author Bio:

    Wuniu LIU was born in Shaanxi Province, China, in 1997. He received the M.S. degree in computer science and technology in 2022 from the School of Computer Science, Shaanxi Normal University, Xi’an, China, where he is currently a Ph.D. candidate in applied mathematics with the School of Mathematics and Statistics. He has published some papers in academic journals such as IEEE Transactions on Systems, Man, and Cybernetics: Systems, IEEE Transactions on Emerging Topics in Computational Intelligence and IEEE Transactions Fuzzy Systems. His research interests include computational intelligence, fuzzy logic, control theory and quantum computation. (Email: liuwuniu@snnu.edu.cn)

    Junmei WANG was born in 1995. She received the M.S. degree from the School of Computer Science of Shaanxi Normal University, Xi’an, China, in 2022. She is now a Researcher at Xi’an BYD Auto Company Limited, Xi’an, China. Her research interests include formal methods and model checking. (Email: wangjunmei@snnu.edu.cn)

    Qing HE was born in Shaanxi Province, China, in 1998. She received the B.S. degree in computer science and technology in 2020 from the School of Computer Science, Shaanxi Normal University, Xi’an, China, where she is currently a Ph.D. candidate in computer science and technology. Her research interests include model checking and fuzzy temporal logic. (Email: heqing@snnu.edu.cn)

    Yongming LI received the Ph.D. degree in mathematics from Sichuan University, Chengdu, China, in 1996. He is currently with Shaanxi Normal University, Xi’an, China, as a Professor of mathematics and computer science. He authored or coauthored more than 300 journal articles in several IEEE transactions and other high impact journals. He serves as a member of Fuzzy Systems Technical Committee in IEEE Computational Intelligence Society, deputy director of the Fuzzy Mathematics and Fuzzy Systems Committee of the Chinese Society for Systems Engineering, vice chairman of the Intelligent Computing Society of the National Operational Research Society, vice chairman of the Computer Education Committee of the National Normal University, director of the Theoretical Computer Society of the Chinese Computer Society, executive director of the Shaanxi Computer Society, and executive committee member of the CCF (Chinese Computer Society) Xi’an branch. His research interests include model checking, fuzzy control theory, fuzzy automata theory, spatial reasoning, quantum logic and quantum computation, and topology over lattices. (Email: liyongm@snnu.edu.cn)

  • Corresponding author: Email: liyongm@snnu.edu.cn
  • Received Date: 2021-09-06
  • Accepted Date: 2023-12-08
  • Available Online: 2024-02-02
  • Publish Date: 2024-11-05
  • Model checking computation tree logic based on multi-valued possibility measures has been studied by Li et al. on Information Sciences in 2019. However, the previous work did not consider the nondeterministic choices inherent in systems represented by multi-valued Kripke structures (MvKSs). This nondeterminism is crucial for accurate system modeling, decision making, and control capabilities. To address this limitation, we draw inspiration from the generalization of Markov chains to Markov decision processes in probabilistic systems. By integrating nondeterminism into MvKS, we introduce multi-valued decision processes (MvDPs) as a framework for modeling MvKSs with nondeterministic choices. We investigate the problems of model checking over MvDPs. Verifying properties are expressed by using multi-valued computation tree logic based on schedulers. Our primary objective is to leverage fixpoint techniques to determine the maximum and minimum possibilities of the system satisfying temporal properties. This allows us to identify the optimal or worst-case schedulers for decision making or control purposes. We aim to develop reduction techniques that enhance the efficiency of model checking, thereby reducing the associated time complexity. We mathematically demonstrate three reduction techniques that improve model checking performance in most scenarios.
  • loading
  • [1]
    C. Baier and J. P. Katoen, Principles of Model Checking. MIT Press, Cambridge, MA, USA, 2008.
    [2]
    M. Huth and M. Kwiatkowska, “Quantitative analysis and model checking,” in Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, pp. 111–122, 1997.
    [3]
    Y. M. Li and Z. Y. Ma, “Quantitative computation tree logic model checking based on generalized possibility measures,” IEEE Transactions on Fuzzy Systems, vol. 23, no. 6, pp. 2034–2047, 2015. doi: 10.1109/TFUZZ.2015.2396537
    [4]
    H. Y. Pan, Y. M. Li, Y. Z. Cao, et al., “Model checking fuzzy computation tree logic,” Fuzzy Sets and Systems, vol. 262, pp. 60–77, 2015. doi: 10.1016/j.fss.2014.07.008
    [5]
    Y. M. Li, “Quantitative model checking of linear-time properties based on generalized possibility measures,” Fuzzy Sets and Systems, vol. 320, pp. 17–39, 2017. doi: 10.1016/j.fss.2017.03.012
    [6]
    Y. M. Li, L. H. Lei, and S. J. Li, “Computation tree logic model checking based on multi-valued possibility measures,” Information Sciences, vol. 485, pp. 87–113, 2019. doi: 10.1016/j.ins.2019.02.003
    [7]
    Y. M. Li and J. L. Wei, “Possibilistic fuzzy linear temporal logic and its model checking,” IEEE Transactions on Fuzzy Systems, vol. 29, no. 7, pp. 1899–1913, 2021. doi: 10.1109/TFUZZ.2020.2988848
    [8]
    W. N. Liu, Q. He, and Y. M. Li, “Computation tree logic model checking over possibilistic decision processes under finite-memory scheduler,” in Proceedings of the 39th National Conference of Theoretical Computer Science, Yinchuan, China, pp. 75–88, 2021.
    [9]
    W. N. Liu, Z. H. Li, and Y. M. Li, “Complex objective optimization in fuzzy environments,” Journal of Intelligent & Fuzzy Systems, vol. 45, no. 2, pp. 3539–3553, 2023. doi: 10.3233/JIFS-221966
    [10]
    W. N. Liu and Y. M. Li, “Optimal strategy model checking in possibilistic decision processes,” IEEE Transactions on Systems, Man, and Cybernetics: Systems, vol. 53, no. 10, pp. 6620–6632, 2023. doi: 10.1109/TSMC.2023.3286127
    [11]
    W. N. Liu, Q. He, Z. H. Li, et al., “Self-learning modeling in possibilistic model checking,” IEEE Transactions on Emerging Topics in Computational Intelligence, vol. 8, no. 1, pp. 264-278, 2024.
    [12]
    Y. M. Li, W. N. Liu, J. M. Wang, et al., “Model checking of possibilistic linear-time properties based on generalized possibilistic decision processes,” IEEE Transactions on Fuzzy Systems, vol. 31, no. 10, pp. 3495–3506, 2023. doi: 10.1109/TFUZZ.2023.3260446
    [13]
    M. Chechik, “On interpreting results of model-checking with abstraction,” CSRG technical report 417, University of Toronto, Department of Computer Science, Canada, 2000.
    [14]
    M. Chechik, B. Devereux, S. Easterbrook, et al., “Multi-valued symbolic model-checking,” ACM Transactions on Software Engineering and Methodology, vol. 12, no. 4, pp. 371–408, 2003. doi: 10.1145/990010.990011
    [15]
    M. Chechik, S. Easterbrook, and V. Petrovykh, “Model-checking over multi-valued logics,” in Proceedings of the International Symposium of Formal Methods Europe, Berlin, Germany, pp. 72–98, 2001.
    [16]
    M. Chechik, A. Gurfinkel, B. Devereux, et al., “Data structures for symbolic multi-valued model-checking,” Formal Methods in System Design, vol. 29, no. 3, pp. 295–344, 2006. doi: 10.1007/s10703-006-0016-z
    [17]
    S. Hazelhurst, “Compositional model checking of partially ordered state spaces,” Ph.D. Thesis, University of British Columbia, Vancouver, Canada, 1996.
    [18]
    Y. Z. Cao and M. S. Ying, “Observability and decentralized control of fuzzy discrete-event systems,” IEEE Transactions on Fuzzy Systems, vol. 14, no. 2, pp. 202–216, 2006. doi: 10.1109/TFUZZ.2005.864085
    [19]
    W. L. Deng and D. W. Qiu, “Bifuzzy discrete event systems and their supervisory control theory,” IEEE Transactions on Fuzzy Systems, vol. 23, no. 6, pp. 2107–2121, 2015. doi: 10.1109/TFUZZ.2015.2403866
    [20]
    F. Lin and H. Ying, “Modeling and control of fuzzy discrete event systems,” IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), vol. 32, no. 4, pp. 408–415, 2002. doi: 10.1109/TSMCB.2002.1018761
    [21]
    D. W. Qiu, “Supervisory control of fuzzy discrete event systems: A formal approach,” IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), vol. 35, no. 1, pp. 72–88, 2005. doi: 10.1109/TSMCB.2004.840457
    [22]
    L. A. Zadeh, “Fuzzy sets,” Information and Control, vol. 8, no. 3, pp. 338–353, 1965. doi: 10.1016/S0019-9958(65)90241-X
    [23]
    L. A. Zadeh, “Fuzzy sets as a basis for a theory of possibility,” Fuzzy Sets and Systems, vol. 1, no. 1, pp. 3–28, 1978. doi: 10.1016/0165-0114(78)90029-5
    [24]
    D. Dubois, “Possibility theory and statistical reasoning,” Computational Statistics & Data Analysis, vol. 51, no. 1, pp. 47–69, 2006. doi: 10.1016/j.csda.2006.04.015
    [25]
    D. Dubois and H. Prade, “Possibility theory, probability theory and multiple-valued logics: A clarification,” Annals of Mathematics and Artificial Intelligence, vol. 32, no. 1, pp. 35–66, 2001. doi: 10.1023/A:1016740830286
    [26]
    D. Dubois and H. Prade, “Possibility theory and its applications: Where do we stand?” in Springer Handbook of Computational Intelligence, J. Kacprzyk and W. Pedrycz, Eds. Springer, Berlin, Heidelberg, Germany, pp. 31–60, 2015.
    [27]
    D. Dubois, F. Dupin de Saint-Cyr, and H. Prade, “Update postulates without inertia,” in European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, Fribourg, Switzerland, pp. 162–170, 1995.
    [28]
    Y. M. Li, Analysis of Fuzzy Systems. Science Press, Beijing, China, 2005. (in Chinese)
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(3)  / Tables(1)

    Article Metrics

    Article views (677) PDF downloads(31) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return