Nicolas Markey

Abstract

We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.

@inproceedings{lics2002-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Temporal Logic with Forgettable Past},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {383-392},
  year =                {2002},
  month =               jul,
  doi =                 {10.1109/LICS.2002.1029846},
  abstract =            {We investigate NLTL, a linear-time temporal logic
                         with forgettable past. NLTL can be exponentially
                         more succinct than LTL + Past (which in turn can be
                         more succinct than LTL). We study satisfiability and
                         model checking for NLTL and provide optimal
                         automata-theoretic algorithms for these
                         EXPSPACE-complete problems.},
}