What Can We Monitor Over Unreliable Channels?

This article addresses the question of what properties can be monitored over an unreliable communication channel. We model unreliable communications as mutations to finite traces and define what it means for a property to be immune to such a mutation. We also introduce the idea of a trustworthy verdict, which is a verdict guaranteed to be correct in the presence of a trace mutation. We show that the trustworthiness of a verdict or immunity of a property for a single mutation is equivalent to the trustworthiness or immunity for any number of mutations. We classify trustworthy verdicts on ω-regular properties by updating a recently proposed monitorability-focused refinement of the safety-liveness taxonomy. The article also includes a fixed-parameter tractable algorithm to test an ω-regular property for immunity to a trace mutation. Our results show that many of the most common properties can be monitored over unreliable channels.