The Complexity of Temporal Logic with Until and Since over Ordinals

Abstract. 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 α and a formula, we can decide in pspace whether the formula has a model over α. In order to show these results, we introduce a class of simple ordinal automata, as expressive as B¨uchi 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.

• Type: Conference
• Year: 2007
• Where: LPAR
• Authors: Stéphane Demri, Alexander Rabinovich
• Keywords: Artificial Intelligence, LPAR 2007, Ordinal Automata, Simple Ordinal Automata, Temporal Logic