# Issues regarding CTL/LTL/w-Automata

Hi,

I have three questions,

• EGEFa, Now verbally it should mean that there must exist a path such that Globally we are able to reach a.(EFa = paths from where we can reach a). I am having some trouble understanding that how in diagram below it holds in s0? s0 path include e.g {} {}.. a {} but we are not getting a globally here?
• • I am having some problem identifying the state formulas in (CTL/CTL*/LTL) Now I know there is a slide as well and its explained there but could you please give me some examples where a formula is a state formula e.g AFa is a state formula I guess then what about EFXa etc? how to recognize one?
• Regarding omega automata, can you please explain these two steps ? where did !q go?
• +1 vote

About the first point: To detail Martin's explanation, let us abbreviate b := EFa (which is what he calls the inner criterion), then we find that state {s0,s1} satisfy EFa. Thus, let's label then these states by b (see structure below), and then check EGb. I think now you will agree that only state s0 satisfies EGb, i.e., EGEFa, right? As you say, EG EF means that there is a path such that we always CAN reach a. It does not say that we actually do reach a. Looping in state s0, allows us to always reach a, if we want, even though we never do so.

About the second point: How to identify state/path formulas? That is quite simple, since the following and only the following are state formulas:

• propositional formulas are state formulas, i.e., all formulas without any temporal operator X,G,F,WU,SU,WB,SB,WW,SW or path quantifier E,A
• every formula starting with a path quantifier E or A is a state formula
• state formulas are closed under boolean operators
Hence, to decide whether a given formula is a state formula, you may first replace the subformulas starting with E or A by new propositional variables. If that is done, and a propositional logic formula is obtained, you have a state formula, otherwise it is a path formula since subformulas with temporal operators are left.
Third, I guess you don't understand the nesting of automaton formulas. An automaton formula A(Q,I,R,F) is evaluated on a path and either accepts or rejects the path by evaluating the acceptance condition F which is a path formula on the path (in a product structure). Automata formulas themselves are also path formulas, so we can consider A(Q1,I1,R1,A(Q2,I2,R2,F2)) which is equivalent to A(Q1∪Q2,I1∧I2,R1∧R2,F2) and the latter is simply the product automaton of the two involved automata. You can find that in the omega-automata chapter.

by (117k points)
selected by
Thanks for great explanation, could you please give me one example of "you may first replace the subformulas starting with E or A by new propositional variables" ?
Sure, if you have [a SU EGb] ∧ EFa, I would replace p1 = EGb and p2 := EFa to get [a SU p1] ∧ p2 which is not propositional, and hence, the given formula is not a state formula. On the contrary, for A[a SU EGb] ∧ EFa, I would replace p1 = EGb, p2 := EFa, and p3 = A[a SU p1] to get p3 ∧ p2 which is propositional, and hence, that formula is a state formula.
Hmm interesting, thanks for the example so e.g Fa is a state formula where as [Fa WU 1] & Fa is not?
No, Fa is not a state formula. Look, there are not subformulas starting with E or A in it that I could replace to make it a propositional formula. That's why it is a path formula like [Fa WU 1] & Fa.
okay understood sorry, in your example where we had [a SU EGb] ∧ EFa what if we had only EFa? It does satisfy the second condition which you shared above and has only one formula!
Yes, EFa would be replaced with my algorithm by a single propositional logic variable p1 which is a propositional formula, thus EFa is a state formula.
+1 vote
• Look at the path s0→s0→s0→s0→s0→… We want to satisfy EG with it. That means that every state in it needs to satisfy the inner criterion. Let's look at its only state s0. From it's only state s0 there is a second path s0→s1→s2→s2→… The second path satisfies a in s1. Hence it satisfies Fa in s0. This is the paths that exists from s0 on.
• “State formula“ in which context? So G, F, SU, WU, SB, WB … and so on are temporal quantifiers. They are describing the property per path. E/A are path quantifiers. They describe per state whether this state has one path/only paths with certain properties.
• The step in the automata formula might be a bug. Do you want to give me more context?
by (25.2k points)
Thanks for the explanation
I dont understand this statement "That means that every state in it needs to satisfy the inner criterion" How does every state in s0,...s0 satisfies the criterion? which is EFa? is EFa = Fa?
In the context of opening e.g E[a & b] we can simplify to Ea & b if b is a state formula. There are some formulas given in this context in slides as well e.g. AP, EP.
Yeah so in the last step we are opening the nesting of A_E formulas and the nesting formula is pretty straightforward However it does not involved negation of q as it deals with only the new state r. I have been seeing previous exam solutions as well and there also in the last step I saw negation for existing states e.g. p,q here are removed or added but the formula of nesting formulas does not says so it simply state we need to take & between states
You are right. As the outer formula is EG…, the one path we picked needs to satisfy G…, which means that every of its states (which is just s0) needs to satisfy the inner formula. The inner formula is EFa. EFa and Fa are different. EFa marks states from where a path satisfying Fa starts. Fa marks whole paths that satisfy a at some point. In particular, EGFa finds one path that satisfies a infinitely often, while EGEFa finds one path from where every step is the start of a (possible different) path that eventually reaches a.

So could it be a a formula that only talks about the properties of states, not about branching behavior not about temporal properties? Can you tell me the slides you mentioned?

Could you tell me exams where you didn't understand the last step (of un-nesting the automata formulas?)? Then I could have a look.
Thanks, Martin for the great explanation, I have understood 1 and 2 and for three I am referring to Exams "2020.08.25" Q 5(c) and 2020.02.19 5(c) i don't understand the last unnesting step only.