The complexity of linear-time temporal logic over the class of 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 by 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

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Stéphane Demri, Alexander Rabinovich
• Keywords: CORR 2010, Education, Ordinal Automata, Simple Ordinal Automata, Temporal Logic