2014/12/03 by Alan Perotti, Guido Boella, Artur d'Avila Garcez
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.169.8
published as EPTCS 169, 2014, pp. 68-81 · In Proceedings HCVS 2014, arXiv:1412.0825
arxiv created 2014/12/03 · arxiv updated 2014/12/04
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.