Definitive set semantics for LTL3

Rayhana Amjad; Rob van Glabbeek; Liam O'Connor

Definitive set semantics for LTL3

Rayhana Amjad, Rob van Glabbeek, Liam O'Connor

Research output: Contribution to specialist publication › Article

Abstract

LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications, originally due to Bauer et al. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. In this submission, which accompanies our EXPRESS/SOS 2024 paper, "Semantics for Linear-time Temporal Logic with Finite Observations", we instead give 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 originally due to Kabanza et al., popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics.

Original language	English
Pages	1-40
Number of pages	40
Specialist publication	Archive of Formal Proofs
Publication status	Published - 12 Aug 2024

Keywords / Materials (for Non-textual outputs)

logic
general logic
temporal logic
computer science
concurrency
semantics and reasoning

Access to Document

https://www.isa-afp.org/entries/LTL3_Semantics.htmlLicence: All Rights Reserved

1 Conference contribution

Semantics for linear-time temporal logic with finite observations
Amjad, R., van Glabbeek, R. & O'Connor, L., 20 Nov 2024, Proceedings Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics. Caltais, G. & Di Giusto, C. (eds.). Open Publishing Association, p. 35-50 16 p. (Electronic Proceedings in Theoretical Computer Science; vol. 412).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

Cite this

@misc{5033721cc1e749edb2e8adce12965f1e,

title = "Definitive set semantics for LTL3",

abstract = "LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications, originally due to Bauer et al. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. In this submission, which accompanies our EXPRESS/SOS 2024 paper, {"}Semantics for Linear-time Temporal Logic with Finite Observations{"}, we instead give 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 originally due to Kabanza et al., popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics.",

keywords = "logic, general logic, temporal logic, computer science, concurrency, semantics and reasoning",

author = "Rayhana Amjad and {van Glabbeek}, Rob and Liam O'Connor",

year = "2024",

month = aug,

day = "12",

language = "English",

pages = "1--40",

journal = "Archive of Formal Proofs",

issn = "2150-914x",

}

TY - GEN

T1 - Definitive set semantics for LTL3

AU - Amjad, Rayhana

AU - van Glabbeek, Rob

AU - O'Connor, Liam

PY - 2024/8/12

Y1 - 2024/8/12

N2 - LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications, originally due to Bauer et al. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. In this submission, which accompanies our EXPRESS/SOS 2024 paper, "Semantics for Linear-time Temporal Logic with Finite Observations", we instead give 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 originally due to Kabanza et al., popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics.

AB - LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications, originally due to Bauer et al. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. In this submission, which accompanies our EXPRESS/SOS 2024 paper, "Semantics for Linear-time Temporal Logic with Finite Observations", we instead give 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 originally due to Kabanza et al., popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics.

KW - logic

KW - general logic

KW - temporal logic

KW - computer science

KW - concurrency

KW - semantics and reasoning

M3 - Article

SN - 2150-914x

SP - 1

EP - 40

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

ER -

Definitive set semantics for LTL3

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Research output

Semantics for linear-time temporal logic with finite observations

Cite this