The complexity of temporal logic with until and since over ordinals

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic thanks to Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal alpha and a formula, we can decide in PSPACE whether the formula has a model over alpha. In order to show these results, we introduce a class of simple ordinal automata, as expressive as Buchi ordinal automata. The PSPACE upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.