Strategies in Spatio-Temporal Logics for Multi-agent Systems

In distributed agent systems, agents with different abilities work autonomously to reach a common task, in the face of challenges posed by their environment. Two types of structures shape the collective behaviour of the system: a temporal one, defined by the progression of states the system goes through, and a spatial one, defined by the various constraints imposed by the environment on agents’ moves. We argue that both structures can be modelled in terms of suitable topologies, giving rise to a common categorical structure, namely that of trees labelled over a well-founded meet-semilattice, which in turn originates specific kinds of propositional and modal logics. As a result, it is immediate to model some sort of temporal and spatial logic on the properties of state sequences. The resulting logics are extended to integrate the constraints induced by the strategies determining the actual behavior of the agents. The modularity of the approach implies a theoretical simplification and suggests the possibility of a variety of applications.