Paper: Temporal Logic with Forgettable Past (at LICS 2002)

Authors: François Laroussinie Nicolas Markey Philippe Schnoebelen

Abstract

We investigate NLTL, a temporal logic with forgettable past. We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems. We also prove a succinctness gap between NLTL and LTL+Past, and between LTL+Past and LTL partly answering a folk conjecture.

BibTeX

  @InProceedings{LaroussinieMarkeySc-TemporalLogicwithFo,
    author = 	 {François Laroussinie and Nicolas Markey and Philippe Schnoebelen},
    title = 	 {Temporal Logic with Forgettable Past},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {383--392},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }