Axiomatising verdict equivalence over regular monitors

Monitors are a key tool in the field of runtime verification, where they are used to check for system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fragment of Milner’s CCS and studied two trace-based notions of equivalence over monitors, namely verdict and ω--verdict equivalence. This talk aims to present the basic notions of this field, study the equational logic of monitors modulo those two notions of equivalence and present some results on equational axiomatisations of verdict and ω--verdict equivalence for closed and open terms over recursion-free monitors.