![](https://csdnimg.cn/release/download_crawler_static/88737836/bg4.jpg)
定理
2.4
设
G
= hN
,
Ei
是一个图,
P
是
N
个稳定
w.r.t.
E
. P
在
N
上诱导的等
价关系是
G
上的最大互模拟。
能够通过互模拟来约简图是模型检测中的关键步骤。 互模拟商强保
持
LTL
、
CTL
、
CTL
和整体演算
[8]
。然而,重要的是互模拟计算不是模型
检查过程的重过载
3
相关作品
在显式模型检验领域,待分析系统的模型是通过使用邻接表或其他数据结
构来表示的,其中所有的状态都是分开保存的。另一方面,符号模型检查
背后的哲学是使用最大化信息共享的数据结构。特别是,在符号模型检
查
OBDD
(有序二元决策图)是用来给一个紧凑的表示两个标记的图形
建模的系统和所有的部分计算结果。在
[8]
中可以找到符号技术处理模型
检测中出现的臭名昭著
的状态爆炸
问题的有用性的证据。由于互模拟是在
这种情况下使用,以减少状态空间,重要的是
/
有必要考虑的问题,从一
个明确的和象征性的观点。
就 显 式 情 形 而 言 , 求 解 互 模 拟 问 题 的 第 一 个 重 要 算 法结果是由
Hopcroft
提出的。在
[11]
中,他提出了一个
O
(
jN j log
(
jN j
))算法,用
于最小化
nite-state
自动机的状态数。这个问题等价于确定一个关于函数
集合稳定的集合的粗划分问题。这个问题的一个变体在
[17]
中进行了研
究,其中显示了如何在线性时间内解决它。最后,在
[16]
中,
Paige
和
Tarjan
解决了一般情况下的问题(即,互模拟),其中的稳定性要求是
相对于一个关系
E
(在一个集合
N
)的算法,其复杂性是
O
(
jE j log jN
j
)。
单函数粗剖分问题的线性解的主要特征(参见
[17])
是在搜索粗糙分
区时使用
积极
策略:起始分区是具有单例类的分区,并且输出是通过一
系列步骤构建的,其中两个或更多个类被合并。相反,
Hopcroft
对(更
困难的)许多函数粗划分问题的解决方案和
Paige
和
Tarjan
互模拟算法都
基于(更自然的)
负
策略。起始分区是输入分区,在每一步中,不满足
稳定性条件的类被拆分。
[11]
和
[16]
中的过程的吸引人的复杂性结果来
自于对处理类的巧妙排序(所谓
的处理最小一半
策略)的使用。