《表1 检测规则的CTL公式表示示例》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于模型检测的财经舆情可信度研究》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

注：路径（1）中第一条规则的CTL公式语义为从源状态State0开始，对于所有满足Description=objective条件的路径其下一个状态是State1，余下规则以此类推；路径（1）中第三条规则表示以状态State3起始的所有路径上最终会到达状态True。

计算树时序逻辑CTL[33]是一种离散、分支时间逻辑，在模型检测中应用较多。在模型检测中，CTL是一种描述能力非常强的时序逻辑，它用来描述计算树的属性，计算树的根对应于初始状态，树上的其他节点对应于可能的状态转换（路径）序列。利用CTL公式对两类规则进行表示，将不可信舆情的检测规则的最后一个状态设置为!=True，表1为由图3中检测路径转化的检测规则的CTL公式表示示例。