Hi, i wanted to know the LTL(linear temporal logic) expressions for the followin

Question

Hi, i wanted to know the LTL(linear temporal logic) expressions for the following properties informally described in english. The temporal operators are: X - next ,U- until, F- eventually, G- always , W- weak until and atomic propositions are r,g,b. (a) once the state becomes red, it remains red forever. (b) There will be infinitely many green states. (c) Eventually the state will be blue forever. (d) A state cannot be both green and red, and the system evolves in an infinite alternation of (non-empty and finite) green periods and red periods.

Explanation / Answer

Dear Friend, Please rate this answer.

a. ~r W G r

b. GF g

c. FG b

d. G(~g v ~r) ^ (G((g^gUr)v(r^rUg)))

please note that i've used ^ to mean AND

Related Questions

Navigate

• Browse (All)
• Browse H
• Subjects

---