Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
Logic in Computer Science
2021-07-14 v1
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.
Keywords
Cite
@article{arxiv.2107.06045,
title = {Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic},
author = {Eric Campbell and Michael Greenberg},
journal= {arXiv preprint arXiv:2107.06045},
year = {2021}
}