时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念 ,作为既涉及通讯又具有实时性的并发系统的模型 .该文给出了这种迁移图时间互模拟的算法 。

时间符号迁移图上的可达性分析

提出了以时间符号迁移图为建模语言、基于可达性分析的模型检测算法 ,并给出了算法的正确性证明 .

面向实时传值系统的局部模型检测

为对实时传值系统进行模型检测，本文给出了时间符号迁移图作为系统的建模语言，以及实时谓词μ演算作为刻画性质的逻辑语言。本文给出了基于时间符号迁移图和实时谓词μ演算的一个模型检测算法，该算法动态生成和检测可达的状态空间，并且采用对数据变量on—the—fly实例化以及动态切分时间计值集合的方法，是一个局部算法。该算法不仅能处理基于有限域的变量，还可处理一类数据域无穷的变量(称“数据无关”变量)。