基于有限迁移系统中全体无穷初始路径之集上的某种均匀概率测度,定义迁移系统TS对于LTL公式φ的满足度,并指出该概念是"TS满足φ"这一概念的计量化推广。在满足度理论的基础上,引入LTL公式之间的相似度,并诱导全体LTL公式之集上的伪距离,从而构建LTL逻辑度量空间。
Based on a certain kind of probabilistic measure under the frame of finite transition systems,the present paper proposes the satisfaction degree of 9 with respect to the transitionsystem TS. It is pointed out that this satisfaction degreequantitatively extends the concept of TSar, the classical case. Furthermore, the concept of similarity degree between LTL formulas is introduced, and a correspond pseudo-metric on the set of all LTL formulas is induced,which enables the LTL logic metric space to be constructed.