JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE) ›› 2015, Vol. 50 ›› Issue (10): 32-39.doi: 10.6040/j.issn.1671-9352.0.2014.401

Previous Articles     Next Articles

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

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

CLC Number: 

  • 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] ZUO Wei-bing. The conditional randomized truth degree of formulas in the fuzzy logic system L* [J]. J4, 2012, 47(6): 121-126.
[2] ZHANG Le, PEI Dao-wu. The conditional truth degree of theory in proposition logic [J]. J4, 2012, 47(2): 82-85.
[3] HU Ming-Di, SHE Yan-Hong, WANG Min. Topological properties of  three-valued   logic  metric space [J]. J4, 2010, 45(6): 86-90.
[4] CUI Mei-hua. The D-conditional truth degree of formulas and approximate reasoning in the  G3 propositional logic system [J]. J4, 2010, 45(11): 52-58.
[5] FU Li. Basic properties of uniform logic formulas and  distribution of their truth degrees [J]. J4, 2010, 45(11): 59-62.
[6] WANG Qing-ping,ZHANG Xing-fang,WANG Da-quan . Stochastic study in the ternary logic system G3 [J]. J4, 2008, 43(2): 101-108 .
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!