Something went wrong. Try again.
my forest
Something went wrong. Try again.
1234567\author{liamoc}\date{2026-04-26}\title{Deep result in monitoring theory}\p{My student [[kaiphan]] 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.}\p{It's well known in the world of runtime verification that the class of \em{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](ltp-0004) or [guarantee](ltp-0005) properties, or their boolean combinations (called \em{obligation} properties or #{\Delta_2}).}\p{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 \em{only observable at infinity anyway}. So the "largeness" of the monitorability classes is illusory, and obligation properties are all you need.}\p{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 \em{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.}