An axiomatization of verdict equivalence over regular monitors
share
Monitors are a key tool in the field of runtime verification, where they are used to check for system properties by analysing 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 article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and ω-verdict equivalence for closed and open terms over recursion-free monitors.
READ FULL TEXT