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

Both sides previous revision Previous revision | Last revision Both sides next revision | ||

cs-486:homework-7 [2017/02/21 11:00] egm [Problems] |
cs-486:homework-7 [2017/02/21 11:05] egm [Problems] |
||
---|---|---|---|

Line 5: | Line 5: | ||

== Problems == | == Problems == | ||

- | # '''(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 | + | * X a |

- | ## XXX a | + | * XXX a |

- | ## [] b | + | * [] b |

- | ## []<>a | + | * []<>a |

- | ## [](b U a) | + | * [](b U a) |

- | ## <>(b U a) | + | * <>(b U a) |

- | # '''(12 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 | + | |

- | '''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. | + | '''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 | ||

+ | | ||

+ | '''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'' | * The number of items in a buffer may not exceed ''n'' | ||

Line 25: | Line 26: | ||

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

- | '''2.''' ('''1 points''') Express the following property in LTL (the '!' operator is a logical not): | + | '''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'' | ''the transition from !p to p will happen at most once'' | ||

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

''there are infinitely many transitions from !p to p (and vice versa)'' | ''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): | + | '''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.'' | ''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: | + | '''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)'' | ''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)'' | ||