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-7 [2017/02/21 18:05]
egm [Problems]
cs-486:homework-7 [2018/11/02 22:21] (current)
egm [Problems]
Line 6: Line 6:
  
 '''​1. (12 points)'''​ For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 -> s2. s2 -> s3. s3 -> s1. s4 -> s2. s3 and s4 are initial states.  ​ '''​1. (12 points)'''​ For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 -> s2. s2 -> s3. s3 -> s1. s4 -> s2. s3 and s4 are initial states.  ​
-* X a +A(X a) 
-* XXX a +A(XXX a) 
-* [] b +A([] b) 
-* []<>​a +A([]<>a) 
-* [](b U a) +A([](b U a)
-* <>(b U a)+A(<>(b U a)
 +Hint: consider each state as the starting state for the formula.
  
 '''​2. (16 points)'''​ This problem is Exercise 5.5 in [http://​is.ifmo.ru/​books/​_principles_of_model_checking.pdf Principles of Model Checking ] (page 321 of the PDF document), consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator as LTL formulae and give the LTL formulae: '''​2. (16 points)'''​ This problem is Exercise 5.5 in [http://​is.ifmo.ru/​books/​_principles_of_model_checking.pdf Principles of Model Checking ] (page 321 of the PDF document), consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator as LTL formulae and give the LTL formulae:
cs-486/homework-7.txt · Last modified: 2018/11/02 22:21 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