线性时序逻辑基于DTMC的计量化方法

考虑随机Kripke模型离散时间马尔可夫链DTMC,并利用DTMC建立线性时序逻辑LTL中公式的满足度理论。首先在DTMC的全体无穷路径之集上引入某种适当的概率测度,考虑任一DTMC D中满足某个LTL公式φ的无穷初始路径占总路径的比例,以此为基础定义D关于公式φ的满足度概念;讨论满足度的若干性质,并指出这一概念体现了DTMC满足某个LTL公式的程度,故可将其作为模型检测理论中“D满足φ”这一概念的计量化推广;引入LTL公式之间的相似度,并诱导全体LTL公式之集上的伪度量,从而构建LTL逻辑度量空间。

Quantitative approach for linear temporal logic based on DTMC

The present paper aims to construct a quantitative approach for linear temporal logic by means of DTMC, a stochastic Kripke structure efficiently used in model checking. Based on a certain kind of probabilistic measure under the frame of DTMC, we compare the set of infinite initial paths satisfying some LTL formula φ with the set of all infinite initial paths, and consider their ratio to be the satisfaction degree of φ with respect to the DTMC D, as defined in this paper. It is pointed out that this satisfaction degree quantitatively extends the notion of D╞φ, the classical case in model checking. Furthermore, the concept of similarity degree between LTL formulas is presented, and a corresponding pseudo-metric on the set of all LTL formulas is induced, which enables the LTL logic metric space to be constructed.