模糊计算树逻辑的符号模型检测

来源：计算机应用研究杂志2021年第8期北京时间：

作者：聂朋展,姜久雷,马占有,

单位：1.北方民族大学计算机科学与工程学院,银川750021；2.常熟理工学院计算机科学与工程学院,江苏苏州215500；

摘要：对含有模糊不确定性信息的系统进行模型检测时，状态空间爆炸问题成为了亟待解决的主要问题。将形式化的系统模型用拟布尔公式表示，用多终端二叉决策图来对拟布尔公式进行存储。对模糊计算树逻辑的不动点语义给出了解释和证明，然后给出模糊计算树逻辑的符号化模型检测算法，最后通过一个实例验证算法的正确性。该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题，并扩展了模型检测的应用范围。

关键词：模糊计算树逻辑,不动点算法,多终端二叉决策图,符号模型检测,

基金资助：国家自然科学基金资助项目(61762002,61962001)；宁夏自然科学基金资助项目(2018AAC03127)；北方民族大学研究生创新项目(YCX20068)；；