This preview shows page 1-2-3-4-5 out of 14 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 14 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture 7: Computation Tree LogicsModel of ComputationComputation Tree LogicsThe Logic CTLPath Formulas and S tate FormulasCTL and LTLExpressive Power of Logics1Model of Computationa bb cca ba bcccb cState Transition Graph orKripke Model(Unwind State Graph to obtain Infinite Tree)Infinite Computation Tree2Model of Computation (Cont.)Formally, a Kripke structure is a triple , whereis the set of sta tes,is the tra n s itio n relation, andgives the set of atomic propositions true in each state.We assume thatis total (i.e ., for all states there exists a state such that ).Apath in M is an infinite sequence of sta tes, such that for , .We w r iteto denote the suffix of starting at .Unless otherwise stated, all of our results apply only tofinite Kripke structures.3Computation Tree LogicsTemporal logics may differ according to how they handle branching in the und erlying computatio ntree.In alinear temporal logic, operators are provided for describing events along a single computationpath.In abranching-time logic the temporal operators quantify over the paths that are possible from agiven state.4The Logic CTLThe computation tree logic CTL combines both branch in g - time and linear-time operator s .In this logic apath quantifier can prefix an assertio n composed of arbitrary combinations of theusual linear-time operators .1. Path quantifier:A—“for every path”E—“there exists a path”2. Linear-time operators:X — holds next time.F — holds sometime in the futureG — holds globally in the futureU — holds until holds5Path Formulas and State FormulasThe s y n tax of state formula s is given by the following rules:If , then is a state formula.If and are state formulas, then and are s tate form u las.If is a path formula, then E is a state formula.Two additional r u les are needed to sp ecify the syntax ofpath formulas:If is a state formula, then is also a path formula.If and are path formulas, the n , , X , and U are p ath formulas.6State Formulas ( Cont.)If is a state formula, the notation means that holds at state in the Kripke structure.Assumeand are state formulas and is a path formula. The r elation is definedinductively as follows:1..2. .3. or .4. E there exists a path starting w ithsuch that .7Path Formulas (Cont.)If is a path formula, means that holds along path in Kripke structure .Assumeand are pa th formulas and is a state formula. The relation is definedinductively as follows:1.is the first state of and .2. .3. or .4. X .5. U there exists a such thatand for , .8Standard AbbreviationsThe customary abbreviations will be used for the connectives of propos itio n al logic.In addition, we will use the f o llowing abbreviations in writing tem p o r al opera to r s :A EUG F9CTL and LTLCTL is a res tr icted subset of CTL that permits only b r anching-time operators —each of thelinear-time operators G, F, X, and U must be immediately preceded by a p ath quantifi er.Example: AGEFLTL consists of formu las that have the form A where is a path formula in which the on ly statesubformulas permitted are atomic propositions.Example: AFG10Expressive PowerIt can be shown th at the thre e logics discussed in this s ection have different expressive powers.For example, there is no CTL formula that is equivalent to the LTL formula AFG .Likewise, there is no LTL formula that is equivalent to the CTL for mula AGEF .The d is ju n ction AFG AG EF is a CTL formu la that is not expressible in e ith er CTL orLTL.11Basic CTL OperatorsThere are eight basic CTL operators:AX and EX,AG and EG,AF and EF,AU and EUEach of these can be expressed in terms of EX, EG, and EU:AX EXAG EFAF EGEF E UA U E U EG12Basic CTL OperatorsThe four most wid ely used CTL operators are illustrate d below. Each computatio n tree has the stateas its root.g............ggggg g g............ggAG AFg............g............ggEF EG13Typical CTL FormulasEF : it is possible to get to a state where Started holds but Ready does nothold.AG AF : if a Request occurs, then it will be eventually Ackn o wledged.AG AF : DeviceEna b led holds in fi n itely often on every co mputation path.AG EF : from any state it is possible to get to the Restart


View Full Document
Download Lecture
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?