Formulas in LTL (temporal logic)

Question

If I have an LTL statement about modus ponens P: "(G A) → B"

If P is false, could the opposite of P also be false?

Is it the case that "G A → B" means "(G A) → B" and not "G (A → B)" ?

Answer 1

First question: is it possible for "a formula and its negation to be both false?"

The actual question is, "given a Kripke structure $K$ and an LTL formula $\varphi$, is it possible that $K \not\models \varphi$ and $K \not\models \neg \varphi$ are both true?" Yes, $K \models \varphi$ if and only if, for every initial state $s$ of $K$, $K,s \models \varphi$. If there's more than one initial state, say $s_0$ and $s_1$, it's possible that $K,s_0 \models \varphi$, and $K,s_1 \models \neg \varphi$, so that $K$ is not a model of either $\varphi$ or $\neg\varphi$.

Second question:

Operator precedence for LTL varies from author to author and from tool to tool. Consult the definitions/documentation or add parentheses.