Examples

We have evaluated the centralised and decentralised monitoring approaches using several set-ups described in the following. For a given formula and a given trace, the formula is monitored twice:

  • 1) by using a central observer to which all monitors report their observation, and
  • 2) without using a central observer and making monitors communicate according to the decentralised monitoring algorithm.

We conducted further experiments to determine which are the parameters that make decentralised monitoring (less) effective w.r.t. a centralised solution, and whether or not the user can control them or at least estimate them prior to monitoring. To this end, we first considered a policy change for sending messages: Under the new policy, components send messages to the central observer only when the truth values have changed w.r.t. a previous event.

We then extended this setting by considering specific probability distributions 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.

In most benchmarks, we are particularly interested by two metrics:

  • The average length of the traces needed to reach a verdict denoted by |trace|.
  • The number of messages, # msg., in the centralised setting, corresponds to the number of events sent by the local monitors to the central monitor (i.e., |trace| × |Decentralised alphabet|), and in the decentralised setting to the number of obligations transmitted between local monitors.

Some benchmarks are also related to another important monitoring statistics which is the delay (in the sense of trace length) induced by decentralised monitoring to reach a verdict. DecentMon provides the average delay and the maximal delay obtained when monitoring several formulae.

Below you can find some of the benchmarks we conducted.
Click on the pictures to enlarge them

Create also you own benchmarks and share them with us! We will put them on the Website !

Note that some of the pictures of benchmarks where taken using version 1.0 of DecentMon. Although, the syntax to reproduce them is provided for the latest version of DecentMon.

Benchmarks for randomly generated LTL formulae

For randomly generated formulae, we conducted several benchmarks:

  • A benchmark that shows how the size of the formula influence the metrics for the distributed alphabet {a|b|c}. For each size, DecentMon monitors 1000 randomly generated formulae against 1000 randomly generated traces.
    This benchmark can be invoked using the following command:
    decentmon -n 1000 -msf 6 -st 1000 -dalpha "{a|b|c}" -prt_full true bench1
  • A benchmark with the same previous set-up, but for a larger alphabet {a1,a2|b1,b2|c1,c2} and we reduced the number of formulae tested to 500.
    This benchmark can be invoked using the following command:
    decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true bench2
  • A benchmark with the same previous set-up, but with a more distributed version of the previous alphabet: {a1|a2|b1|b2|c1|c2}.
    This benchmark can be invoked using the following command:
    decentmon -n 500 -msf 6 -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true bench3

Benchmarks for LTL specification patterns

For LTL specification patterns, we conducted several benchmarks:

  • A benchmark that experiments on all specification patterns. For each specification pattern, DecentMon monitors 1000 generated formulae against 1000 randomly generated traces. The distributed alphabet used is "{a|b|c}". The length of each freshly generated trace is 1000 events.
    This benchmark can be invoked using the following command:
    decentmon -n 1000 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a|b|c}" -prt_full true bench2-1
  • A benchmark with the same previous set-up, but for a larger alphabet {a1,a2|b1,b2|c1,c2} and we reduced the number of formulae tested to 500.
    This benchmark can be invoked using the following command:
    decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true bench-2-2
  • A benchmark with the same previous set-up, but with a more distributed version of the previous alphabet: {a1|a2|b1|b2|c1|c2}.
    This benchmark can be invoked using the following command:
    decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true bench2-3
  • A benchmark dedicated to bounded existence patterns, a particularly heavy one! The distributed alphabet used is "{a|b|c}". The length of each freshly generated trace is 1000 events. For this specification pattern, we monitored 500 formulae against 500 traces.
    This benchmark can be invoked using the following command:
    decentmon -n 500 -bexis true -st 1000 -dalpha "{a|b|c}" -prt_full true bench-boundedexistence

Benchmarks for randomly generated LTL formulae
- - "send by need" policy used in the centralised case

For randomly generated formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before.

  • decentmon -n 1000 -msf 6 -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes random-onlychange-1
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes random-onlychange-2
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes random-onlychange-3
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes random-onlychange-4

Benchmarks for LTL specification pattern formulae
- - "send by need" policy used in the centralised case

For LTL specification pattern formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before.

  • decentmon -n 1000 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes pattern-onlychange-1
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes pattern-onlychange-2
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes pattern-onlychange-3
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes pattern-onlychange-4

Benchmarks for randomly generated LTL formulae
- - "send by need" policy used in the centralised case
- - bernouilli probability distribution 0.1

For randomly generated formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before. Commands and parameters to invoke them is indicated in the screenshot. Below you can find only some benchmarks using the bernouilli probability distribution (some other probability distribution can be invoked -- see the features of DecentMon).

  • decentmon -n 1000 -msf 6 -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes -bernouilli 0.1 random-onlychange-bernouilli01-1
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes -bernouilli 0.1 random-onlychange-bernouilli01-2
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes -bernouilli 0.1 random-onlychange-bernouilli01-3
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes -bernouilli 0.1 random-onlychange-bernouilli01-4

Benchmarks for LTL specification pattern formulae
- - "send by need" policy used in the centralised case
- - bernouilli probability distribution 0.1

For LTL specification pattern formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before.

  • decentmon -n 1000 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes -bernouilli 0.1 pattern-onlychange-bernouilli01-1
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes -bernouilli 0.1 pattern-onlychange-bernouilli01-2
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes -bernouilli 0.1 pattern-onlychange-bernouilli01-3
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes -bernouilli 0.1 pattern-onlychange-bernouilli01-4

Benchmarks for randomly generated LTL formulae
- - "send by need" policy used in the centralised case
- - bernouilli probability distribution 0.01

For randomly generated formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before.

  • decentmon -n 1000 -msf 6 -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes -bernouilli 0.01 random-onlychange-bernouilli001-1
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes -bernouilli 0.01 random-onlychange-bernouilli001-2
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes -bernouilli 0.01 random-onlychange-bernouilli001-3
  • decentmon -n 500 -msf 6 -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes -bernouilli 0.01 random-onlychange-bernouilli001-4

Benchmarks for LTL specification pattern formulae
- - "send by need" policy used in the centralised case
- - bernouilli probability distribution 0.01

For LTL specification pattern formulae, we conducted several benchmarks. The benchmarks vary in their parameters used as before.

  • decentmon -n 1000 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 1000 -dalpha "{a|b|c}" -prt_full true -only_changes -bernouilli 0.01 pattern-onlychange-bernouilli001-1
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2|b1,b2|c1,c2}" -prt_full true -only_changes -bernouilli 0.01 pattern-onlychange-bernouilli001-2
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1|a2|b1|b2|c1|c2}" -prt_full true -only_changes -bernouilli 0.01 pattern-onlychange-bernouilli001-3
  • decentmon -n 500 -abs true -exis true -univ true -prec true -resp true -precc true -respc true -consc true -st 200 -dalpha "{a1,a2,a3|b1,b2,b3|c1,c2,c3}" -prt_full true -only_changes -bernouilli 0.01 pattern-onlychange-bernouilli001-4