# Simple LTL formulas into First Order Logic formulas

I would like to know if it is possible to transform simple LTL logic formula i.e.: $G a$ or $F a$ (where $G$ - globally, $F$ - finally) to First Order Logic formula.

I was wondering if the below statements are true under some conditions: $$Ga = \forall a \\ Fa = \exists a$$

My aim is to use SPASS theorem prover (https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/) to prove simple LTL formulas, but the SPASS is the First Order Logic prover. If it is possible how to present in SPASS syntax statements like: $Ga$ or $Fa$.

A first order formula $T(\varphi)$ equivalent to the LTL formula $\varphi$ can be computed as follows (see these slides): \begin{align} T(a) &= a(x)\\ T(X\varphi) &= ∃y\ (y=x+1)∧T(\varphi)[y/x] \\ T(\varphi \mathop{U} \psi) &= ∃y\ (x \leqslant y) \wedge T(\psi)[y/x] \wedge ∀z\ \bigl((x \leqslant z < y) \rightarrow T(\varphi)[z/x]\bigr) \end{align} For $F$ and $G$, you can use the formulas $F\varphi = \textbf{True} \mathop{U} \varphi$ and $G\varphi = \neg F \neg \varphi$. For instance, $$Fa = T(\textbf{True} \mathop{U} a) = ∃y\ (x \leqslant y) \wedge a(y) \wedge ∀z\ \bigl((x \leqslant z < y) \rightarrow \textbf{True}(z)\bigr)$$ Note that the opposite conversion (FO to LTL) would be much harder. Indeed, also Propositional LTL over the naturals has the expressive power of FO (Gabbay, Pnueli, Shelah & Stavi, 1980), LTL satisfiability is is PSPACE-complete (Halpern&Reif, 1981, Sistla&Clarke, 1982) while satisfiability of FO over finite words is nonelementary (no bounded-height tower) [Stockmeyer, 1974]. Thus there is no elementary conversion from FO to LTL.

• So for the $Fa$ the FO formula should be like below? $$\exists y (x \leqslant y) \land a(x)[y/x] \land \forall z ((x \leqslant z < y) \implies a(true)[z/x])$$ – michalk93 Oct 9 '17 at 19:25
• @michalk93 $a(true)$ does not mean anything. – J.-E. Pin Oct 11 '17 at 10:42
• @j-e-pin So is it bad transform or can I omit the last part with $\forall \dots$ ? – michalk93 Oct 11 '17 at 15:03
• I have edited my answer. – J.-E. Pin Oct 12 '17 at 8:04