2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/32617This 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 pagesLogic in Computer ScienceF.4.1; F.3.1text