DecentMon: An OCaml Benchmark for Decentralised LTL Monitoring

DecentMon is an open-source OCaml benchmark for Decentralised LTL monitoring.

DecenMon simulates the verfication of LTL formulae at runtime on a distributed system in a decentralised fashion.

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.

One can consult this website for more information on DecentMon.