Computer says no : verdict explainability for runtime monitors using a local proof

Abstract

Monitors in Runtime Verification are often constructed as black boxes: they provide verdicts on whether a property is satisfied or violated by the executing system under scrutiny, without much explanation as to why this is the case. In the best of cases, monitors might also return the trace observed, still leaving it up to the user to figure out the logic employed to reach the declared verdict from this trace. In this paper, we propose a local proof system for Linear Temporal Logic—a popular logic used in Runtime Verification—formalising the symbolic deductions within the constraints of Runtime Verification. We prove novel soundness and partial completeness results for this proof system with respect to the original semantics of the logic. Crucially, we show how such a deductive system can be used as a realistic basis for constructing online runtime monitors that provide explanations for their verdicts; we also show the resulting monitor algorithms to satisfy pleasing correctness criteria identified by other works, such as the decidability and incrementality of the analysis and the irrevocability of verdicts. Finally, we relate the expressiveness of the Linear Temporal Logic proof system to existing symbolic analysis techniques used in Runtime Verification.