Real-Time Guarantees for SLCS Monitors in XC

The behavior of distributed systems situated in space can be required to satisfy spatial properties, in addition to the more widely known temporal properties. In particular, it has been previously shown that fully distributed monitors in eXchange Calculus (XC) can be automatically derived for verifying properties of situated systems expressed in the Spatial Logic of Closure Spaces (SLCS). While it has been proven that such monitors eventually compute the truth value of the desired properties, the actual time required for such computations has been thus far disregarded. In the present paper, we fill this gap by investigating the real-time guarantees that can be given in terms of upper bounds on the time taken by the XC monitors to compute the truth of SLCS properties after stabilisation of inputs.