Temporal Logic

How can we say whether CTL* formula will be converted to LTL and CTL?

I know LTL formula is the one which has only path formulas (temporal operators) and they don't have path quantifiers

CTL formulas have pair of temporal operator and path quantifier.

But here I am not able to simplify the formula. Can you please help how to approach them?

1) How we are getting A0? Which formulas are we using?

2) How are we getting highlighted steps? Which formulas are we using here?

In general, it is not that simple to decide whether a CTL* formula is equivalent to a LTL or CTL formula. For LTL, there is the following nice theorem that you can find on slide 43 of Chapter VRS-07.

Theorem ([2]): Given a CTL formula phi, let psi be the quantifier-free formula that is obtained by removing all path quantifiers from phi. Then, there is an equivalent LTL formula for phi iff A psi is equivalent to phi.

It requires however to check whether the original formula is equivalent to the constructed LTL formula, and that is again not that simple, since we did not discuss theorem proving for CTL*. Here, you need to check that by your intuitive understanding, i.e., read the formulas and try to say whether or not the above two formulas are the same. Typical cases where it goes wrong are alternating path quantifiers like A...E.. or E..A.., but that is not necessrarily the case.

It is a bit simpler for the question whether a given CTL* formula is equivalent to a CTL formula. We learned two major transformations: (1) driving path quantifiers inwards (and duplicating them thereby), and (2) removing propositional operators after a path quantifiers. Number (2) can ALWAYS be done, but number (1) sometimes fails and only works for the subset that is called LeftCTL* of CTL*. So, try to apply these transformations, and if they work, you have a CTL formula.

Apart from that, you also need to check some contradictions in the formulas that allow certain simplifications. In the above case, AGFa and AFG!a are contradicting and can only be satisfied if a state does not have any outgoing infinite path which are exactly the states satisfying A false. Since A false is not a CTL formula, it is replaced by the equivalent AGfalse.

Second example: in general, we have [p WU q] & (F q) = [p SU q] which is step 1, and second, we have [true SU q] = F q which is step 2.
by (162k points)