Representing RCC relations in temporal logic

Abstract

In this article we attempt to represent a spatial logic with a temporal logic in such a way that the spatial relations and the temporal relations can be used like a spatio-temporal logic. The spatial logic we try to represent is the Region Connection Calculus (RCC). The temporal logics we will discuss are Linear-time Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL). We also discuss the available model checkers for these temporal logics and give an example of the use of the spatio-temporal logic. We conclude that LTL can only represent some RCC relations. CTL can represent all RCC relations but temporal reasoning isn't possible anymore. ATL can represent all RCC relations and temporal reasoning is still possible.