1
$\begingroup$

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?

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.