[1] Christe B,Joost P K.Principles of Model Checking[M].Cambridge:The MIT Press,2008.
[2] 林慧民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,36(12A):1907-1912. LIN Hui-min,ZHANG Wen-hui.Model checking:Theories,techniques and applications[J].Acta Electronica Sinica,2002,36(12A):1907-1912.(in Chinese)
[3] Pnueli A.The temporal logic of programs[A].Proceedings of the 18th IEEE Symposium on Foundations of Computer Science[C].USA:IEEE,2017.46-67.
[4] 朱维军,周清雷,李永亮.以DNA为载体的线性时序逻辑模型检测[J].电子学报,2016,44(6):1265-1271. Zhu Wei-jun,Zhou Qing-lei,Li Yong-liang.Conduct linear temporal logic model checking via DNA molecules[J].Acta Electronica Sinica,2016,44(6):1265-1271.(in Chinese)
[5] Glenn B,Patrice G.Model checking with multi-valued modal logic[A].Proceedings of the 31st International Colloquium Automata,Languages and Programming[C].Turku,Finland,2004.281-293.
[6] Marsha C,Benet D,Steve E,Arie G.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(C):371-408.
[7] Yong M Li,Manfred D,Li H L.Model checking of linear-time properties based on multi-valued systems[J].Information Sciences,2017,377:51-74.
[8] Yong M Li,Li J Li.Model checking of linear-time properties based on possibility measures[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[9] Yong M Li,Ya L Li,Zhan Y Ma.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262(C):44-59.
[10] Yong M Li,Zhan Y Ma.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(C):2034-2047.
[11] Li Y M.Quantitative Model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320(C):17-39.
[12] Seong-ick M,Ko-Hsin L,Doheo L.Fuzzy branching temporal logic[J].IEEE Transactions on System,Man and Cybernetics,Part B(Cybernetics),2004,34(2):1045-1055.
[13] Subhankar M,Pallab D.A fuzzy real-time temporal logic[J].International Journal of Approximate Reasoning,2013,54(9):1452-1470.
[14] Pan H Y,Li Y M,Cao Y Z C,Ma Z Y.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262(C):60-77.
[15] Pan H Y,Li Y M,Cao Y Z,Ma Z Y.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scinece,2016,612(C):45-62.
[16] Li Y M.Finite automata theory with membership valued in lattice[J].Information Science,2011,181(C):1003-1017.
[17] Cao Y Z,Yoshinoru E.Nondeterministic fuzzy automata[J].Information Sciences,2012,191(C):86-97.
[18] 李永明,李平.模糊计算理论[M].北京:科学出版社,2016.
[19] 马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学,2016,46(11):1591-1607. MA Zhan-you,LI Yong-ming.Computation tree logic model checking for generalized possibilistic decision processes[J]. Scientia Sinica(Informationis),2016,46(11):1591-1607.(in Chinese)
[20] 郦丽,沈应兄,潘海玉.不确定多值Kripke结构的模型检测[J].模糊系统与数学,2016,30(5):60-70. Li L,Shen Y X,Pan H Y.Nondeterministic multi-valued Kripke structure model checking[J].Fuzzy Systems and Sets,2016,30(5):60-70.(in Chinese)
[21] Lotfi A Z.Fuzzy sets[J].Information and Control,1965,8(C):338-353.
[22] Alfred T.A lattice-theoretical fixpoint theorem and its applications[J].Pacific Journal of Mathematics,1955,5(2):285-309.
[23] Luca D A,Marco F,Thomas A H,et al.Model checking discounted temporal proerties[J].Theoretical Computer Science,2005,345(C):139-170.
[24] Pan H Y,Li Y M,Cao Y Z,et.al.Reachability in fuzzy game graphs[J].IEEE Transactions on Systems,2017,25(4):972-984. |