Runtime Verification: Monitoring, Knowledge, and Uncertainty (Lecture Notes)
It provides a comprehensive tutorial for researchers and practitioners needing formal foundations for monitoring partially observable or black-box systems.
This work presents automata-theoretic, temporal-logical, and epistemic foundations for runtime verification, covering specification, diagnosis, opacity, and monitorability, including timed extensions.
Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model in advance. It is particularly useful for partially observable or black-box systems, where uncertainty can only be resolved through observation. These lecture notes present automata-theoretic, temporal-logical, and epistemic foundations of runtime verification. They cover specification formalisms, diagnosis, opacity, and monitorability, and explain how offline analysis can be used to construct monitors that operate online on observed executions. The notes also discuss timed extensions and the additional algorithmic and semantic challenges that arise in the real-time setting.