Kai Phan has been building on her already very impressive result to produce a very nice picture of the monitorability landscape. I will present a brief summary of her results here, but eventually they will be incorporated into my research notebook on linear-time temporal properties. Mostly, our results concern the space of program properties — sets of program behaviours.
The classes of safety and guarantee above are the familiar closed and open sets respectively in the topology of program behaviours. In the above diagram, decision properties are the clopen sets — those sets that are both Safety properties and Guarantee properties, and obligation properties are, following Amir Pnueli, any boolean combination of closed or open sets.
Kai's original result was to show that all Bauer monitorable properties — that is, all properties for which a monitor can always potentially give an answer — cannot be distinguished from an obligation property by any monitor observing finite prefixes. What she has now done is prove that Bauer monitorable properties are exactly those properties that approximate an obligation property in this way. This led us to re-christen Bauer monitorability as the class of quasi-obligation properties. In a similar way, she has also identified the classes of quasi-safety and quasi-guarantee, which cannot be monitorably distinguished from safety and guarantee properties respectively, and proved that quasi-obligation properties are exactly those that are made up of boolean combinations of these.
At the bottom of the prism, we have another set of classes. What is commonly called weak monitorability sits at the very bottom — those properties for which there is at least one finite prefix that causes a monitor to give a definitive answer. We also have good monitorability and bad monitorability, which are those properties with at least one good or bad prefix respectively. It is easy to see that weak monitorability is the union of these classes. (Taking boolean combinations, as in the higher levels of the cube, leads to a trivial class containing all properties).
Kai has also now defined CTL characterisations for all of these lower classes, expressed as formulae over monitor trees, which we define reminiscent of Ghani, Hancock and Pattinson's stream processors. She then showed that the CTL formulae for all of the middle layer classes of the prism are obtained by wrapping the corresponding formula for the class below with \mathbf {AG}. For example, weak monitorability is defined as \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}), and quasi-obligation is just \mathbf {AG}\ \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}). Because of the aforementioned indistinguishability result (and because indistinguishable properties have indentical monitors), it's not possible to write CTL formulae for the top level of the prism, except for Decision properties (clopen sets) which correspond exactly to those monitors described by inductive trees — where all paths eventually terminate with an answer.
We're aiming to get this into ESOP or FoSSaCS this year. Hoping for the best! I think this is great work.