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

• 作者: 时慧娴 李永明
• 来源期刊: 山东大学学报（理学版）
• 学科: 数学
• 关键词: 线性时序逻辑 DTMC 满足度 计量逻辑 逻辑度量空间
• 年，卷（期）: 2015,（10）
• 页码范围: 32-39,46
• 页数: 9页
• 分类号: O141.1
• 字数: 7544字
• 语种: 中文
• DOI: 10.6040/j.issn.1671-9352.0.2014.401

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李永明	陕西师范大学计算机科学学院	165	505	12.0	16.0
2	时慧娴	陕西师范大学数学与信息科学学院	7	21	3.0	4.0