Nicolas Markey

Abstract

We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.

@article{acta40(6-7)-Mar,
  author =              {Markey, Nicolas},
  title =               {Past is for Free: On the Complexity of Verifying
                         Linear Temporal Properties with Past},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {40},
  number =              {6-7},
  pages =               {431-458},
  year =                {2004},
  month =               may,
  doi =                 {10.1007/s00236-003-0136-5},
  abstract =            {We study the complexity of satisfiability and model
                         checking problems for fragments of linear-time
                         temporal logic with past (PLTL). We consider many
                         fragments of PLTL, obtained by restricting the set
                         of allowed temporal modalities, the use of negations
                         or the nesting of future formulas into past
                         formulas. Our results strengthen the widely accepted
                         fact that {"}past is for free{"}, in the sense that
                         allowing symmetric past-time modalities does not
                         bring additional theoretical complexity. This result
                         holds even for small fragments and even when nesting
                         future formulas into past formulas.},
}