The complexity of linear-time temporal logic over the class of ordinals

TL;DR

This paper investigates the satisfiability problem of linear-time temporal logic over ordinals, proving it is PSPACE-complete and introducing simple ordinal automata to facilitate decision procedures.

Contribution

It establishes the PSPACE-completeness of the satisfiability problem for temporal logic over ordinals and introduces simple ordinal automata for decision procedures.

Findings

PSPACE-complete satisfiability problem over ordinals

Decidability of model existence given an ordinal code

Introduction of simple ordinal automata as expressive as B"uchi ordinal automata

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 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 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 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.