Dynamic spatio‐temporal logic based on RCC‐8

Summary Qualitative spatio‐temporal reasoning is an important problem in artificial intelligence and has been widely and successfully applied in geographic information system and spatio‐temporal database. Currently, action features can be found in spatio‐temporal domain and the existing spatio‐temporal formalisms are not suitable for dealing with dynamic spatio‐temporal knowledge. Thus, how to represent and reason dynamic spatio‐temporal knowledge has become an important research issue. In this article, we present a dynamic spatio‐temporal logic for representing and reasoning dynamic spatio‐temporal knowledge. is a natural combination of spatio‐temporal logic ‐8 based on ‐8 and propositional dynamic logic. Timed actions of can be considered as temporal terms, moving the regions of topological space from one time point to another. can capture actions that change spatial relations between regions over time. For a formula from , we present a construction of a Büchi tree automaton. At the same time, we prove that deciding the satisfiability problem of is an EXPTIME‐complete problem.