Speaker: Kim Guldstrand Larsen

Title: Timed Monitoring and Monitorability

Abstract: 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. 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. 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. 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.