The Infinite, in Finite Time
2026-08-24 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study how to check if a system behaves correctly over time when only a limited part of its behavior can be seen. They improve a version of Linear-time Temporal Logic (LTL), called LTL3, which helps give clear yes-or-no answers from short observed behaviors. They prove that LTL3 behaves very much like regular LTL and confirm the accuracy of a method used to evaluate these properties during system monitoring. Additionally, the authors explore broader properties about system behaviors, giving precise definitions for when these can be monitored, and organize these into a structured hierarchy. All their work is formally verified using a proof assistant called Isabelle/HOL.
Linear-time Temporal LogicLTL3run-time verificationfinite prefixesformula progressionsafety-liveness decompositionmonitorabilityIsabelle/HOLinfinite tracestopology of traces
Authors
Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
Abstract
Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system's behaviour can be observed. For some properties, these finite prefixes may be definitive---a yes or no answer can be given without further observation. By enriching the semantics of LTL with these definitive prefixes, we give a proper inductive accounting of the semantics of LTL$_3$, a multi-valued variant of Linear-time Temporal Logic for run-time verification applications. The semantic descriptions of LTL$_3$ in previous work are given only in terms of their relationship to conventional LTL. We show that the semantics of LTL and of LTL$_3$ are isomorphic. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification contexts, and show its soundness and completeness up to finite traces with respect to our semantics. Then, we turn to linear-time properties more generally: using our theory of definitive prefixes, we re-prove the well-known safety-liveness decomposition theorem, and reconstruct the topology of infinite traces. We define monitorability for properties, providing neat topological characterisations for various monitorability classes, and arrange them into a hierarchy. All of our definitions and proofs are mechanised in Isabelle/HOL.