LATPub332: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 1: | Zeile 1: | ||
{{Publikation Erster Autor | {{Publikation Erster Autor | ||
|ErsterAutorVorname= | |ErsterAutorVorname=Carsten | ||
|ErsterAutorNachname=Lutz | |ErsterAutorNachname=Lutz | ||
|FurtherAuthors=D. Walther; | |FurtherAuthors=D. Walther; Frank Wolter | ||
}} | }} | ||
{{Article | {{Article | ||
| Zeile 18: | Zeile 18: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract= | |Abstract= 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. | ||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 57: | Zeile 36: | ||
year = {2006}, | year = {2006}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
Quantitative Temporal Logics: PSpace and below
Carsten LutzCarsten Lutz, D. WaltherD. Walther, Frank WolterFrank Wolter
Carsten Lutz, D. Walther, Frank Wolter
Quantitative Temporal Logics: PSpace and below
Information and Computation, 205(1):99-123, 2006
Quantitative Temporal Logics: PSpace and below
Information and Computation, 205(1):99-123, 2006
- 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},
}
