DecenMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae. For a full description of the underlying algorithms and principles, we refer the reader to the associated technical report.
DecentMon takes as input:
- some LTL formulae to be monitored or some LTL Specification patterns (see the Specification Patterns Website);
- some traces against the formulae are monitored;
- an architecture given by a distributed alphabet indicating how components are organised and distributed in the system.
Note that the two first inputs are not mandatory. One can simply indicate a size for a formula that will be automatically generated. Similarly, a size can be indicated for a trace to be automatically generated. Also note that trivial formulae (that can be simplified in either the LTL formulae True or False) are automatically discarded.
Note also that several probability distributions can be used for the occurrence of local propositions. Currently, the probability distributions supported by DecentMon are the following:
- "Flipcoin distribution": the occurence of each atomic proposition in an event has a probability of 1/2
- Bernouilli distribution (parameterized by a float 0 < p < 1): the occurence of each atomic proposition in an event has a probability of p
- Exponential distribution (of parameter lambda), see link for a description of its behavior.
DecentMon 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 length of the trace needed to reach a verdict, and
- the delay induced by decentralised monitoring (average and maximal values when monitorign several formulae).
During a benchmark, LTL formulae are analysed in two different modes:
- a) by using the decentralised approach described above (i.e., each trace is read by a separate monitor), and
- b) 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).