Past is for free: on the complexity of verifying linear temporal properties with past

We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (pltl). More precisely, we consider several fragments of pltl, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments.

• Type: Journal
• Year: 2004
• Where: ACTA
• Authors: Nicolas Markey
• Keywords: ACTA 2004, Additional Theoretical Complexity, Future Formulae, Linear-time Temporal Logic