2021/07/13 by Eric G. Campbell, Michael Greenberg, Campbell, Eric +2
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2107.06045
openalex publication_date 2021/07/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Roşu first proved completeness for linear temporal logic on finite traces (LTLf) with a novel coinductive axiom. We offer a different proof, with fewer, more conventional axioms. Our proof is a direct adaptation of Kröger and Merz's Henkin-Hasenjaeger-style proof. The essence of our adaption is that we "inject" finiteness: that is, we alter the proof structure to ensure that models are finite. We aim to present a thorough, accessible proof.