欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
考虑随机Kripke模型离散时间马尔可夫链DTMC,并利用DTMC建立线性时序逻辑LTL中公式的满足度理论。首先在DTMC的全体无穷路径之集上引入某种适当的概率测度,考虑任一DTMC D中满足某个LTL公式φ的无穷初始路径占总路径的比例,以此为基础定义D关于公式φ的满足度概念;讨论满足度的若干性质,并指出这一概念体现了DTMC满足某个LTL公式的程度,故可将其作为模型检测理论中＂D满足φ＂这一概念的计量化推广;引入LTL公式之间的相似度,并诱导全体LTL公式之集上的伪度量,从而构建LTL逻辑度量空间。
英文摘要：
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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：