Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic

TL;DR

This paper provides a new, more straightforward proof of completeness for finite-trace linear temporal logic (LTLf) by adapting existing methods and explicitly ensuring models are finite.

Contribution

It introduces a novel proof technique that injects finiteness into the model construction, simplifying the completeness proof for LTLf.

Findings

The new proof is more conventional and accessible.

It confirms the completeness of LTLf with fewer axioms.

The approach ensures models are finite, aligning with the logic's semantics.

Abstract

Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Ro\c{s}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\"{o}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.