FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Counting Semantics for Monitoring LTL Specifications over Finite Traces

Authors: Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck

Paper Information

Title:A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Authors:Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Specification-based monitoring, Runtime Verification, Quantitative Semantics for Temporal Logic
Abstract:

ABSTRACT. We consider the problem of monitoring a Linear Time Logic (LTL) specification that is defined on infinite paths, over finite traces. For example, we may need to draw a verdict on whether the system satisfies or violates the property p holds infinitely often.'' The problem is that there is always a continuation of a finite trace that satisfies the property and a different continuation that violates it.

We propose a two-step approach to address this problem. First, we introduce a counting semantics that computes the number of steps to witness the satisfaction or violation of a formula for each position in the trace. Second, we use this information to make a prediction on inconclusive suffixes. In particular, we consider a \emph{good} suffix to be one that is shorter than the longest witness for a satisfaction, and a \emph{bad} suffix to be shorter than or equal to the longest witness for a violation. Based on this assumption, we provide a verdict assessing whether a continuation of the execution on the same system will presumably satisfy or violate the property.

Pages:17
Talk:Jul 15 12:15 (Session 103A: Runtime Verification, Hybrid and Timed Systems)
Paper: