Sciweavers

Share
IANDC
2007

Quantitative temporal logics over the reals: PSpace and below

9 years 2 months ago
Quantitative temporal logics over the reals: PSpace and below
In many cases, the addition of metric operators to qualitative temporal logics (TLs) increases the complexity of satisfiability by at least one exponential: while common qualitative TLs are complete for NP or PSpace, their metric extensions are often ExpSpace-complete or even undecidable. In this paper, we exhibit several metric extensions of qualitative TLs of the real line that are at most PSpace-complete, and analyze the transition from NP to PSpace for such logics. Our first result is that the logic obtained by extending since-until logic of the real line with the operators ‘sometime within n time units in the past/future’ is still PSpace-complete. In contrast to existing results, we also capture the case where n is coded in binary and the finite variability assumption is not made. To establish containment in PSpace, we use a novel reduction technique that can also be used to prove tight upper complexity bounds for many other metric TLs in which the numerical parameters to ...
Carsten Lutz, Dirk Walther, Frank Wolter
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where IANDC
Authors Carsten Lutz, Dirk Walther, Frank Wolter
Comments (0)
books