Deep result in monitoring theory [loc-0046]

My student Kai Phan was absolutely on fire this week. About five times I threw out a few idle conjectures I had, and within hours she'd come back with a proof or a counterexample. We made more progress in one week than I had thinking about this stuff for months.

It's well known in the world of runtime verification that the class of monitorable properties (by which I mean the definition used by Bauer, where no monitor will get into an "ugly" state where no informative answer is possible) is larger than the set of safety or guarantee properties, or their boolean combinations (called obligation properties or \Delta _2).

What Kai showed recently is that all monitorable properties are indistinguishable by any monitor from an obligation property. This shows that a lot of the monitorability classes we find in the literature are making a distinction from standard sets in \Delta _2 that is only observable at infinity anyway. So the "largeness" of the monitorability classes is illusory, and obligation properties are all you need.

The proof has been mechanised in Isabelle/HOL, and we have a number of other supporting contributions that I think will make a good paper for POPL or LICS. I'm very proud of Kai's progress so far! I think this result will reinforce her plan for her thesis, which is to semantically tackle revocable monitors (i.e. monitors that can change their mind). Seeing as the difference hierarchy is contained at all finite levels in \Delta _2, we should have an easy time justifying restricting to \Delta _2 properties now.