Quantitative Temporal Logics: PSpace and below

Carsten LutzCarsten Lutz, Dirk WaltherDirk Walther, Frank WolterFrank Wolter

Datei:LutzWaltherWolter-LTCS-05-03.ps.gz

Download

Carsten Lutz, Dirk Walther, Frank Wolter
Quantitative Temporal Logics: PSpace and below
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-05-03, 2005. LTCS-Report

Details
Bibtex

KurzfassungAbstract
The addition of metric operators to qualitative temporal logics often 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. The main result states 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.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ LutzWaltherWolter-LTCS-05-03,
  address = {Germany},
  author = {C. {Lutz} and D. {Walther} and F. {Wolter}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-03},
  title = {Quantitative Temporal Logics: PSpace and below},
  type = {LTCS-Report},
  year = {2005},
}