Semantics for linear-time temporal logic with finite observations

Rayhana Amjad, Rob van Glabbeek, Liam O'Connor

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProceedings Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics
EditorsGeorgiana Caltais, Cinzia Di Giusto
PublisherOpen Publishing Association
Pages35-50
Number of pages16
DOIs
Publication statusPublished - 20 Nov 2024
EventCombined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics - Calgary, Canada
Duration: 9 Sept 20249 Sept 2024
Conference number: 31/21
https://express-sos.github.io/

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume412
ISSN (Electronic)2075-2180

Workshop

WorkshopCombined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics
Abbreviated titleEXPRESS/SOS 2024
Country/TerritoryCanada
CityCalgary
Period9/09/249/09/24
Internet address

Fingerprint

Dive into the research topics of 'Semantics for linear-time temporal logic with finite observations'. Together they form a unique fingerprint.
  • Definitive set semantics for LTL3

    Amjad, R., van Glabbeek, R. & O'Connor, L., 12 Aug 2024, Archive of Formal Proofs, p. 1-40 40 p.

    Research output: Contribution to specialist publicationArticle

    Open Access

Cite this