Skip to main content

Accelerated Runtime Verification of LTL Specifications with Counting Semantics

Publication Type
Year of Publication
Conference/Journal Name
International Conference on Runtime Verification (RV)
This paper presents a novel and efficient parallel algorithm for runtime verification of an extension of LTL that allows for nested
quantifiers subject to numerical constraints. Such constraints are useful in evaluating thresholds (e.g., expected uptime of a web server). Our algorithm uses the MapReduce programming model to split a program trace into variable-based clusters at run time. Each cluster is then mapped to its respective monitor instances, verified, and reduced collectively on a multi-core CPU or the GPU. Our experiments on real-world case studies show that the algorithm imposes negligible monitoring overhead.