Computer Science ›› 2021, Vol. 48 ›› Issue (4): 31-36.doi: 10.11896/jsjkx.200500036

• Computer Science Theory • Previous Articles     Next Articles

Fuzzy Safety and Liveness Properties

SHI Tie-zhu, QIAN Jun-yan, PAN Hai-yu   

  1. Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin,Guangxi 541004,China
  • Received:2020-06-24 Revised:2020-08-16 Online:2021-04-15 Published:2021-04-09
  • About author:SHI Tie-zhu,born in 1995,master.His main research interests include formal verification and so on.(tiezhus86@163.com)
    PAN Hai-yu,born in 1976,Ph.D,asso-ciate professor,M.S supervisor,is a member of China Computer Federation.His main research interests include formal verification and so on.
  • Supported by:
    National Natural Science Foundation of China(61672023),Natural Science Foundation of Guangxi(2018GXNSFAA281326) and Foundation of Guangxi Key Laboratory of Trusted Software(kx201911).

Abstract: Formal specification is to construct specification of the developed software and hardware systems by using formal language and describes their models and properties.Among which,the specification of properties which includes the specification of branching-time properties,plays an important role in verification of systems.In the classical setting,the specification of properties is based on two-valued logic,and hence cannot describe the inconsistent or uncertain information.Consequently,extending the specification languages of properties to the fuzzy setting helps to verify the fuzzy systems.In this paper,first,a formal definition of branching-time properties,especially the safety and liveness properties in the fuzzy setting,is given.Then,two types of closure operations are defined,resulting in 4 types of properties which are universal safety,universal liveness,existential safety,and existential liveness.Finally,it is shown that any branching-time property is the intersection between an existential safety property and an existential liveness property,or a universal safety property and a universal liveness property,or an existential safety property and a universal liveness property.

Key words: Branching-time properties, Formal specification, Fuzzy logic, Liveness properties, Safety properties

CLC Number: 

  • TP301
