Supplement: Some Variations of the Axiomatic System for LTL

Note that (GFP$_G$) generalizes the induction axiom (IND) $\varphi \wedge G(\varphi \rightarrow X\varphi)\rightarrow G\varphi$ (which we discuss in Section 4.1). In fact, the axiom (GFP$_G$) can be replaced by the following induction rule, which is deducible in the LTL system provided in the main text:

• If $\vdash \psi \rightarrow \varphi \land X\psi$, then $\vdash \psi \rightarrow G\varphi$.

Likewise, (LFP$_U$) can be replaced by the following derivable rule:

• If $\vdash (\psi \vee (\varphi \wedge X\theta)) \rightarrow \theta$, then $\vdash \varphi U \psi \rightarrow \theta$.

Moreover, if we define $G p$ as $\lnot (\top U \lnot p)$, the axioms (FP$_G$) and (GFP$_G$) become deducible from the rest.