Differences

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

Link to this comparison view

Both sides previous revision Previous revision
cs-486:homework-8 [2017/02/21 18:02]
egm
cs-486:homework-8 [2017/02/21 18:05] (current)
egm
Line 1: Line 1:
 == Problems == == Problems ==
  
-'''​1. (points)'''​ Which equivalences are true (justify your answer with a proof or counter-example)+'''​1. (20 points)'''​ Which equivalences are true (justify your answer with a proof or counter-example)
 * []f -> <>g <=> f U (g \/ !f) * []f -> <>g <=> f U (g \/ !f)
 * X <> f1 <=> <> X f1 * X <> f1 <=> <> X f1
Line 8: Line 8:
 * <> f /\ X []f <=> <>f * <> f /\ X []f <=> <>f
  
-'''​2.'''​ ('''​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.''​+'''​2.'''​ ('''​20 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.''​
  
-'''​3.'''​ ('''​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.''​+'''​3.'''​ ('''​25 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.''​
  
-'''​4.'''​ ('''​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.+'''​4.'''​ ('''​20 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.
  
-'''​5.'''​ ('''​points'''​) Is [('''​EF'''​ ''​p''​) || ('''​EF'''​ ''​q''​)] equivalent to '''​EF'''​(''​p''​ || ''​q''​) where the '​||'​ operator is logical OR? Justify your answer.+'''​5.'''​ ('''​10 points'''​) Is [('''​EF'''​ ''​p''​) || ('''​EF'''​ ''​q''​)] equivalent to '''​EF'''​(''​p''​ || ''​q''​) where the '​||'​ operator is logical OR? Justify your answer.
  
-'''​6.'''​ ('''​points'''​) Is [('''​AF'''​ ''​p''​) || ('''​AF'''​ ''​q''​)] equivalent to '''​AF'''​(''​p''​ || ''​q''​)?​ Justify your answer.+'''​6.'''​ ('''​10 points'''​) Is [('''​AF'''​ ''​p''​) || ('''​AF'''​ ''​q''​)] equivalent to '''​AF'''​(''​p''​ || ''​q''​)?​ Justify your answer.
  
cs-486/homework-8.txt ยท Last modified: 2017/02/21 18:05 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