## About DecentMon 2

DecentMon 2 is an OCaml Benchmark for Generalized and Efficient Decentralized Monitoring of Regular Languages. A full description of the underlying algorithms and principles are currently being submitted.

DecentMon 2 takes as input:

- a deterministic finite-state automaton to be monitored;
- some traces against the formulae are monitored;
- an architecture given by a distributed alphabet indicating how components are organised and distributed in the system.

DecentMon 2 then outputs:

- verdicts for the monitored formulae against the input traces;
- some monitoring statistics such as:
- the number of messages exchanged by the local monitors,
- the size of messages exchanged by the local monitors,
- the length of the trace needed to reach a verdict,
- the length of the trace needed to reach a verdict,
- the delay induced by decentralised monitoring (average and maximal values when monitorign several formulae), and
- the memory consummed by local monitors.

We also have compared DecentMon 2 with its previous version DecentMon (available at http://decentmonitor.forge.imag.fr) which processes LTL formulae. Several comparison modes were used:

- a) by merging the traces to a single, global trace and then using a “central monitor” for the formula (i.e., all local monitors send their respective events to the central monitor who makes the decisions regarding the trace),
- b) by using the decentralised approach of DecentMon based on LTL formulae (each trace is read by a separate monitor), and
- b) by using the decentralised approach of DecentMon 2 based on automata (each trace is read by a separate monitor).

We have evaluated the three different monitoring approaches (i.e., centralized vs. LTL-decentralized vs generalized-decentralized) using several set-ups. To compare monitoring metrics obtained with the decentralized algorithm of DecentMon and the one of DecentMon 2, we have used LTL2MON (http://ltl3tools.sourceforge.net), which converts any LTL formula into an automata-based (centralized) monitor. For our comparison purposes, we used results on common LTL formulae and traces using the experimental setup depicted in the figure below.