Logic Column 11: The Finite and the Infinite in Temporal Logic
<|reference_start|>Logic Column 11: The Finite and the Infinite in Temporal Logic: 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.<|reference_end|>
@article{pucella2005logic,
    title={Logic Column 11: The Finite and the Infinite in Temporal Logic},
    author={Riccardo Pucella},
    journal={SIGACT News, 36(1), pp. 86-99, 2005},
    year={2005},
    archivePrefix={arXiv},
    eprint={cs/0502031},
    primaryClass={cs.LO}
}