Computer Science ›› 2020, Vol. 47 ›› Issue (10): 309-314.doi: 10.11896/jsjkx.191000175

• Information Security • Previous Articles     Next Articles

Approximate Safety Properties in Metric Linear Temporal Logic

CAI Yong, QIAN Jun-yan, PAN Hai-yu   

  1. Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin,Guangxi 541004,China
  • Received:2019-10-27 Revised:2020-05-08 Online:2020-10-15 Published:2020-10-16
  • About author:CAI Yong,born in 1995,master.His main research interests include formal verification.
    PAN Hai-yu,born in 1976,Ph.D,associate professor,M.S supervisor,is a member of China Computer Federation.His main research interests include formal verification.
  • Supported by:
    National Natural Science Foundation of China (61672023),Natural Science Foundation of Guangxi, China (2018GXNSFAA281326) and Foundation of Guangxi Key Laboratory of Trusted Software (kx201911)

Abstract: In recent years,quantitative verification of computer systems has attracted much attention from the academic and industrial communities,where the study of system specifications over metric spaces has offered a new research line for the development of quantitative verification.In system verification,linear time attribute is often used to describe the properties of the system,and security,as one of the most important basic attributes of linear time attribute,can assert that nothing “bad” happens during execution of systems.Hence the extension of safety properties should also be concerned in the context of metrics.This paper investigates safety properties over pseudo-ultrametric spaces.First,metric linear temporal logic (MLTL) is used to characterize linear-time properties in the context of metrics metrics.Then,this paper lifts the notion of safety properties to pseudo-ultrametric spaces,called α-safety properties,by introducing the distance threshold α.Finally,the relationship between MLTL and α-safety properties is discussed.These results provide a theoretical basis for the verification of safety properties in the context of metrics.

Key words: Linear temporal logic, Linear-time property, Model checking, Pseudo-ultrametric space, Safety property

CLC Number: 

  • TP301
[1] BAIER C,KATOEN J P.Principles of model checking[M].The MIT Press,2008.
[2] MANNA Z,PNUELI A.The temporal logic of reactive and concurrent systems:Specification [M].Springer-verlag,1992.
[3] LIN H M,ZHANG W H.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912.
[4] WANG X B,DUAN Z H.Model checking for temporal logicprograms[J].Computer Science,2009,36(10):164-167.
[5] WANG Z Z.Survey of model checking[J].Computer Science,2013,40(6A):1-14.
[6] HOU G,ZHOU K J,YONG J W,et al.Survey of state explosion problem in model checking [J].Computer Science,2013,40(6A):77-86.
[7] ZHU C Y,CHANG L,XU Z B,et al.Model checking of temporal description logic ALC-LTL based on label Büchi automata[J].Computer Science,2013,40(10):166-171.
[8] BU L,XIE D B.Formal verification of Hybrid system[J].Journal of Software,2014,25(2):219-233.
[9] WANG J,ZHAN N J,FENG X Y,et al.Over-view of formalmethods[J].Journal of Software,2019,30(1):33-61.
[10]ALPERN B,SCHNEIDER F B.Defining liveness[J].Information Processing Letters,1985,21(4):181-185.
[11]ALPERN B,SCHNEIDER F B.Recognizing safety and liveness[J].Distributed Computing,1987,2(3):117-126.
[12]KUPFERMAN O,VARDI M Y.Model checking of safetyproperties[J].Formal Methods in System Design,2001,19(3):291-314.
[13]FARAN R,KUPFERMAN O.Spanning the spectrum fromsafety to liveness[J].Acta Informatica,2018,55(8):703-732.
[14]KUPFERMAN O,VARDI G.On relative and probabilistic finite counterability[J].Formal Methods in System Design,2018,52(2):117-146.
[15]SISTLA A P.Safety,liveness and fairness in temporal logic[J].Formal Aspects of Computing,1994,6(5):495-511.
[16]LI Y M,DROSTE M,LEI L H.Model checking of linear-time properties in multi-valued systems[J].Information Sciences,2017,377:51-74.
[17]LI Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320:17-39.
[18]KATOEN J P,LEI S,ZHANG L.Probably safe or live[C]//Eacsl Conference on Computer Science Logic.2014:1-10.
[19]FAHRENBERG U,LARSEN K G,THRANE C R.A quantitative characterization of weighted Kripke structures in temporal logic [C]//Doctoral Workshop on Mathematical & Engineering Methods in Computer Science.DBLP,2009.
[20]PAN H Y.Lattice-valued quantitative verification of state transition systems[D].Shanghai:East China Normal University,2012.
[21]PAN H Y,LI Y M,CAO Y Z,et al.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262:60-77.
[22]PAN H Y,LI Y M,CAO Y Z,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scien-ce,2016,612(C):45-62.
[23]LIANG C J,LI Y M.Model checking of fuzzy linear temporal logic based on generalized possibility measures[J].Acta Electronica Sinica,2017,45(12):2971-2977.
[24]LIANG C J,LI Y M.The model checking problem of computing tree logic based on generalized possibility measures[J].Acta Electronica Sinica,2017,45(11):2641-2648.
[25]FAN Y H,LI Y M.The realizability of fuzzy linear temporal logic[J].Acta Electronica Sinica,2018,46(2):341-346.
[26]FAN Y H,LI Y M,PAN H Y.Computation tree logic model checking for nondeterminisitc fuzzy Kripke structure[J].Acta Electronica Sinica,2018,46(1):152-159.
[27]LEI L H,WANG J.Parallelization of LTL model checking based on possibility measure [J].Computer Science,2018,45(4):71-75.
[28]ZHU Y,YUAN H J,QIAN J Y,et al.Some notes on fuzzy alternating-time temporal logic [J].Journal of Frontiers of Computer Science and Technology,2018,12(12):2033-2040.
[29]ALFARO L D,FAELLA M,STOELINGA M.Linear andbranching system metrics[J].IEEE Transactions on Software Engineering,2009,35(2):258-273.
[30]CAO Y Z,SUN S X,WANG H Q,et al.A behavioral distance for fuzzy-transition sys-tems[J].IEEE Transactions on Fuzzy Systems,2013,21(4):735-747.
[31]BU T M,WU H Y,CHEN Y X.Computing behavioural distance for fuzzy transition systems[C]//International Symposiumon Theoretical Aspects of Software Engineering.IEEE Computer Society,2017.
[32]CHEN T L,HAN T T,CAO Y Z.Polynomial-time algorithms for computing distances of fuzzy transition systems[J].Theore-tical Computer Science,2018,727:24-36.
[1] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[2] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[3] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[4] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[5] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[6] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[7] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[8] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[9] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[10] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[11] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[12] GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503.
[13] QU Yuan-yuan, HONG Mei and SUN Ning. Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System [J]. Computer Science, 2017, 44(Z11): 542-546.
[14] GUO Zong-hao and WEI Ou. Optimal Control of Probabilistic Boolean Networks Using Model Checking [J]. Computer Science, 2017, 44(5): 193-198.
[15] LIU Bin-bin, LIU Wan-wei, MAO Xiao-guang and DONG Wei. Correctness Verification of Rules for Unmanned Vehicles’ Decision System [J]. Computer Science, 2017, 44(4): 72-74.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!