您的位置:山东大学 -> 科技期刊社 -> 《山东大学学报(理学版)》

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

• 论文 • 上一篇    下一篇

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

时慧娴1, 李永明2   

  1. 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-xian1, LI Yong-ming2   

  1. 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

摘要: 考虑随机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
[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.
[1] 左卫兵. 模糊命题逻辑L*中公式的条件随机真度[J]. J4, 2012, 47(6): 121-126.
[2] 张乐,裴道武. 命题逻辑中理论的条件真度[J]. J4, 2012, 47(2): 82-85.
[3] 胡明娣1,2,折延宏1,王敏3. L3*系统中逻辑度量空间的拓扑性质[J]. J4, 2010, 45(6): 86-90.
[4] 崔美华. 逻辑系统G3中命题的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 .
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!