Expspace-complete variant of guarded fragment with transitivity

Abstract

We introduce a new fragment GF2 + -T →G of the first order logic – the two-variable guarded fragment with one-way transitive guards.This logic corresponds in a natural way to temporal logics without past operators.We prove that the satisfiability problem for GF2+-T →G is EXPSPACE-complete.The lower bound, obtained for the monadic version of the considered logic without equality, improves NEXPTIME lower bound for the whole two-variable guarded fragment with transitive guards GF2 + TG, given by Szwast and Tendera [8].