This shows you the differences between two versions of the page.

— |
cs-486:homework-2-2016 [2017/01/11 10:18] (current) egm created |
||
---|---|---|---|

Line 1: | Line 1: | ||

+ | Objectives: | ||

+ | * Practice writing CTL* properties | ||

+ | * Create minimal paths that satisfy properties | ||

+ | * Practice writing LTL properties | ||

+ | * Describe the difference in expressiveness between LTL, CTL, and CTL* | ||

+ | |||

+ | == Reading == | ||

+ | Chapter 2 of the course text. | ||

+ | |||

+ | == Paper Pencil Problems == | ||

+ | '''1.''' ('''4 points''') For each of the following properties: label as either safety or liveness, express in a CTL* formula, and create a minimal label trace to satisfy written formula. | ||

+ | |||

+ | * The number of items in a buffer may not exceed ''n'' | ||

+ | * If a process reaches a location ''li'' just before a critical section, it should not be blocked forever | ||

+ | * Clients may not retain resources forever | ||

+ | * It is always cloudy before it rains | ||

+ | |||

+ | '''2.''' ('''1 points''') Express the following property in LTL (the '!' operator is a logical not): | ||

+ | |||

+ | ''the transition from !p to p will happen at most once'' | ||

+ | |||

+ | '''3.''' ('''1 points''') Express the following property in LTL: | ||

+ | |||

+ | ''there are infinitely many transitions from !p to p (and vice versa)'' | ||

+ | |||

+ | '''4.''' ('''3 points''') Express the following property in LTL using ''r'', ''y'', ''g'' as atomic propositions denoting the states of the traffic light (r = red, y = yellow, g = green): | ||

+ | |||

+ | ''The lights of a traffic signal light in the following periodic sequence: red, yellow, green, red, yellow, green,... and only one light is on at any given time, starting with red. You cannot make any assumptions on how long a light is on other than it will be on for a finite length of time.'' | ||

+ | |||

+ | '''5.''' ('''3 points''') Express the following property in LTL: | ||

+ | |||

+ | ''if q holds in a state si and r holds in some subsequent state (sj , j > i) then p must not hold in any state sk in between si and sj (i < k < j , where j is the first such subsequent state)'' | ||

+ | |||

+ | '''6.''' ('''5 points''') The CTL formula '''AF''' ('''AG''' ''p'') is stronger than the LTL formula '''FG''' ''p'' meaning that a particular Kripke structure may model '''FG''' ''p'' but not '''AF''' ('''AG''' ''p''). Draw such a Kripke structure and explain why that Kripke structure does not satisfy the CTL formula. Also prove that if a system satisfies the CTL formula, it must also satisfy the LTL formula. In what situation might you want to use the stronger formula (finding bugs or verifying correctness)? '''Hint''': ''there are only three states in the Kripke structure.'' | ||

+ | |||

+ | '''7.''' ('''5 points''') The LTL formula '''GF''' ''p'' is stronger than the CTL formula '''AG''' ('''EF''' ''p'') meaning a Kripke structure may model '''AG''' ('''EF''' ''p'') but not model '''GF''' ''p''. Draw such a Kripke structure and explain why that Kripke structure does not satisfy the LTL formula. Also prove that if a system satisfies the LTL formula, it must also satisfy the CTL formula. '''Hint''': ''there are only two states in the Kripke structure.'' | ||

+ | |||

+ | '''8.''' ('''3 points''') Explain why the CTL* formula '''E'''('''GF''' ''p'') is not equivalent to either of the CTL formulas '''EG'''('''EF''' ''p'') and '''EG'''('''AF''' ''p''). For each pair of (CTL*, CTL) formula, state which property is stronger, and draw a Kripke structure that satisfies the weaker property but not the stronger property. | ||

+ | |||

+ | '''9.''' ('''3 points''') Is [('''EF''' ''p'') || ('''EF''' ''q'')] equivalent to '''EF'''(''p'' || ''q'') where the '||' operator is logical OR? Justify your answer. | ||

+ | |||

+ | '''10.''' ('''3 points''') Is [('''AF''' ''p'') || ('''AF''' ''q'')] equivalent to '''AF'''(''p'' || ''q'')? Justify your answer. | ||