Title :
Temporal logic with forgettable past
Author :
Laroussinie, François ; Markey, Nicolas ; Schnoebelen, Philippe
Author_Institution :
Lab. Specification et Verification, ENS de Cachan, France
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.
Keywords :
automata theory; computability; computational complexity; temporal logic; EXPSPACE-complete problems; NLTL; forgettable past; linear-time temporal logic; model checking; optimal automata-theoretic algorithms; satisfiability; Automatic logic units; Computer science; Polynomials;
Conference_Titel :
Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on
Print_ISBN :
0-7695-1483-9
DOI :
10.1109/LICS.2002.1029846
