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

PDF (PC)

788

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!
Copyright 2018 © Editorial office of JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE)
Supported by Beijing Magtech Co.Ltd