Epistemic dynamic logic models noisy runtime verification monitorability
A Formal Framework for Noisy Runtime Verification
Logic in Computer Science
Summary
Computers often check their behavior while running, but noise or errors can make this hard. The paper presents a new logic called EDMon that helps describe and understand how to monitor programs even when the observations are noisy. The authors show how EDMon captures many existing ideas in noisy runtime verification and connects to related logics. This helps clarify what can and cannot be reliably monitored under noisy conditions.
What this means in practice
- •For software verification engineers: Specify and reason about what program properties can be monitored reliably when system observations are noisy or imperfect.
- •For sensor system designers: Understand and formalize limits of monitoring systems when sensors produce noisy or uncertain data.
A theory result. No direct application yet.
Authors
Shay Allen Logan, Shawn Standefer, Thomas Ferguson
Abstract
We introduce the logic EDMon---an epistemic dynamic logic meant to model monitorability concepts in noisy runtime verification. Its syntax and semantics are defined and explained and the connection between EDMon and monitorability and noisy runtime verification concepts is explored. We then demonstrate that EDMon is sufficient to capture many of the results in the noisy runtime verification literature and catalog its relation to nearby logics and describe a large class of its theorems.