Differences

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

Link to this comparison view

cs-486:homework-2-2016 [2017/01/11 17: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.
  
cs-486/homework-2-2016.txt ยท Last modified: 2017/01/11 17:18 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0