[1]WANG J,ZHAN N J,FENG X Y,et al.Overview of formal methods[J].Journal of Software,2019,30(1):33-61.
[2]BAIER C,KATOEN J P.Principles of model checking[M].Cambridge,MA: The MIT Press,2008.
[3]LIN H M,ZHANG W H.Model checking: theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912.
[4]WANG Z Z.Survey of Model Checking[J].Computer Science,2013,40(Z6):1-14.
[5]WEI O,SHI Y F,XU B F,et al.Abstract Modeling Formalisms in Software Model Checking[J].Journal of Computer Research and Development,2015,52(7):1580-1603.
[6]HAN Y J,ZHOU Q L,ZHU W J.Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking[J].Computer Science,2019,46(11):25-31.
[7]LIU Y,LI X D,MA Y.Model abstraction for stochastic modelchecking[J].Journal of Software,2015,26(8):1853-1870.
[8]LIU Y,LI X D,MA Y,et al.Survey for Stochastic Model Checking[J].Chinese Jour-nal of Computers,2015,38(11):2145-2162.
[9]CHECHIK M,DEVEREUX B,EASTERBRO-OK S,et al.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.
[10]LI Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320:17-39.
[11]DENG H,XUE Y,LI Y L,et al.Computation Tree Logic CTL*Based on Possibility Measure and Possibilistic Bisimulation[J].Computer Science,2012,39(10):258-263.
[12]LEI L H,WANG J.Parallelization of LTL model checking based on possibility measure [J].Computer Science,2018,45(4):71-75.
[13]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.
[14]PAN H Y,LI Y M,CAO Y Z,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scie-nce,2016,612(C):45-62.
[15]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.
[16]FARAN R,KUPFERMAN O.Spanning the spectrum fromsafety to liveness[J].Acta Informatica,2018,55(8):703-732.
[17]ALPERN B,DEMERS A J,SCHNEIDER F B.Safety without stuttering[J].Information Proce-ssing Letters,1986,23(4):177-180.
[18]KUPFERMAN O,VARDI M Y.Model checking of safetyproperties[J].Formal Methods in System Design,2001,19(3):291-314.
[19]LAMPORT L.Proving the Correctness of Multip-rocess Pro-grams[J].IEEE Transactions on Software Engineering,1977,SE-3(2):125-143.
[20]ALPERN B,SCHNEIDER F B.Defining liveness[J].Information Processing Letters,1985,21(4):181-185.
[21]ALPERN B,SCHNEIDER F B.Recognizing safety and liveness[J].Distributed Computing,1987,2(3):117-126.
[22]SISTLA A P.Safety,liveness and fairness in temporal logic[J].Formal Aspects of Computing,1994,6(5):495-511.
[23]LI Y M,DROSTE M,LEI L H.Model checkin-g of linear-time properties in multi-valued systems[J].Information Sciences,2017,377:51-74.
[24]MANOLIOS P,TTEFLER R.Safety and liven-ess in branching time[C]//In LICS.IEEE Computer Society,2001:366-374.
[25]BOUAJJANI A,FERNANDEZ J C.Safety for branching time semantics[C]//18th ICALP.LNCS 510,1991:76-92.
[26]KATOEN J P,LEI S,ZHANG L.Probably safe or live[C]//Eacsl Conference on Computer Science Logic.2014:1-10.
[27]ZHANG X H,WU D P,DAI J H.Fuzzy Mathematics andRough Set Theory[M].Beijing: Tsinghua University Press,2012.
[28]MANTACI S,RESTIVO A.Codes and equations on trees [J].Theoretical Computer Science,2001,255(1/2):483-509.
[1] XI Xin-xing, LUO Xiao-qing, ZHANG Zhan-cheng. Multi-modal Medical Volumetric Image Fusion Based on 3-D Shearlet Transform
and Generalized Gaussian Model
[J]. Computer Science, 2019, 46(5): 254-259.
[2] LUO Xu-dong, HUANG Qiao-juan, ZHAN Jie-yu. A Survey of Automated Negotiation and Its Fuzzy Set Based Models [J]. Computer Science, 2019, 46(12): 220-230.
[3] YANG Lu, YU Shou-wen and YAN Jian-feng. Type-2 Fuzzy Logic Based Multi-threaded Data Race Detection [J]. Computer Science, 2017, 44(12): 135-143.
[4] LUO Pin-jie, WEN He and WAN Li. Research on Bus Arrival Time Prediction Model Based on Fuzzy Neural Network with Genetic Algorithm [J]. Computer Science, 2016, 43(Z6): 87-89.
[5] MA Xiao-xin and ZENG Guo-sun. Scheme of Automated Trust Negotiation Based on Fuzzy Logic [J]. Computer Science, 2015, 42(12): 220-223.
[6] WANG Wan-liang, SHI Hao and LI Yan-jun. Weighted Centroid Localization Algorithm Based on Mamdani Fuzzy Theory [J]. Computer Science, 2015, 42(10): 101-105.
[7] LI Qing and LI Dong-hui. Lossless Color Image Compression Method Based on Fuzzy Logic [J]. Computer Science, 2014, 41(Z11): 103-106.
[8] ZHANG Feng,WANG Jian,ZHAO Yan-fei and DU He. Markov Model for Predicting Trust [J]. Computer Science, 2014, 41(4): 155-158.
[9] ZOU Li,TAN Xue-wei and ZHANG Yun-xia. Knowledge Reasoning Based on Linguistic Truth-valued Intuitionstic Fuzzy Logic [J]. Computer Science, 2014, 41(1): 134-137.
[10] DU Jian,CHEN Hong-bin and ZHAO Feng. Digital Home Service Scheduling Algorithm Based on Fuzzy Logic [J]. Computer Science, 2013, 40(6): 63-66.
[11] PAN Hai-yu,ZHANG Min and CHEN Yi-xiang. Relationships among Several Types of Kripke Structures Based on Fuzzy Logic [J]. Computer Science, 2013, 40(5): 42-44.
[12] ZHANG Jun,GAO Yan and YU Su-hua. Research on Fuzzy Logic in Database Information Retrieval [J]. Computer Science, 2013, 40(10): 183-189.
[13] . Research of MAC Protocol for Wireless Medical Body Area Network Based on Fuzzy Logical Algorithm [J]. Computer Science, 2013, 40(1): 88-90.
[14] . Protocol Based Real-time Component Behavior Consistency Verification [J]. Computer Science, 2012, 39(6): 125-128.
[15] . Research on Dynamic Obstacle Avoidance and Path [J]. Computer Science, 2012, 39(3): 223-227.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!