Exploring the Bidimensional Space: A Dynamic Logic Point of View

We present a family of logics for reasoning about agents' positions and movements in the plane which have several potential applications in the area of multi-agent systems, such as multi-agent planning and robotics. The most general logic includes (i) atomic formulas for representing the truth of a fact or the presence of an agent at a certain position of the plane, (ii) atomic programs corresponding to the four basic orientations in the plane (up, down, left, right) as well as the four program constructs of propositional dynamic logic PDL (sequential composition, nondeterministic composition, iteration and test). As this logic is not computably enumerable, we study some interesting decidable and axiomatizable fragments of it. We also present a decidable extension of its iteration-free fragment by special programs representing movements of agents in the plane.