# Formula for F(phi)

+1 vote

I have this doubt about which formula to use for F(phi) in 2 different questions (maybe my concept is not clear but please help):

Aug 2017 6. e) L1  L2 = L1 , here for L1 = F(!b  Xa ∧ G'a)

Aug 2017 7.a)  for F(c)

+1 vote
I am not sure what you are really asking when you mean "to use", but let me try to explain what's the purpose of those F-formulas in the mentioned exam questions.

In Aug-2017-6e, the language L1 has been described by the formula F(!b ∧ X a ∧ PG a) (I am writing PG for the past-G; see http://es.cs.uni-kl.de/tools/teaching/QuartzRef.pdf). The meaning of that formula is as follows: It holds at time t=0 on a path iff there is a point of time delta, such that (!b ∧ X a ∧ PG a) holds at time delta. That means that !b holds at t=delta, a holds at delta+1, and for all x with 0<=x<=delta also a holds. This is exactly the description of L1 in the exercise text, so the formula characterizes L1.

In Aug-2017-7a, the task was to translation the given LTL formula F[a WU b] ∨ [a SB (F c)] to an equivalent ω-automaton. The LTL formula was thereby chosen quite arbitrarily, not having a special meaning. Anyway, let's consider [a SB (F c)]: It states that a must hold before F c holds. Now, if c would hold at some point of time d, then also F(c) would hold from t=0 up to (including) t=d. But then, a has no chance to hold before F(c). So, we conclude that c can never hold, thus. G(!c) must hold. Moreover, as we have a strong-before, a must hold at some point of time, and that can now be anyone.

Hence, [a SB (F c)] is equivalent to (F a) & (G !c). In a similar way, you can argue and find that F[a WU b] is equivalent to (F b) ∨ (F G a).

Does this help?
by (143k points)
I appreciate your explanation sir. I just wanted to know which out of the two formula of F should be applied when we encounter F(something) :

F(psi)= AE ({q},!q,q' <-> q v psi, GFq)
or
phi(F(psi))= AE ({q},1,q <-> psi v Xq, phi(q) ∧ GF[ q -> psi])
Hahaha, I really went in the wrong direction, I see. But you didn't make it easy for me to answer also. Now, I see what you are asking, and actually that is an interesting question.

Clearly, Fφ = A∃({q},¬q,q′↔q∨φ,GFq) means that Fφ is equivalent to the given Büchi automaton A∃({q},¬q,q′↔q∨φ,GFq). However, this refers only to the initial point of time. That means you can replace all formulas Fφ with A∃({q},¬q,q′↔q∨φ,GFq) as long as they are not nested in other formulas. For example, if you have [a SB (F c)], this formula is not the one to choose, since the SB operator will ask for F(c) for points of time later than t=0.

Why is that so? The transition relation q′↔q∨φ implements a watchdog that starts initially in state ¬q, and will switch to q as soon as the first occurrence of φ is seen. It never goes back to ¬q afterwards, and therefore only checks Fφ from t=0 on, but not later.

The other formula you mention is based on the equivalence between G[q↔Fφ] and G[q↔φ∨Xq]∧GF[q→φ] which means that q must ALWAYS (!) behave like Fφ provided that we have q↔φ∨Xq in the transition relation, and add GF[q→φ] as a constraint. This allows you to replace Fφ in any context by q, and therefore also F(c) in [a SB (F c)] to [a SB q] (as long as you add q↔φ∨Xq in the transition relation, and add GF[q→φ] as a constraint).

However, you could use my arguments in the answer above to replace [a SB (F c)] with (F a) & (G !c). Here, the subformula (F a) is only evaluated at the initial point of time, so that you could then use also Fφ = A∃({q},¬q,q′↔q∨φ,GFq) to replace it.

So, the short answer is that it depends on whether the formula Fφ you want to replace is evaluated only at the initial point of time (no surrounding temporal operator) or not.
Does the same condition apply for Xφ and PXφ when translating to w-automaton?

Φ(X(φ))= A∃({q},1,q↔X(φ),Φ(q))
and
Φ(X(φ))= A∃({q0,q1},1,(q0↔φ)&(q1↔Xq0),Φ(q1))

Φ(PX(φ))= A∃({q},q,Xq↔φ,Φ(q))
and
Φ(PX(φ))= A∃({q},!q,Xq↔φ,Φ(q))
Yes, it is the same there. That is why the notation Φ(X(ψ)) is used: It emphasizes that the formula X(ψ) that we abbreviate may occur in any context Φ of other formulas. Thus, we do not just talk about the initial point of time, but all points of times, and all contexts.