Temporal logic - mixing AF and AG in CTL formula

Question

Let's look at example AF(φ1 -> AG(φ2)).

Does it mean that:

1. In all paths it eventually happens that if φ1 was satisfied, φ2 is satisfied all along the path (so it basically means φ2 is satisfied in all states in all paths)

or

2. In all paths it eventually happens that if φ1 was satisfied, φ2 is satisfied starting when the φ1 satisfaction started

or

3. Something else?

If 1, then isn't it equivalent to AF(φ1) -> AG(φ2)?

If 2, will the G start at the current or at the next iteration?

For example if φ1=p , φ2=q, are both A and B in the language, or just A?

A. q-p-q-pq-q-q-q-q-q...

B. q-p-q-p-q-q-q-q-q...

Answer 1

Does it mean that: 1. or 2. or 3.?

Your second interpretation is correct: $\varphi_1 \rightarrow AG(\varphi_2)$ is a CTL state formula, and to check whether it is satisfied by a state $s$, the path formula $G(\varphi_2)$ is evaluated relatively to the paths starting in s.

Therefore, a state $s$ satisfies your formula $AF(\varphi_1 \rightarrow AG(\varphi_2))$ iff all paths starting at $s$ eventually reach a state $s'$, such that if $\varphi_1$ holds in $s'$, then all paths starting at $s'$ satisfy that all states on this path satisfy $\varphi_2$.

If 2, will the G start at the current or at the next iteration?

G starts at the current state/iteration. A path satisfies $G\varphi$ iff all states on this path satisfy $\varphi$, including the current state.

For example if φ1=p , φ2=q, are both A and B in the language, or just A?

I am not sure what you mean by the "language" of a CTL formula. For LTL it makes sense to define the language of a formula, containing the words / label sequences that satisfy the formula. CTL does not reason about linear sequences, but about branching time, so usually for a CTL formula we are interested in the labeled transition systems whose initial states satisfy the formula (alternatively, you can unroll the transition systems and use CTL formulas to reason about languages of infinite, finitely-branching, labeled trees). I assume you meant "language" in this sense, i.e. A and B are meant as sketches of transitions systems or their unrolling, with the left-most state as the initial state.

Then A and B both satisfy the formula: Both have an initial state that is not labeled with $\varphi_1 = p$. Hence both initial states satisfy the CTL state formula $\varphi_1 \rightarrow AG(\varphi_2)$. Therefore, it is true that all paths starting from their initial states eventually (in this case immediately) reach a state that satisfies $\varphi_1 \rightarrow AG(\varphi_2)$. Thus, the initial states satisfy $AF(\varphi_1 \rightarrow AG(\varphi_2))$.

References: Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.