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

LIU Wuniu; WANG Junmei; HE Qing; LI Yongming

doi:10.23919/cje.2021.00.333

Article Contents

Article Navigation > Chinese Journal of Electronics > 2024 > Accepted Manuscript

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. x, no. x, pp. 1–13, xxxx 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. x, no. x, pp. 1–13, xxxx doi: 10.23919/cje.2021.00.333

Citation:

PDF( 7873 KB)

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

doi: 10.23919/cje.2021.00.333

LIU Wuniu^{1, 2
,},
WANG Junmei^2
,,
HE Qing^2
,,
LI Yongming^{1, 2
,
,}

1.
The School of Mathematics and Statistics, Shaanxi Normal University, Xi’an 710119, China
2.
The School of Computer Science, Shaanxi Normal University, Xi’an 710119, China

More Information

Author Bio:
Wuniu LIU was born in Yulin, Shaanxi, China, in 1997. He received the M.Sc. degree in computer science and technology in 2022 from the School of Computer Science, Shaanxi Normal University, Xi’an, China, where he is currently working toward the doctoral degree in applied mathematics from 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 master’s degree from the School of Computer Science of Shaanxi Normal University, in 2022. She is now a researcher at Xi'an BYD Auto Company Limited. Her research interests include formal methods, model checking. (Email: wangjunmei@snnu.edu.cn)

Qing HE was born in Xi’an, Shaanxi, 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 working toward the doctoral degree in computer science and technology with the School of Computer Science. 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

Abstract

Abstract

Model checking computation tree logic (CTL) based on multi-valued possibility measures has been studied by Li et al. 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 (MCs) to Markov decision processes (MDPs) in probabilistic systems. By integrating nondeterminism into MvKS, we introduce multi-valued decision processes (MvDPs) as a framework for modeling MvKSs with nondeterministic choices. Additionally, we investigate the challenges of model checking over MvDPs. In our approach, verifying properties are expressed by using multi-valued computation tree logic (MvCTL) 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. Furthermore, we aim to develop reduction techniques that enhance the efficiency of model checking, thereby reducing the associated time complexity.
- Multi-valued decision processes (MvDPs),
- Multi-valued computation tree logic (MvCTL),
- Scheduler,
- Reduction techniques and Model checking

FullText(HTML)

References(28)

References

[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, in press, 2023.
[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,” in press, 2000. (查阅网上资料, 请核对文献类型及格式) . M. Chechik, “On interpreting results of model-checking with abstraction,” in press, 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) (查阅网上资料, 未找到对应的英文翻译, 请确认) . Y. M. Li, Analysis of Fuzzy Systems. Science Press, Beijing, China, 2005. (in Chinese) (查阅网上资料, 未找到对应的英文翻译, 请确认).