## 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: |