Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Semantics for Linear-time Temporal Logic with Finite Observations

Rayhana Amjad, Rob van Glabbeek, Liam O'Connor

TL;DR

It is shown that the definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby it is shown that the semantics of LTL3 directly correspond to the semantics of conventional LTL.

Abstract

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.

Semantics for Linear-time Temporal Logic with Finite Observations

TL;DR

It is shown that the definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby it is shown that the semantics of LTL3 directly correspond to the semantics of conventional LTL.

Abstract

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.

Paper Structure

This paper contains 15 sections, 11 theorems, 30 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Linear-time Temporal Logic
  3. Definitive Prefix Sets
  4. Lattice Properties
  5. Isomorphism to Linear-time Temporal Properties
  6. Semantics of LTL and LTL$_3$
  7. Answer-indexed Families
  8. The Prepend Operation
  9. Semantics for LTL$_3$
  10. Formula Progression
  11. Discussion
  12. Prefix Characterisations and Monitorability
  13. Safety and Liveness
  14. RV-LTL
  15. Conclusion

Key Result

Theorem 1

The definitive union gives least upper bounds for definitive sets ordered by set inclusion, i.e., for a set $S \subseteq \mathcal{D}$ of definitive sets:

Figures (5)

  • Figure 1: Syntax of LTL
  • Figure 2: Semantics of conventional LTL
  • Figure 3: LTL semantics using answer-indexed families
  • Figure 4: LTL$_3$ semantics using answer-indexed families
  • Figure 5: Rules for formula progression

Theorems & Definitions (22)

  • Theorem 1
  • proof
  • Theorem 2
  • proof
  • Theorem 3
  • proof
  • Theorem 4: Equivalence to conventional semantics
  • proof
  • Theorem 5
  • proof
  • ...and 12 more