Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

+1 vote
The Que is from 2016 sept prob 7.b

How is (past(X)a <->a) = Ga //why not Ga V G neg(a)
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+1 vote
The PSX (past-strong-X) and PWX (past-weak-X) are defined such that they check whether their argument formula φ holds on the point of time right before the considered point of time. They differ at the initial point of time: PSXφ is false there, and PWXφ is true there.

Now, consider G((PWX a) <-> a): It means, that (PWX a) <-> a holds at all points of time. At time 0, this means true<->a since PWX a is true there, and at time 1, it means a(0) <-> a(1), and thus a(1) must hold, and so on. Thus, always a(t) holds, and that means Ga holds.
by (166k points)

Related questions

Imprint | Privacy Policy