Logic Column 11: The Finite and the Infinite in Temporal Logic
arXiv:cs/0502031
Abstract
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.
14 pages