区间时序逻辑的模型检查

摘要

为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集.这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题.