Temporal Logic with Forgettable Past

F. Laroussinie N. Markey Ph. Schnoebelen

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002

Abstract

We investigate NLTL, a temporal logic with forgettable past. We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems. We also prove a succinctness gap between NLTL and LTL+Past, and between LTL+Past and LTL partly answering a folk conjecture.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:31
Maintainer lics02@dcs.ed.ac.uk.
Start Conference Manager
Conference Systems