基于模糊测度的最大可能性互模拟等价研究

打开文本图片集

中图分类号：TP301 文献标志码：ADOI：10. 13705/j. issn. 1671-6841. 2024144

文章编号：1671-6841（2026）01-0058-07

Abstract： In order to solve the problem of state space explosion in the model checking of complex systems，the fuzzy maximum possibility bisimulation equivalent theory was proposed，and its correlation properties were used to optimize the state space. Firstly，the fuzzy measure and maximum bisimulation equivalence were defined in the fuzzy decision process，and the correlation theorem was proved. Secondly，the definition of the fuzzy bisimulationquotient and the theorem of equal path length and maximum possibility were given. Finally，the syntax and semantics of fuzzy computation tree logic* were given，and the fuzzy maximum possibility bisimulation equivalence properties of fuzzy computation tree logic and fuzzy computation tree logic* were discussed in the fuzzy decision process.

Key words： model checking; fuzzy measure; fuzzy maximum bisimulation； equivalence; fuzzy computation tree logic *

0 引言

模型检测[1-3]是形式化自动验证的重要技术之二[4]，其使用逻辑公式F去描述状态转换系统M 的性质，验证系统是否满足性质的问题可以转换为M是否满足F。（剩余5548字）