Simple interpretations among complicated theories (Q923068)

Let QPTL denote the quantified propositional temporal logic with temporal operators ``nexttime'' and ``from now on forever'' and with the time structure of the type of natural numbers. Interpretations of some formal theories in QPTL are described which do not increase the number of quantifier alternations. By use of results of Sistla, Vardi and Wolper on complexity of quantifier bounded fragments of QPTL it gives (k-1)-fold exponential upper bounds of space complexity for the formulae of these theories with at most k quantifier alternations. The theories considered are 1): extensions of Presburger arithmetic by the predicate \(x/_ my\) which expresses that x is a power of m which divides y (for fixed m), 2) first order theories of m-ary trees with m successors, the prefix relation and the equal length relation, 3) the existential monadic second order theory of finite linear orders.