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

doi:10.6040/j.issn.1671-9352.0.2014.401

山东大学学报（理学版） ›› 2015, Vol. 50 ›› Issue (10): 32-39.doi: 10.6040/j.issn.1671-9352.0.2014.401

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

时慧娴¹, 李永明²

1. 陕西师范大学数学与信息科学学院, 陕西西安 710062;
2. 陕西师范大学计算机科学学院, 陕西西安 710062

收稿日期:2014-09-06 修回日期:2014-12-02 出版日期:2015-10-20 发布日期:2015-10-21
通讯作者: 李永明(1966-),男,博士,教授,研究方向为计算智能、模糊系统分析、量子信息与量子计算.E-mail:liyongm@snnu.edu.cn E-mail:liyongm@snnu.edu.cn
作者简介:时慧娴(1985-),女,博士,讲师,研究方向为不确定性推理、模型检测.E-mail:rubyshi@163.com
基金资助:
国家自然科学基金资助项目(11171200,11271237,11426148);中央高校基本科研业务费专项资金(GK201402006)

Quantitative approach for linear temporal logic based on DTMC

SHI Hui-xian¹, LI Yong-ming²

1. School of Mathematics and Information Science, Shaanxi Normal University, Xi'an 710062, Shaanxi, China;
2. School of Computer Science, Shaanxi Normal University, Xi'an 710062, Shaanxi, China

Received:2014-09-06 Revised:2014-12-02 Online:2015-10-20 Published:2015-10-21

摘要/Abstract

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

关键词: 满足度, 逻辑度量空间, DTMC, 计量逻辑, 线性时序逻辑

Abstract: 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.

Key words: linear temporal logic, DTMC, satisfaction degree, logic metric space, quantitative logic

中图分类号:

O141.1

时慧娴, 李永明. 线性时序逻辑基于DTMC的计量化方法[J]. 山东大学学报（理学版）, 2015, 50(10): 32-39.

