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

Full description

Bibliographic Details
Main Authors: Stephane Demri, Alexander Rabinovich
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2010-12-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/1230/pdf