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.

image post

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.