安 杰, 张苗苗

(同济大学 软件学院,上海 201804)

文献[7]证明了基于实时自动机的 LDI性质的模型检验问题是可判定的.实时自动机可以看作是一类特殊的时间自动机,即只有一个时钟变量并且每次迁移都会重置该时钟.基于该工作,学术界研究了在比实时自动机表达能力更强的模型(如时间自动机、混成自动机)下LDI公式的模型检验问题[8-12].其中,文献[11,12]提出了一些对于时间自动机下LDI的模型检验的高效算法,并将这些方法扩展到时间自动机网络中[13].

那么对于时段演算是否可以找到一个比 LDI更大的子集,其模型检验问题仍然是可以判定的.一个比较自然的想法是,对 LDI进行扩展,例如,加入布尔连接符和模态词切变(chop),这样就形成扩展线性时段不变式(extended linear duration invariants,简称ELDI).根据文献[6]的结论,在离散时间语义和连续时间语义下,ELDI的可满足性(satisfiability)和正确性(validity)都是不可判定的.Martin等人证明了在离散时间语义和连续时间语义下,对于有限状态机下ELDI的模型检验问题是不可判定的[14].因此,他们提出了ELDI的一个近似语义,并且给出了在该近似语义和离散时间条件下的模型检验算法.由于该算法复杂度过高,在实际系统中很难运用,所以Martin等人提出了另外一种近似语义,并将ELDI的模型检验问题转化为Presburger算术[15].受到该工作的启发,我们证明了在标准离散时间语义下基于时间自动机的ELDI有界模型检验问题是可以判定的,并给出了一种高效的模型检验算法[16].更进一步地,我们讨论了在连续……