Why can't we somehow represent it's negation in LTL and go from there? I think maybe because it has (effectively) two existential quantifiers, so negating it does not work. But how do I prove it?
1 Answer
$\begingroup$
$\endgroup$
There is a delicate point here, about the semantics of LTL vs CTL.
Given a formula $\psi$ in LTL, we say that it holds in a structure $K$ if every path in $K$ satisfies $\psi$.
In CTL, however, the path quantifiers are built in to the formula.
To make this more precise, you can think of LTL as the fragment of CTL* of the form $A\psi$, where $\psi$ doesn't contain any path quantifiers (i.e., it's in LTL).
Now, you suggest negating your formula, so you obtain $AG\neg p$. This formula is not an LTL formula, due to the quantifier $A$. But it does have an LTL equivalent, namely $G\neg p$.
However, if you try to negate back to CTL, the negation of the LTL formula is now $Fp$, but the semantic of LTL means that it is interpreted as $AFp$, whereas you wanted $EFp$.
To sum up, you just cannot express the path quantifier $E$ in LTL.
To prove that the formula $EFp$ does not have an LTL equivalent, consider (towards a contradiction) some equivalent LTL formula $\psi$, and take a structure that has two "branches" -- one with $p$ and one without (e.g., two states with self loops). Since this structure satisfies the $EFp$, then it also satisfies $\psi$, meaning that every computation in it satisfies $\psi$. But now, if you remove one of the branches (the one with $p$), then $\psi$ is still satisfied (since you only removed computations). However, $EFp$ is not satisfies, so $\psi$ is not its equivalent.