SHI Hui-xian, LI Yong-ming. Quantitative approach for linear temporal logic based on DTMC[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2015, 50(10): 32-39.

参考文献

[1] KROGER F, MERZ S. Temporal logic and state systems[M]. Berlin: Springer-Verlag, 2008.
[2] HUTH M, RYAN M. Logic in computer science-modelling and reasoning about systems[M]. 2nd Ed. Cambridge: Cambridge University Press, 2004.
[3] MANNA Z, PNUELI A. Temporal verification of reactive systems[M]. New York: Springer-Verlag, 1995.
[4] CLARKE E M, EMERSON E A. Design and synthesis of synchronisation skeletons using branching time temporal logic[C]. Logics of Programs, LNCS. New York: Springer-Verlag, 1981, 131:52-71.
[5] BAIER C, KATOEN J P. Principles of model checking[M]. London: MIT Press, 2008.
[6] CLARKE E M, GRUMBERG O, PILID D. Model checking[M]. London: MIT Press, 2000.
[7] WANG Guojun, ZHOU Hongjun. Quantitative logic[J]. Information Sciences, 2009, 179:226-247.
[8] WANG Guojun, ZHOU Hongjun. Introduction to mathematical logic and resolution principle[M]. Beijing: Science Press;Oxford: U.K. Alpha Science International Limited, 2009.
[9] 王国俊, 傅丽, 宋建社. 二值命题逻辑中命题的真度理论[J]. 中国科学: 数学, 2001, 31(11):998-1008. WANG Guojun, FU Li, SONG Jianshe. The truth degree theory in two-valued propositional logic[J]. Science in China Mathematics, 2001, 31(11):998-1008.
[10] 王国俊, 李璧镜. ?ukasiwicz n值命题逻辑中公式的真度理论和极限定理[J]. 中国科学: 信息科学, 2005, 35(6):561-569. WANG Guojun, LI Bijing. The truth degree theory in n-valued ?ukasiwicz propositional logic and the limit theorem[J]. Science in China Information Sciences, 2005, 35(6):561-569.
[11] 李骏, 王国俊. 逻辑系统L^*_n中命题的真度理论[J]. 中国科学: 信息科学, 2006, 36(6):631-643. LI Jun, WANG Guojun. The truth degree theory in logic system L^*_n[J]. Science in China Information Sciences, 2006, 36(6):631-643.
[12] 刘华文, 王国俊, 张诚一. 几种逻辑系统中的近似推理理论[J]. 山东大学学报:理学版, 2007, 42(7):77-86. LIU Huawen, WANG Guojun, ZHANG Chengyi. The approximate reasoning theory in several logic systems[J]. Journal of Shandong University: Natural Science, 2007, 42(7):77-86.
[13] LIU Huawen. Notes on triple I method of fuzzy reasoning[J]. Computers and Mathematics with Applications, 2009, 58:1598-1603.
[14] 裴道武, 王国俊. 形式系统L^*的完备性及其应用[J]. 中国科学: 信息科学, 2002, 32(1):56-64. PEI Daowu, WANG Guojun. The completeness of logic system L^* and its application[J]. Science in China Information Sciences, 2002, 32(1):56-64.
[15] SHI Huixian, WANG Guojun. Lattice-valued modal propositional logic and its completeness[J]. Scientia Sinica Informatior, 2010, 53(11):2230-2239.
[16] 时慧娴, 王国俊. 多值模态逻辑的计量化方法[J]. 软件学报, 2012, 23(12):3074-3087. SHI Huixian, WANG Guojun. A quantitative method for multi-value modal logic[J]. Journal of Software, 2012, 23(12):3074-3087.
[17] SHI Huixian, WANG Guojun. Maximal contractions in Boolean algebras[J]. Science China Information Sciences, 2012, 55(9):2044-2055.
[18] 时慧娴. 模态逻辑的计量化研究及其在模型检验中的应用[D]. 西安: 陕西师范大学, 2013. SHI Huixian. Quantitative methods for modal logic and its application in model checking[D]. Xi'an: Shaanxi Normal University, 2013.
[19] 王国俊. 一类一阶逻辑公式中的公理化真度理论及其应用[J]. 中国科学:信息科学, 2012, 42(5):648-662. WANG Guojun. The axiomatic truth degree for a class of first-order logical formulae and its application[J]. Scientia Sinica Information, 2012, 42(5):648-662.
[20] 时慧娴, 王国俊. 基于有限迁移系统的线性时态逻辑的计量化方法[J]. 模糊系统与数学, 2012, 26(5):30-35.SHI Huixian, WANG Guojun. A quantitative method for Linear Temporal Logic based on finite transition systems[J]. Fuzzy Systems and Mathematics, 2012, 26(5):30-35.
[21] 王国俊, 王庆平, 时慧娴,等. 迁移系统关于一类时态逻辑公式的满足度[J]. 陕西师范大学学报:自然科学版, 2013, 41(4):1-10.WANG Guojun, WANG Qingping, SHI Huixian, et al. The satisfaction degree for a class of temporal logical formulae with respect to transition systems[J]. Journal of Shaanxi Normal University: Natural Science, 2013, 41(4):1-10.
[22] BILLINGSLEY P. Probability and measure[M]. USA: Wiley, 1995.
[23] KELLEY J L. General topology[M]. New York: Springer-Verlag, 1975.

多维度评价

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

Quantitative approach for linear temporal logic based on DTMC

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 6

多维度评价

本文评价

推荐阅读 0

[1]	左卫兵. 模糊命题逻辑L*中公式的条件随机真度[J]. J4, 2012, 47(6): 121-126.
[2]	张乐,裴道武. 命题逻辑中理论的条件真度[J]. J4, 2012, 47(2): 82-85.
[3]	胡明娣1,2,折延宏1,王敏3. L₃*系统中逻辑度量空间的拓扑性质[J]. J4, 2010, 45(6): 86-90.
[4]	崔美华. 逻辑系统G₃中命题的D-条件真度与近似推理[J]. J4, 2010, 45(11): 52-58.
[5]	傅丽. 均匀逻辑公式的基本性质及其真度的分布[J]. J4, 2010, 45(11): 59-62.
[6]	王庆平,张兴芳,王大全 . 三值逻辑系统G3中的随机化研究[J]. J4, 2008, 43(2): 101-108 .