logo

SCIENTIA SINICA Informationis, Volume 46, Issue 11: 1591-1607(2016) https://doi.org/10.1360/N112016-00108

Model checking generalized possibilistic computation tree logic based on decision processes

More info
  • ReceivedApr 24, 2016
  • AcceptedAug 2, 2016
  • PublishedNov 9, 2016

Abstract

We study model-checking generalized possibilistic computation tree logic (GPoCTL) and its application in system verification, in particular, nondeterministic systems. Firstly, we introduce generalized possibilistic decision-making processes (GPDP) as system models and GPoCTL formulae under GPDP to describe the properties of the system. Then, we provide a model-checking algorithm for GPoCTL. The main advantage of the algorithm is that it can use scheduling in the decision making processes to convert the model-checking problem into operations of the fuzzy matrix or fixed point of fuzzy matrix functions, which need polynomial time. Finally, an example is given to illustrate the application of the model-checking generalized possibilistic computation tree logic in verification of a nondeterministic system.


Funded by

国家自然科学基金(11271237)

国家自然科学基金(61228305)

国家自然科学基金(61462001)

高等学校博士学科点专项科研基金(20130202110001)

高等学校博士学科点专项科研基金(20130202120002)


References

[1] Baier C, Katoen J P. Principles of Model Checking. Cambridge: MIT Press, 2008. Google Scholar

[2] Edmund M, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 1999. Google Scholar

[3] Zheng Y, Wang L. Consensus of switched multi-agent systems. IEEE Trans Circ Syst II, 2016, 63: 314-318. Google Scholar

[4] Zheng Y, Wang L. A novel group consensus protocol for heterogeneous multi-agent systems. Int J Contr, 2015, 106: 1-13. Google Scholar

[5] Li T, Zhang J F. Consensus conditions of multi-agent systems with time-varying topologies and stochastic communication noises. IEEE Trans Automat Contr, 2010, 55: 2043-2057 CrossRef Google Scholar

[6] Li T, Fu M, Xie L, et al. Distributed consensus with limited communication data rate. IEEE Trans Automat Contr, 2011, 56: 279-292 CrossRef Google Scholar

[7] Baier C, Kwiatkowska M. Model checking for a probabilistic branching time logic with fairness. Distrib Comput, 1998, 11: 125-155 CrossRef Google Scholar

[8] Hart S, Sharir M. Termination of probabilistic concurrent programs. ACM Trans Prog Lang Syst, 1983, 5: 356-380 CrossRef Google Scholar

[9] Sultan K, Bentahar J, Wei W, et al. Modeling and verifying probabilistic multi-agent systems using knowledge and social commitments. Expert Syst Appl, 2014, 41: 6291-6304 CrossRef Google Scholar

[10] Sultan K, Bentahar J, EI-Menshawy M. Model checking probabilistic social commitments for intelligent agent communication. Appl Softw Comput, 2014, 22: 397-409 CrossRef Google Scholar

[11] Chechik M, Devereux B, Easterbrook S, et al. Multi-valued symbolic model-checking. ACM Trans Softw Eng Method, 2003, 12: 371-408 CrossRef Google Scholar

[12] Chechik M, Gurfinkel A, Devereux B, et al. Data structures for symbolic multi-valued model-checking. Formal Methods Syst Des, 2006, 29: 295-344 CrossRef Google Scholar

[13] Pan H Y, Li Y M, Cao Y Z, et al. Model checking fuzzy computation tree logic. Fuzzy Sets Syst, 2015, 262: 60-77 CrossRef Google Scholar

[14] Pan H Y, Li Y M, Cao Y Z, et al. Model checking computation tree logic over finite lattices. Theor Comput Sci, 2016, 612: 45-62 CrossRef Google Scholar

[15] Li Y M, Li L J. Model checking of linear-time properties based on possibility measure. IEEE Trans Fuzzy Syst, 2013, 21: 842-854 CrossRef Google Scholar

[16] Li Y M, Li Y L, Ma Z Y. Computation tree logic model checking based on possibility measures. Fuzzy Sets Syst, 2015, 262: 44-59 CrossRef Google Scholar

[17] Li Y M, Ma Z Y. Quantitative computation tree logic model checking based on generalized possibility measures. IEEE Trans Fuzzy Syst, 2015, 23: 2034-2047 CrossRef Google Scholar

[18] Drakopoulos A. Probabilities, possibilities, and fuzzy sets. Fuzzy Sets Syst, 1995, 75: 1-15 CrossRef Google Scholar

[19] Dubois D. Possibility theory and statistical reasoning. Comput Stat Data Anal, 2006, 51: 47-69 CrossRef Google Scholar

[20] Dubois D, Prade H. Possibility Theory. NewYork: Plenum, 1988. Google Scholar

[21] Dubois D, Prade H. Possibility theory, probability theory and multiple-valued logics: a clarification. Ann Math Artif Intell, 2001, 32: 35-66 CrossRef Google Scholar

[22] Grabisch M, Murofushi T, Sugeno M. Fuzzy Measures and Integrals. Heidelberg: Physica-Verlag, 2000. Google Scholar

[23] Zadeh L A. Fuzzy sets as a basis for a theory of possibility. Fuzzy Sets Syst, 1978, 1: 3-28 CrossRef Google Scholar

[24] Li Y M. Analysis of Fuzzy Systems. Beijing: Science Press, 2005 [李永明. 模糊系统分析. 北京: 科学出版社, 2005]. Google Scholar

[25] Garmendia L, Gonz$\acute{a}$lez del Campo R, López V, et al. An algorithm to compute the transitive closure, a transitive approximation and a transitive opening of a fuzzy proximity. Mathware Soft Comput, 2009, 16: 175-191. Google Scholar

[26] Lin F, Ying H. Modeling and control of fuzzy discrete event systems. IEEE Trans Syst Man Cybernetics Part B, 2002, 32: 408-415 CrossRef Google Scholar

[27] Qiu D. Supervisory control of fuzzy discrete event systems: a formal approach. IEEE Trans Syst Man Cybern Part B, 2005, 35: 72-88 CrossRef Google Scholar

[28] Cao Y, Ying M. Observability and decentralized control of fuzzy discrete-event systems. IEEE Trans Fuzzy Syst, 2006, 14: 202-216 CrossRef Google Scholar

[29] Liu F C, Qiu D W. Diagnosability of fuzzy discrete event systems: a fuzzy approach. IEEE Trans Fuzzy Syst, 2009, 17: 372-384 CrossRef Google Scholar

[30] Xing H Y, Zhang Q S, Huang K S. Analysis and control of fuzzy discrete event systems using bisimulation equivalence. Theor Comput Sci, 2012, 456: 100-111 CrossRef Google Scholar

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1       京公网安备11010102003388号