Sciweavers

Share
LPAR
2007
Springer

The Complexity of Temporal Logic with Until and Since over Ordinals

9 years 10 months ago
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.
Stéphane Demri, Alexander Rabinovich
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LPAR
Authors Stéphane Demri, Alexander Rabinovich
Comments (0)
books