Temporal logic with forgettable past
Authors:
Open Access
- 1 January 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 383-392
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
This publication has 21 references indexed in Scilit:
- Extended Temporal Logic Revisited2001
- Specification in CTL+Past for Verification in CTLInformation and Computation, 2000
- A hierarchy of temporal logics with pastTheoretical Computer Science, 1995
- A decision algorithm for full propositional temporal logicLecture Notes in Computer Science, 1993
- The Temporal Logic of Reactive and Concurrent Systems1992
- A temporal fixpoint calculus1988
- The complementation problem for Büchi automata with applications to temporal logicTheoretical Computer Science, 1987
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- The glory of the past1985
- Alternating finite automata on ω-wordsTheoretical Computer Science, 1984