Synthesising Safety Runtime Enforcement Monitors in μHML

Undergraduate dissertation in computer science, 2019

Cite as: Luke Collins. (2019). Synthesising Safety Runtime Enforcement Monitors in μHML.

PDF download available here.


In this project, we consider a subset $\text{sHML}$ of formulæ in the Hennessy-Milner Logic with recursion ($\mu\text{HML}$) which are enforceable through suppressions. A synthesis function is introduced, which converts safety properties in $\text{sHML}$ to suppression enforcers through a formula normalisation process. This synthesis function assumes that different branches in the input formula are disjoint, and that every variable is guarded by modal necessity—such formulæ are said to be in normal form. It turns out that this restriction of input formulæ is only superficial: an algorithm which converts any given formula in $\text{sHML}$ to an equivalent formula in normal form is implemented in the form of a Haskell program.

Additional Information

I gave a presentation about the topics covered in my dissertation.

Leave a Comment