Decentralised Runtime Verification of Timed Regular Expressions

Our paper Decentralised Runtime Verification of Timed Regular Expressions has been accepted for publication in TIME 2022, the 29th International Symposium on Temporal Representation and Reasoning.

The abstract of the paper is below:

Ensuring the correctness of distributed cyber-physical systems at runtime requires monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. Since there is no approach for monitoring global timed properties in this decentralised setting, we introduce a monitoring framework for timed properties described by timed regular expressions over a distributed network of monitors. First, we define functions to rewrite expressions according to partial knowledge for both the centralised and decentralised cases. Then, we define decentralised algorithms for monitors to evaluate properties using these functions. Finally, we implement and evaluate our framework on synthetic timed regular expressions, giving insights on the cost of the centralised and decentralised settings and when to best use each of them.

This is joint work with Victor Roussalany.