2015Utrecht University Repository (Utrecht University)Open access

Representing RCC relations in temporal logic

T. Harteveld

Open full text 0 citations

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.

About this research paper

What this paper is about

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.

Why it matters

A significance statement is not available in the OpenAlex record.

Key contribution

A contribution statement is not available in the OpenAlex record.

Method / approach

Method details are not available in the OpenAlex metadata.

Main findings

Findings are not separately available in the OpenAlex metadata.

Limitations

Limitations are not available in the OpenAlex metadata.

Applications

Application details are not available in the OpenAlex metadata.

Available 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.

Key concepts: Computation tree logic, Temporal logic, Linear temporal logic, Temporal logic of actions, Interval temporal logic, Computer science, Dynamic logic (digital electronics), CTL*

Related papers

Back to paper searchBrowse research topicsOriginal source
Representing RCC relations in temporal logic — Research Paper | ScholarLens