0.6 Using temporal logic to specify properties: homework exercises

Give an English translation of the following LTL formulae. Try to give a natural wording for each, not just a transliterationof the logical operators.

• $(◇r(pUr))$
• $\square (q\square p)$

In the following, give an LTL formula that formalizes the given English wording.If the English is subject to any ambiguity, as it frequently is, describe how you are disambiguating it, and why.

• `` $p$ is true.''
• `` $p$ becomes true before $r$ .''
• • `` $p$ will happen at most once.''
  • `` $p$ will happen at most twice.''
• ``The light always blinks.''Use the following proposition: $p$ = the light is on.
• ``The lights of a traffic signal always light in thefollowing sequence: green, yellow, red, and back to green, etc. , with exactly one light on at any time.''Use the following propositions: $g$ = the green light is on, $y$ = the yellow light is on, and $r$ = the red light is on.

Recall the Dining Philosophers Problem from the previous homework . Using temporal logic, formally specify the following desiredproperties of solutions to the D.P. Problem. Use the following logic variables, where $0i<N$ :

• $l_i$ : Philosopher $i$ has his/her left fork.
• $r_i$ : Philosopher $i$ has his/her left fork.

For each question, your answer should cover exactly the given condition -- nothing more or less.You may assume $N=3$ .

• No fork is ever claimed to be held bytwo philosophers simultaneously.
• Philosopher $i$ gets to eat (at least once).
• Each philosopher gets to eat infinitely often.
• The philosophers don't deadlock.(The main difficulty is to conceptualize and restate ``deadlock''within this specific model in terms of the available logic variables.)You may assume philosophers pick uptwo forks in some order, eat, and drop both forks.
• The philosophers don't deadlock.(The main difficulty is to conceptualize and restate ``deadlock''within this specific model in terms of the available logic variables.)You may not assume philosophers pick uptwo forks in some order, eat, and drop both forks. For example, one might pick up a single fork and then drop it.Or, the philosophers might be lazy and never pick up a fork.
• Describe a D.P. Problem run in which philosophers don'tdeadlock, but it is not the case that each philosopher gets to eat infinitely often.