Quantitative Temporal Logics: PSpace and below

C. LutzC. Lutz, D. WaltherD. Walther, F. WolterF. Wolter

Datei:LuWaWo-IandC06.ps.gz

Download

C. Lutz, D. Walther, F. Wolter
Quantitative Temporal Logics: PSpace and below
Information and Computation, 205(1):99-123, 2006

Details
Bibtex

KurzfassungAbstract
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 metric operators are coded in binary.  We
 then consider metric TLs of the reals that do not offer any
 qualitative temporal operators.  In such languages, the complexity
 turns out to depend on whether binary or unary coding of parameters
 is assumed: satisfiability is still PSpace-complete under binary

coding, but only NP-complete under unary coding.

Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ LuWaWo-IandC-06,
  author = {C. {Lutz} and D. {Walther} and F. {Wolter}},
  journal = {Information and Computation},
  number = {1},
  pages = {99--123},
  title = {Quantitative Temporal Logics: {{\sc PSpace}} and below},
  volume = {205},
  year = {2006},
}