Kai Phan very impressive result research notebook properties behaviours
The classes of safety guarantee topology of program behaviours decision properties are the clopen sets — those sets that are both Safety properties Guarantee properties obligation properties are, following Amir Pnueli
Kai's original result 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 bad 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 Pattinson stream processors \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.