The Complexity of the Temporal Logic with Until over General Linear Time

Abstract

It is shown that the decision problem for the temporal logic with the strict until operator over general linear time is PSPACE-complete. This shows that it is no harder to reason with arbitrary linear orderings than with discrete linear time temporal logics. New techniques are used to give a PSPACE procedure for the logic.

Full Paper

Postscript version 8/3/2002
Sightly different earlier version of May 1999

Status

Appeared as:
M. Reynolds. The complexity of the temporal logic with “until” over general linear time, Journal of Computer and System Sciences, 66 (2003) pp 393-426.

Bibtex

@article{Rey:cult,
author="M. Reynolds",
title="The Complexity of the Temporal Logic with Until over General Linear Time",
journal="Journal of Computer and System Science",
volume="66",
pages="393--426",
year="2003"
}