Runtime verification of temporal properties over timed observations is essential in cyber-physical systems such as autonomous vehicles, smart grids, and medical devices. This talk presents recent advances in predicting property satisfaction or violation in continuous real-time settings. We focus on monitoring properties expressed in Metric Interval Temporal Logic (MITL) or Timed Büchi Automata [2, 4]. Our symbolic online algorithms exploit zone-based techniques from Timed Automata model checking, enabling efficient handling of challenges like time divergence, timing uncertainty, and fluctuating parametric delays–without relying on costly parametric verification. Assumptions about system behavior, expressed as Timed Automata, can further enhance monitoring [1]. We propose an assumption-based runtime verification framework and discuss its extension to probabilistic settings using Stochastic Timed Automata. Implemented in UPPAAL, our algorithms show promising initial results. Finally [3], we also present new findings on monitorability, showing decidability and computable verdict bounds for deterministic Timed Muller Automata, while proving undecidability for nondeterministic Timed Büchi Automata. In addition we introduce and settle decidability of step- and time-bounded monitorability.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Timed Monitoring and Timed Monitorability

  • Kim Guldstrand Larsen

摘要

Runtime verification of temporal properties over timed observations is essential in cyber-physical systems such as autonomous vehicles, smart grids, and medical devices. This talk presents recent advances in predicting property satisfaction or violation in continuous real-time settings. We focus on monitoring properties expressed in Metric Interval Temporal Logic (MITL) or Timed Büchi Automata [2, 4]. Our symbolic online algorithms exploit zone-based techniques from Timed Automata model checking, enabling efficient handling of challenges like time divergence, timing uncertainty, and fluctuating parametric delays–without relying on costly parametric verification. Assumptions about system behavior, expressed as Timed Automata, can further enhance monitoring [1]. We propose an assumption-based runtime verification framework and discuss its extension to probabilistic settings using Stochastic Timed Automata. Implemented in UPPAAL, our algorithms show promising initial results. Finally [3], we also present new findings on monitorability, showing decidability and computable verdict bounds for deterministic Timed Muller Automata, while proving undecidability for nondeterministic Timed Büchi Automata. In addition we introduce and settle decidability of step- and time-bounded monitorability.