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.

翻译：运行时验证是一种轻量级验证技术，它通过运行时分析系统执行过程而非预先探索完整系统模型，从而弥补模型检验的不足。该技术尤其适用于部分可观测或黑盒系统——此类系统中的不确定性仅能通过观测来消除。本讲义系统阐述了运行时验证的自动机理论、时序逻辑及认识论基础，涵盖规范形式化方法、诊断、不透明性及可监控性等核心主题，并阐释如何通过离线分析构建能够基于观测执行轨迹进行在线监控的监控器。讲义还探讨了时间扩展特性及其在实时场景中引发的附加算法与语义挑战。