0
$\begingroup$

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$.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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]) $$ $\endgroup$ – michalk93 Oct 9 '17 at 19:25
  • $\begingroup$ @michalk93 $a(true)$ does not mean anything. $\endgroup$ – J.-E. Pin Oct 11 '17 at 10:42
  • $\begingroup$ @j-e-pin So is it bad transform or can I omit the last part with $\forall \dots$ ? $\endgroup$ – michalk93 Oct 11 '17 at 15:03
  • $\begingroup$ I have edited my answer. $\endgroup$ – J.-E. Pin Oct 12 '17 at 8:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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