形式陈述
监控一条观测轨迹
运行时验证接收系统产生的有限事件前缀
并用监控器更新状态。与路径语义中的全行为集合不同，它只观察本次运行已发生的事件，不能直接量化其他未执行路径。
对 regular finite-trace property，可由有限状态自动机实现监控器：
状态摘要此前全部相关历史，使每个新事件只需局部更新。若性质需要无界数据关联，纯有限状态监控器不够，需寄存器、参数化实例或外部存储。
监控器 determinization 可让每个事件只有一个下一状态，便于在线常数时间更新；由 LTL/正则表达式生成的 automaton 可能指数增长。保持 NFA state set 可延迟确定化，但每步需更新一组候选状态。
事件 alphabet 必须包含足够观察。只记录 grant 而不记录对应 request id，无法验证一一响应；加入所有 payload 又可能造成无限字母表，需要 symbolic guard 或参数化 monitor。
三值前缀语义
对无限行为性质，有限前缀常既未证明满足也未证明违反。三值语义可返回
若前缀所有延伸都满足，返回 true；若所有延伸都违反，返回 false；否则 inconclusive。
安全性质 G not bad 一旦观察到 bad 就永久 false，却通常无法在持续系统的任意安全前缀上返回永久 true。co-safety 性质 F done 看到 done 后可永久 true，却无法因暂未看到而返回 false。
把 inconclusive 当作通过，会把尚未发生的活性义务误判为已兑现。
下图只表示单个已登记 request(7) 的一次有限任务：grant(7) 完成这个任务，end 则把仍未完成的任务判失败。它的绿色终态不声称整个持续系统今后永远满足所有请求响应义务；后续新请求必须另建或重启相应监控实例。
本页采用常见的 Bauer–Leucker–Schallhart 式 monitorability：对每个有限前缀
有限 trace 语义可以强制日志结束时评价所有义务，但这改变了原无限规格。end 是真实系统终止事件、观测窗口关闭还是日志丢失，必须区分。
直觉
请求—响应状态轨迹
监控 G(request -> F grant) 时，可维护 outstanding request 集。事件 request(id) 加入 id，grant(id) 删除对应 id。
轨迹
request(7), request(9), grant(7)结束时 id 9 仍 outstanding。若日志截断只是观察暂时停止，结论是 inconclusive；若 end 表示系统正式终止，有限 trace 语义可判违反。
只维护一个布尔 pending 会把多个并发请求合并，grant(7) 可能错误清除 request(9) 的义务。监控状态必须匹配事件参数和需求的关联量词。
参数化监控通常为每个 id 建实例。实例可在义务完成后回收，但若性质还允许未来事件引用旧 id，过早 GC 会漏违反；回收条件需从 automaton 的终态和参数作用域证明。
高基数攻击者可不断制造新 id 使监控表无界。容量保护应发出 overflow/unknown，并记录丢弃范围，不能静默淘汰后继续返回 true。
例子与边界
Instrumentation 与观察缺口
监控正确性分两层：从完整事件序列到 verdict 的 automaton 正确；instrumentation 还要保证真实相关事件都被捕获、顺序和参数准确。
异步日志可能重排跨线程事件，采样会漏事件，时钟漂移会改变实时约束。监控器对输入 trace 的正确结论，不能补偿 trace 本身不忠实。
插桩也可能改变调度，隐藏原竞态或引入延迟。低开销与可观察完整性是工程权衡，应在保证中说明 drop policy。
分布式日志只有偏序。不同节点时间戳不能在有漂移时直接给出真实全序；监控器可枚举与 happens-before 一致的线性化，或使用 partial-order semantics。任取一个排序可能把“先认证后访问”判反。
网络重复、重传和 exactly-once 假设也影响事件语义。若同一 logical request 出现两条日志，监控需用唯一标识去重，不能把它们当两个独立义务。
推论与应用
在线、离线与可执行动作
在线监控随系统运行，能及时告警或触发恢复；离线监控分析已保存日志，可用更多内存和双向扫描。两者使用同一性质也可能因日志结束语义不同给出不同 verdict。
enforcement monitor 若阻止、延迟或改写动作，已从观察升级为控制。只有可通过此类编辑保持的性质才能透明 enforcement，且干预本身要进入系统语义。
实时监控使用 event time 还是 processing time 会改变窗口。迟到事件的 watermark 策略必须说明何时关闭窗口；关闭后到达的合法 grant 若被丢弃，可能产生假警报。
对 duration 约束，单调时钟、时钟回拨和跨机同步误差需要预算。普通事件自动机没有这些数值时间假设。
边界
一次运行通过不能证明所有未来或所有输入都通过。运行时验证补充静态证明与模型检查，主要价值是对部署中的实际 trace 给出形式化诊断。
监控器内存也可能无界，例如要关联任意多未完成请求。给表设置容量并丢弃旧义务会改变 soundness；应返回 unknown/overflow，而非继续声称完整验证。
监控器本身可通过模型检查、代码生成证明或 differential testing 验证。若 specification compiler 有 bug，同一错误可能同时存在于生成器和测试 oracle；保留独立语义解释器或证书能缩小共同失效。
隐私场景中对 payload 脱敏可能删除验证所需关系。应先证明抽象事件映射保存性质，再应用最小化，而不是事后发现监控无法区分关键状态。
参考资料
- Andreas Bauer, “Monitorability of ω-regular languages”, 2010：每个有限前缀具有某个可决定的有限扩展这一量词约定。
- Martin Leucker and Christian Schallhart, “A Brief Account of Runtime Verification,” Journal of Logic and Algebraic Programming 78(5), 2009, pp. 293–303。
- Andreas Bauer, Martin Leucker, and Christian Schallhart, “Runtime Verification for LTL and TLTL,” ACM TOSEM 20(4), 2011, Article 14。
- Ezio Bartocci et al., “Specification-Based Monitoring of Cyber-Physical Systems: A Survey,” in Lectures on Runtime Verification: Introductory and Advanced Topics, LNCS 10457, Springer, 2018, pp. 135–175。