• DocumentCode
    3386008
  • Title

    Quantitative temporal logics: PSpace and below

  • Author

    Lutz, Carsten ; Walther, Dirk ; Wolter, Frank

  • Author_Institution
    Inst. fur Theor. Informatik, TU Dresden, Germany
  • fYear
    2005
  • fDate
    23-25 June 2005
  • Firstpage
    138
  • Lastpage
    146
  • Abstract
    Often, the addition of metric operators to qualitative temporal logics leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. We show that the language obtained by extending since/until logic of the real line with the operators ´sometime within n time units´, n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.
  • Keywords
    computability; computational complexity; temporal logic; PSpace-complete; PSpace-hard; computational complexity; quantitative temporal logics; satisfiability complexity; unary coding; Application software; Computational complexity; Computer science; Counting circuits; Logic; Mathematics; Real time systems; Upper bound;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on
  • ISSN
    1530-1311
  • Print_ISBN
    0-7695-2370-6
  • Type

    conf

  • DOI
    10.1109/TIME.2005.31
  • Filename
    1443361