Decentralized and heterogeneous systems—such as IoT networks and autonomous multi-agent systems—are increasingly characterized by dynamic, proximity-based interactions that naturally induce directed communication graphs. Ensuring correct behaviour in such settings requires expressive and scalable techniques for specifying and monitoring spatial properties of these graphs at runtime.

In this work, we introduce the Spatial Logic of Directed Graphs, a formal logic designed to specify properties of paths and connectivity patterns in potentially partitioned directed graphs. This logic builds upon the Spatial Logic of Closure Spaces (SLCS). While SLCS supports only node-based spatial reasoning, we extend it to capture and exploit properties of edges. In doing so, we provide a unified framework for the concise specification of non-trivial spatial behaviours, through a combination of local (neighbourhood-based) and global (graph-level) modalities.

We first define the formal semantics of the logic, and then show how specifications can be systematically compiled into runtime monitors through the eXchange Calculus (XC), yielding aggregate programs suitable for decentralized execution. This, in turn, enables efficient automatic monitor synthesis and seamless deployment on large-scale distributed systems by leveraging existing XC toolchains in C++ (FCPP) and Scala (ScaFi). Finally, we demonstrate the expressiveness and practicality of our approach through a set of representative examples, and validate it via simulations and visualizations implemented in FCPP, supporting rapid prototyping of spatial applications and their associated monitors.