Runtime Verification Through Forward Chaining

TL;DR

This paper introduces a fast, scalable runtime verification method using forward chaining and Horn clauses to efficiently monitor FLTL properties over expanding traces, avoiding complex tableau-based approaches.

Contribution

It presents a novel rule-based, forward chaining approach for runtime verification that simplifies monitoring and improves scalability compared to traditional tableau methods.

Findings

Creates monitors with a single state and fixed rules

Avoids exponential complexity of tableau-based methods

Demonstrates a working implementation of the approach

Abstract

In this paper we present a novel rule-based approach for Runtime Verification of FLTL properties over finite but expanding traces. Our system exploits Horn clauses in implication form and relies on a forward chaining-based monitoring algorithm. This approach avoids the branching structure and exponential complexity typical of tableaux-based formulations, creating monitors with a single state and a fixed number of rules. This allows for a fast and scalable tool for Runtime Verification: we present the technical details together with a working implementation.