##### Differences

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

 cs-486:homework-7 [2017/01/11 19:12]egm removed cs-486:homework-7 [2018/11/02 22:21] (current)egm [Problems] Both sides previous revision Previous revision 2018/11/02 22:21 egm [Problems] 2017/02/21 18:05 egm [Problems] 2017/02/21 18:00 egm [Problems] 2017/02/21 17:59 egm 2017/02/21 17:58 egm created2017/01/11 19:12 egm removed2016/04/06 19:44 egm [Paper Pencil] 2014/09/02 16:43 egm created Next revision Previous revision 2018/11/02 22:21 egm [Problems] 2017/02/21 18:05 egm [Problems] 2017/02/21 18:00 egm [Problems] 2017/02/21 17:59 egm 2017/02/21 17:58 egm created2017/01/11 19:12 egm removed2016/04/06 19:44 egm [Paper Pencil] 2014/09/02 16:43 egm created Line 1: Line 1: - This homework is to practice using BDDs for symbolic model checking. + Objectives:​ + * Write temporal logic properties + * Master the semantics of temporal logic - ==Paper Pencil== + == Problems ​== - # ('''​3 points'''​) Write a CTL property for the transition ​relation for the dinning philosophers ​system ​in [[Homework 3]]--the property must require ​a least or greatest fix-point to compute. + '''​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. - # ('''​5 points'''​) At an abstract level, similar to what we did on the board in lecture, perform symbolic model checking for the formula in the prior problem. Be sure to show each step of the fix-pont computation. Please note that if the '''​when'''​ clause is correctly treated as a single atomic action (i.e., the test, state update, ​and goto are one step), then there are only 10 reachable ​states. + * A(X a) + * A(XXX a) + * A([] b) + * A([]<>​a) + * A([](b U a)) + * A(<>​(b U a)) + Hint: consider each state as the starting state for the formula. - ==Programming== + '''​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: + * Any door on any floor is never open when the elevator is not present + * A requested floor will be served eventually + * The elevator repeatedly returns to floor 0 + * When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up - Use the CUDD package for the following ​problems. + '''​3.'''​ ('''​16 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 + + '''​4.'''​ ('''​4 points'''​) Express ​the following ​property in LTL (the '​!'​ operator is a logical not): + + ''​the transition from !p to p will happen at most once''​ + + '''​5.'''​ ('''​4 points'''​) Express the following property in LTL: + + ''​there are infinitely many transitions from !p to p (and vice versa)''​ + + '''​6.'''​ ('''​8 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.''​ + + '''​7.'''​ ('''​5 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)''​ - # ('''​10 points'''​) Write a program in CUDD using your solution from [[Homework 6]] that does symbolic model checking for your formula in the prior problem.