Runtime Verification Through Forward Chaining
Logic in Computer Science
2014-12-04 v1
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.
Cite
@article{arxiv.1412.1156,
title = {Runtime Verification Through Forward Chaining},
author = {Alan Perotti and Guido Boella and Artur d'Avila Garcez},
journal= {arXiv preprint arXiv:1412.1156},
year = {2014}
}
Comments
In Proceedings HCVS 2014, arXiv:1412.0825