Axiomatizing recursion-free, regular monitors

TL;DR

This paper develops complete axiomatizations for the equivalence relations of verdict and ω-verdict in recursion-free monitors used in runtime verification, highlighting limitations in finite axiomatizations.

Contribution

It provides the first complete equational axiomatizations for verdict and ω-verdict equivalence in recursion-free monitors, and shows the non-existence of finite axiomatizations under certain conditions.

Findings

Complete axiomatizations for verdict and ω-verdict equivalence are presented.

Verdict equivalence cannot be finitely axiomatized over open monitors with multiple actions.

The study advances the theoretical understanding of monitor equivalences in runtime verification.

Abstract

Monitors are a key tool in the field of runtime verification, where they are used to verify 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 $\omega$-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 $\omega$-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.