《ltl和CTL讲义》PPT课件

《《ltl和CTL讲义》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、LinearTemporalLogicRestrictpathquantificationto“ALL”(no“EXISTS”)ReasonintermsoflineartracesinsteadofbranchingtreesLinearTemporalLogic(LTL)SemanticIntuition[]F…alwaysF<>F…eventuallyFFUG…FuntilGFFFFFFFFFFFFFFFFFFFFFFGFGF::=P…primitivepropositions

2、!F

3、F&&F

4、F

5、

6、F

7、F->F…

8、propositionalconnectives

9、[]F

10、<>F

11、FUF

12、XF…temporaloperatorsSyntaxLTLNotesInventedbyPrior(1960’s),andfirstusetoreasonaboutconcurrentsystemsbyA.Pnueli,Z.Manna,etc.LTLmodel-checkersareusuallyexplicit-statecheckersduetoconnectionbetweenLTLandautomatatheoryMostpopularLT

13、L-basedcheckerisSpin(G.Holzman)ComputationalTreeLogic(CTL)F::=P…primitivepropositions

14、!F

15、F&&F

16、F

17、

18、F

19、F->F…propositionalconnectives

20、AGF

21、EGF

22、AFF

23、EFF…temporaloperators

24、AXF

25、EXF

26、A[FUF]

27、E[FUF]SyntaxSemanticIntuitionAGp…alongAllpathspholdsGloballyEGp…thereExistsapathwher

28、epholdsGloballyAFp…alongAllpathspholdsatsomestateintheFutureEFp…thereExistsapathwherepholdsatsomestateintheFuturepathquantifiertemporaloperatorComputationalTreeLogic(CTL)F::=P…primitivepropositions

29、!F

30、F&&F

31、F

32、

33、F

34、F->F…propositionalconnectives

35、AGF

36、EGF

37、AFF

38、EFF…path/t

39、emporaloperators

40、AXF

41、EXF

42、A[FUF]

43、E[FUF]SyntaxSemanticIntuitionAXp…alongAllpaths,pholdsintheneXtstateEXp…thereExistsapathwherepholdsintheneXtstateA[pUq]…alongAllpaths,pholdsUntilqholdsE[pUq]…thereExistsapathwherepholdsUntilqholdsComputationTreeLogicpppppppppppppppA

44、GpComputationTreeLogicEGpppppComputationTreeLogicAFpppppppComputationTreeLogicEFppComputationTreeLogicAXppppppppppComputationTreeLogicEXpppppppComputationTreeLogicA[pUq]pppqqppqqppComputationTreeLogicE[pUq]ppqqppqqqExampleCTLSpecificationsForanystate,arequest(for

45、someresource)willeventuallybeacknowledgedAG(requested->AFacknowledged)Fromanystate,itispossibletogettoarestartstateAG(EFrestart)AnupwardstravellingelevatoratthesecondfloordoesnotchangesitsdirectionwhenithaspassengerswaitingtogotothefifthfloorAG((floor=2&&directio

46、n=up&&button5pressed)->A[direction=upUfloor=5])CTLNotesInventedbyE.ClarkeandE.A.Emerson(early1980’s)SpecificationlanguageforSymbolicModelVerifier(SMV)model-che