Our student Rayhana Amjad has published her first paper recently, presenting our work on LTL semantics with respect to finite partial traces. This work is a result of our trying to investigate the semantic properties of LTL when applied to testing in the context of the Quickstrom project. Congratulations to Rayhana and thanks also go to Rob van Glabbeek, her secondary supervisor and co-author of this work.

Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
Semantics for Linear-time Temporal Logic with Finite Observations Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS), pp. 35-50, Calgary, Canada, September 2024
Available from ETPCS

LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.

The Isabelle/HOL proofs can be found at The Archive of Formal Proofs.