Semantisches Browsen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
LATPub332
Abstract In many cases, the addition of metric oper
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.
, but only NP-complete under unary coding.  +
Author Carsten Lutz + , Frank Wolter + , Dirk Walther +
BibTex
@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},
}
Bibtype Article  +
Download LuWaWo-IandC06.ps.gz  +
ErsterAutorNachname Lutz  +
ErsterAutorVorname Carsten  +
Forschungsgruppe Automatentheorie +
Journal Information and Computation  +
Num 1  +
Pages 99-123  +
Publication text Carsten Lutz, Dirk Walther, Frank Wolter&l
Carsten Lutz, Dirk Walther, Frank Wolter<br/> '''[[LATPub332|Quantitative Temporal Logics: PSpace and below]]''' <br/>__NOTOC__Information and Computation, 205(1):99-123, 2006<br/><span class="glyphicon glyphicon-chevron-right" style="font-size: 85%;" ></span> [[LATPub332|Details]] <span class="glyphicon glyphicon-chevron-right" style="font-size: 85%; margin-left: 2ex; "></span> [[Media:LuWaWo-IandC06.ps.gz|Download]]
t; [[Media:LuWaWo-IandC06.ps.gz|Download]]  +
Publication text en Carsten Lutz, Dirk Walther, Frank Wolter&l
Carsten Lutz, Dirk Walther, Frank Wolter<br/> '''[[LATPub332/en|Quantitative Temporal Logics: PSpace and below]]''' <br/>__NOTOC__Information and Computation, 205(1):99-123, 2006<br/><span class="glyphicon glyphicon-chevron-right" style="font-size: 85%;" ></span> [[LATPub332|Details]] <span class="glyphicon glyphicon-chevron-right" style="font-size: 85%; margin-left: 2ex;" ></span> [[Media:LuWaWo-IandC06.ps.gz|Download]]
t; [[Media:LuWaWo-IandC06.ps.gz|Download]]  +
Referiert 1  +
Title Quantitative Temporal Logics: PSpace and below  +
To appear 0  +
Type article  +
Volume 205  +
Year 2006  +
Hat Abfrage
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
LATPub332 + , LATPub332 + , LATPub332 + , LATPub332 + , LATPub332 + , LATPub332 + , LATPub332 +
Kategorien Publikation , Article
Zuletzt geändert
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
26 März 2015 17:33:37  +
verstecke Attribute die hierhin verlinken 
LATPub332/en + Weiterleitungsseite
 

 

Bitte den Namen einer Seite angeben, um mit dem Browsen zu beginnen.