2005/02/28 by Riccardo Pucella
Computer Science · #cs.LO
published as SIGACT News, 36(1), pp. 86-99, 2005 · 14 pages
arxiv created 2005/04/24 · arxiv updated 2009/12/01
This article examines the interpretation of the LTL temporal operators over finite and infinite sequences. This is used as the basis for deriving a sound and complete axiomatization for Caret, a recent temporal logic for reasoning about programs with nested procedure calls and returns.