Stephane Demri ; Alexander Rabinovich - The complexity of linear-time temporal logic over the class of ordinals

lmcs:1230 - Logical Methods in Computer Science, December 21, 2010, Volume 6, Issue 4 - https://doi.org/10.2168/LMCS-6(4:9)2010
The complexity of linear-time temporal logic over the class of ordinalsArticle

Authors: Stephane Demri ORCID; Alexander Rabinovich ORCID

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

    https://doi.org/10.2168/LMCS-6(4:9)2010
    Source: arXiv.org:1009.5206
    Volume: Volume 6, Issue 4
    Published on: December 21, 2010
    Imported on: February 23, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1, F.3.1., F.2.2
    Licence: arXiv.org - Non-exclusive license to distribute

    2 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1564 times.
    This article's PDF has been downloaded 277 times.