Temporal Logic with Forgettable Past

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.

• Type: Conference
• Year: 2002
• Where: LICS
• Authors: François Laroussinie, Nicolas Markey, Ph. Schnoebelen
• Keywords: Automated Reasoning, Forgettable Past, LICS 2002, Linear-time Temporal Logic, Optimal Automata-theoretic Algorithms