多速率混合系统的模型检查

摘要

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质.首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式.接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题.利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题.