Axiomatizing recursion-free, regular monitors

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 fra...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logical and algebraic methods in programming 2022-06, Vol.127, p.100778, Article 100778
Main Authors: Aceto, Luca, Achilleos, Antonis, Anastasiadi, Elli, Ingolfsdottir, Anna
Format: Article
Language:English
Subjects:
Axiomatization
Equational logic
Formal verification
Monitors
Process algebra
Verdict equivalence
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 ω-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. 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.
ISSN:2352-2208
DOI:10.1016/j.jlamp.2022.100778