From first-order temporal logic to parametric trace slicing

Giles Reger*, David Rydeheard

*Corresponding author for this work

    Research output: Chapter in Book/Conference proceedingConference contributionpeer-review

    Abstract

    Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper considers the relationship between two widely-used specification approaches to parametric runtime verification: trace slicing and first-order temporal logic. This work is a first step in understanding this relationship. We introduce a technique of identifying syntactic fragments of temporal logics that admit notions of sliceability. We show how to translate formulas in such fragments into automata with a slicing-based semantics. In exploring this relationship, the paper aims to allow monitoring techniques to be shared between the two approaches and initiate a wider effort to unify specification languages for runtime verification.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    PublisherSpringer Nature
    Pages216-232
    Number of pages17
    Volume9333
    ISBN (Print)9783319238197
    DOIs
    Publication statusPublished - 2015
    Event6th International Conference on Runtime Verification, RV 2015 - Vienna, Austria
    Duration: 22 Sept 201525 Sept 2015

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume9333
    ISSN (Print)03029743
    ISSN (Electronic)16113349

    Conference

    Conference6th International Conference on Runtime Verification, RV 2015
    Country/TerritoryAustria
    CityVienna
    Period22/09/1525/09/15

    Fingerprint

    Dive into the research topics of 'From first-order temporal logic to parametric trace slicing'. Together they form a unique fingerprint.

    Cite this