Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning.
In this paper we advocate the use of multi-dimensional modal logics as a framework for knowledge representation and, in particular, for representing spatio-temporal information. We construct a two-dimensional logic capable of describing topological relationships that change over time. This logic, called (Propositional Spatio-Temporal Logic) is the Cartesian product of the well-known temporal logic PTL and the modal logic S4u, which is the Lewis system S4 augmented with the universal modality. Although it is an open problem whether the full PSTL is decidable, we show that it contains decidable fragments into which various temporal extensions (both point-based and interval based) of the spatial logic RCC-8 can be embedded. We consider known decidability and complexity results that are relevant to computation with multi-dimensional formalisms and discuss possible directions for further research.
Introduction
It is widely accepted that many kinds of AI applications require high-level
reasoning involving spatial and temporal concepts (see e.g. (Hayes,
1979; Hobbs and Moore, 1985; Davis, 1990)). Several approaches have
been applied to representing these concepts: some researchers have developed
specialised computation-oriented representations such as solid
geometry (Requicha, 1980), constraints techniques (Allen, 1981) and
spatio-temporal database architectures (Guting et al., 2000); others
have employed techniques of formal logics. Typically, logical representations
have made use of the expressive power of rst-order languages
(e.g. (McCarthy and Hayes, 1969; Clarke, 1981; Allen, 1984; Hayes,
1985; Kowalski and Sergot, 1986; Randell et al., 1992b)); but, since
Supported by the EPSRC under grants GR/K65041 and GR/M56807
c
2000 Kluwer Academic Publishers. Printed in the Netherlands.
rst-order logic is undecidable, such languages do not provide an eec-
tive reasoning algorithm unless supplemented by some special purpose
inference mechanism.
An alternative to rst-order logic is the framework of propositional
modal logic, which extends classical propositional calculus with one
or more 'modal' operators, interpreted on some relational or algebraic
structures. Appropriate structures may be chosen to correspond to an
aspect of reality, such as time or space, which one wishes to describe
within a logical representation.
For example, one may think of time as a sequence of points represented
by the natural numbers hN; <i on which temporal operators |
'some time in the future', `since' etc. | can be dened. For instance
is true at a time point t 2 N (in symbols t
only if t 0 t. The resulting propositional temporal
logic, PTL, is decidable in PSPACE (Sistla and Clarke, 1985) and by
Kamp's theorem (Kamp, 1968) it is as expressive (on hN; <i) as the
rst-order language with unary predicates P i (x), < and =. Temporal
logics of this sort are widely used in computer science (Manna and
Pnueli, 1992; Stirling, 1992).
Modal representations of space are relatively new to computer sci-
ence. However, the possibility of giving topological interpretations of intuitionistic
propositional logic has been known since the thirties (Stone,
1937{8; Tarski, 1938). Tang (1938) and later McKinsey and Tarski
(1948) interpreted the necessity operator of the Lewis modal system
S4 as the interior operator of topological spaces and proved that S4
is sound and complete with respect to this interpretation (for details
see e.g. Chagrov and Zakharyaschev (1997)). Since S4 is decidable in
PSPACE, this suggests that it might provide a computationally viable
language for describing topological information. That S4 really can be
used for qualitative spatial representation and reasoning was observed
by Bennett (1996, 1998), who embedded the spatial language RCC-8
into extended with the universal modality 8 (for all
points in the space). This encoding, which will be explained in Section 2,
provides a decision procedure for a spatial language that can express
a large class of signicant topological relations including all those in
RCC-8.
As we have seen, propositional modal and temporal logics may be
decidable and hence amenable to automated reasoning (Demri, 1994;
Giunchiglia and Sebastiani, 1996; Horrocks, 1998; Dixon et al., 1998;
Voronkov, 1999; De Nivelle et al., 2000). This of course means that
they are less expressive than rst-order logic. Moreover it is clear that
modalities of single type (say, only temporal or only spatial) are not
comprehensive enough for many real applications, which require rea-
Time
Space
Space

Figure

1. Motion modelled in terms of a Cartesian product of space and time
soning with a range of dierent concepts. What we actually need is
systems combining several types of modal operator. Such multi-modal
logics have been the subject of much recent research | e.g. (Kracht
and Wolter, 1991; Spaan, 1993; Marx and Venema, 1997; Gabbay,
1998; Wolter, 2000; Gabbay et al., 2000). Central problems in this eld
concern how modalities can be combined, whether interplay between
operators preserves decidability and other meta-logical properties, and
what is the computational complexity of the resulting systems.
Whereas modalities can be successfully combined as logically independent
operators (Kracht and Wolter, 1991; Fine and Schurz, 1996),
a key feature of most of the more interesting systems is the interaction
between dierent modalities. This applies in particular to modal operators
relevant to describing spatial and temporal concepts. Consider, for
instance, a moving region (the black disk) depicted in Fig. 1. If we can
model space as an S4 u -frame (i.e., a quasi-order) F and if the
ow of
time is represented by a linear order G, then the whole spatio-temporal
'universe' can be viewed as the Cartesian product F G, in which the
act 'horizontally' to talk about spatial regions, while
the temporal operators act 'vertically' taking care of their movements
in time.
Cartesian products of Kripke frames are typical examples of multi-dimensional
structures that serve as models of multi-dimensional modal
logics . The idea of a multi-dimensional modal logic was introduced by
presented an axiomatisation for a 2-dimensional
extension of S5. Products of modal logics were investigated in (Sheht-
man, 1978; Gabbay and Shehtman, 1998; Marx, 1999). In computer science
and AI, multi-dimensional modal logics are used e.g. for constructing
temporal epistemic logics for multi-agent and distributed systems
et al., 1995), temporal logics of parallel processes (Reynolds,
1997), temporal, epistemic, and dynamic description logics (Baader and
Ohlbach, 1995; Wolter and Zakharyaschev, 1998, 1999, 2000c). Further
details and development of multi-dimensional modal logic can be found
in (Gabbay et al., 2000).
Although the idea of constructing multi-dimensional modal logics
may appear natural and simple, the resulting 'hybrids' often turn out
to be very complex or undecidable, even if the one-dimensional components
are 'almost tractable'. As with other frameworks for knowledge
representation there is a delicate balance between expressive power and
computational complexity. Let us consider, for instance, the following
nave example of a 'compass' spatial logic (Venema, 1990).
In our everyday practice, we often connect spatial structures with
this or that system of coordinates. For instance, in geographical maps
we have four compass directions: North, South, West, and East. Using
these we can say e.g. that Moscow is to the North-East of London.
Spatial relations of this sort can be expressed in a modal language with
four operators N ('somewhere to the ('somewhere to
the South') interpreted in the Cartesian product of two linear orders,
say, hR; <i hR; <i in the standard Kripke-style manner:
etc.
That 'Moscow is to the North-East of London' can be represented in
this language by the formula London It is well known
from modal logic that the satisability problem for a language with
a single  operator is NP-complete for the frames hR; <i or hN; <i,
(Ono and Nakamura, 1980). However, the satisability problem for a bi-modal
language (with N and E ) in hR; <ihR;<i or hN; <ihN;<i
turns out to be undecidable, even  1
and Reynolds, 1999; Reynolds and Zakharyaschev, 2001). The interval
temporal logic of Halpern and Shoham (1986) can be interpreted in
the f(x; y) 2 N  N : x  yg part of hN; <i  hN; <i (see (Venema,
1990)), and this logic is also not recursively enumerable. There are
many other examples of undecidable multi-dimensional modal logics,
e.g. S5S5S5 (Maddux, 1980) or even any logic between KKK
and S5S5S5 (Hirsch et al., 2000).
Thus, we see that multi-dimensional modal logics are not easy to deal
with, and we need to be careful in constructing eective and expressive
spatio-temporal formalisms. For example, the straightforward attack
on the problem by means of using the Cartesian products of frames
for S4 and the
ow of time hN; <i (or any other innite linear
has not brought any result yet: whether the logic of such 2-dimensional
frames is decidable remains one of the challenging open problems in
the eld.
In the rest of this paper, we discuss possible uses of multi-dimensional
modal logics for spatio-temporal representation and reasoning, giving
initial results already obtained in this direction. Thereby we would like
both to attract the attention of the knowledge representation community
to this novel and promising approach and also to give incentive
to logicians to investigate modal languages that may turn out to have
practical utility.
2. Region Connection Calculus and a Modal Interpretation
The Region Connection Calculus (RCC) is a rst-order theory proposed
by Randell et al. (1992a) for qualitative spatial representation
and reasoning. 1 The basic language of RCC contains only one primitive
predicate C(X; Y ), read as 'region X is connected with region Y '. 2
Many other spatial relations can be dened in terms of the C primi-
tive. Of particular signicance are the eight relations depicted in Fig. 2.
These form a pairwise disjoint and exhaustive set of relations known as
RCC-8. Essentially the same set (but applied to the more restricted
class of connected regions) has been independently identied as useful
in the context of Geographical Information Systems (Egenhofer and
Franzosa, 1991). In English, the relations can be described as: Dis-
Connection, External Connection, Partial Overlap, Tangential Proper
Part, Non-Tangential Proper Part and Equality. Formal notations for
these relations are given under the diagrams. The part relations are
asymmetric, so each has an inverse, su-xed by 'i'.
The RCC formalism was originally presented as a nave theory in
the spirit of Hayes (1979), so no specic model was assumed. However,
it has been found that the theory can be interpreted in classical point-set
topology (Gotts 1996a; Bennett 1997,1998). Thus, we can take as
models of RCC, topological spaces, U is a non-empty
set, the universe of the space, and Ian interior operator on U . 3
comprehensive account of this theory and its applications can be found in
(Cohn et al., 1997).
Randell et al. (1992a) also considered an extended language incorporating an
additional primitive function conv(r), which denotes the convex-hull of region r. We
will comment brie
y on convexity later (Section 6).
3 This means that Imust satisfy the axioms I(X)  X,
and I(X \ Y
a
a
a
a
a b
a
a
a b

Figure

2. Basic Relations in the RCC Theory
Individual variables of RCC range over non-empty regular closed sets of
T, i.e., an assignment in T is a map a associating with every variable X
a set a(X)  U such that
is the closure operator on U dual to I. The connection relation C(X; Y )
is then interpreted as meaning that the point sets denoted by X and
Y share at least one point:
The full rst-order theory of RCC is too expressive to be computationally
useful and is in fact undecidable (this follows from (Grzegor-
czyk, 1951); results applying more specically to RCC can be found in
(Gotts, 1996b) and (Dornheim, 1998)). Fortunately, there are various
decidable (and even tractable) fragments of RCC.
As was mentioned above, for certain applications one can limit the
relations employed to the set RCC-8. Moreover, according to the experiments
reported by Knau et al. (1997) the eight predicates turn out
to be 'cognitively adequate' in the sense that people indeed distinguish
between those relations. Formally, the language of RCC-8 consists of a
set of individual variables X called region variables, the eight
binary predicates DC, EC, PO, EQ, TPP, TPPi, NTPP, NTPPi, and the
Boolean connectives (:, out of which we can construct
spatial formulas.
RCC-8 is interpreted in topological spaces
the region variables range over non-empty regular closed sets in T, and
the eight predicates are dened in the following way:
For example, according to this denition, EC(X; Y ) means that X and
Y share at least one point but do not share any interior point (i.e. they
only share boundary points).
The main reasoning task for RCC-8 can be formulated as follows:
given a nite set  of spatial formulas, decide whether  is satis-
able in a topological space, i.e., whether there exists a topological
space T and an assignment a in it such that T j= a .
That this satisability problem is decidable was observed by Bennett
(1994), who exploited the results of Tarski (1938) to encode RCC-8
into intuitionistic propositional logic. Subsequently, Bennett (1996) gave
another embedding of RCC-8 into the more expressive logic containing
Lewis's S4 modality and an additional universal modality, whose
meaning will be explained below. In the current paper we shall refer
to this bi-modal logic as S4 u . The embedding is based on the result of
McKinsey and Tarski (1948) according to which S4 is characterised by
the class of topological spaces in the following sense:
Given a topological space
interpret the propositional variables in ' as subsets of U , the Boolean
connectives as the corresponding set-theoretic operations, the necessity
operator I as I, and the possibility operator C as C (we denote the
usual box  and diamond  of S4 by I and C to emphasize their
topological meaning). Now, if the value of ' is the whole space U , no
matter what sets are assigned to its variables and what topological
space is taken, then ' is provable in S4, and vice versa.
According to (Goranko and Passy, 1992), this completeness theorem
still holds if we extend S4 with the universal modalities 8 and
9 interpreted in T as 'for all points in T' and `there is a point in T',
respectively. That is the value of 8' (under a certain interpretation) is
U if the value of ' (under this interpretation) is U , otherwise it is ;;
:8:'.
It is easy to see that the language of the resulting logic S4 u is expressive
enough to encode the topological meaning of the RCC-8 formulas
as dened above. Given such a formula ', we replace in it occurrences
of RCC-8 predicates with the corresponding modal formulas, e.g.
etc.
are propositional variables) and add to the result the conjunct
for every region variable X i in ' to ensure that the propositional variables
are interpreted by non-empty regular closed sets of topological
spaces. The resulting modal formula is denoted by ' y .
Now, if we recall that some (in particular, all nite) topological
spaces are determined by Kripke frames hW; Ri for S4 | every such
frame gives rise to the topological space hW; Ii, where
for any X  W | and that S4 u has the nite model property (Goranko
and Passy, 1992), then we immediately obtain
Theorem 1. For every RCC-8 formula ', the following conditions
are equivalent:
(i) ' is satisable in a topological space,
(ii) ' y is satisable in a topological space,
(iii) ' y is satisable in some nite Kripke frame for S4.
Thus we reduce the satisability problem for RCC-8 formulas to
the satisability problem for propositional bimodal formulas in Kripke
frames for S4 u , which is decidable (Goranko and Passy, 1992).
Moreover, one can show that every satisable formula of the form
' y can be satised in a partially ordered Kripke frame each point in
which has at most two (incomparable) successors, and the number of
worlds in this frame is linear in the number of symbols in 'y (and
consequently also linear in the length of the RCC-8 formula '). This
result was obtained by Renz (1998); a somewhat more general theorem
is proved in (Wolter and Zakharyaschev, 2000a). It follows in particular
that the satisability problem for RCC-8 formulas is NP-complete;
see (Renz and Nebel, 1997; Renz and Nebel, 1999) where maximal
tractable fragments of RCC-8 are also described. It also follows that
all satisable RCC-8 formulas can be satised in R n for any n  1.
(Note however that S4 u is not complete with respect to R n .)
3. Point-based temporal RCC-8
One approach to constructing spatio-temporal logics is to combine
RCC-8 with point-based temporal logics, for instance, the well-known
propositional temporal logic PTL interpreted on the
ow of time hN; <i
and having the temporal operators S (Since) and U (Until). Other
standard operators can be dened:
('at the next moment "),
(p _ :p) U ' (`at some time in the future '')
in the future ''),
and similarly for their past counterparts f ,  and  .
The spatial regions occupied by the objects under consideration may
change with time passing by, but the topological space in which they
are moving always remains the same. This nave picture is formalised
by the following concept of topological temporal model.
Denition 1. A topological temporal model (or tt-model, for short)
based on a topological space is a triple of the form
a, an assignment in T, associates with every region
variable X and every moment of time n 2 N a non-empty regular
closed subset of U . For each n, we take a n to be the function dened
by a
There are several dierent ways of introducing a temporal dimension
into the syntax of RCC-8. The most obvious is to allow applications of
the operators S and U (along with the Booleans) to spatial formulas.
We call the resulting spatio-temporal language ST 0 .
Denition 2. For a tt-model ai, an ST 0 -formula ', and
dene the truth-relation (M; n) meaning `' holds in M at
moment n,' by induction on the construction of ':
if ' contains no temporal operators, then (M; n) an ';
(M; n) there is k > n such that
every l such that n < l < k;
(M; n) there is k < n such that
every l such that k < l < n.
allows us to say many things about changes of spatial relationships
over time. For example, means that
'Kosovo will not always be part of Yugoslavia.' It is also expressive
enough to constrain movements to be continuous, in so far as one can
describe possible continuous transitions among the RCC-8 relations
that can hold between two regions (such transitions were identied by
Randell et al. (1992a) and the importance has been emphasised more
recently by Muller (1998)):
etc.
However, the expressive power of ST 0 is limited in that one can only
employ the RCC-8 relations to compare region variables at the same
point in time; so it does not allow one to describe spatial relations
between the extensions of a region variable at dierent times. For ex-
ample, there is no way to say something like 'The extension of the EU
is a part of what its extension will be next year (i.e. at the next time
To overcome this limitation we introduce the logic ST 1 , which extends
ST 0 by allowing applications of the next-time operator f not only
to formulas but also to region variables. Thus, arguments of the RCC-
8 predicates are now region terms, which consist of a region variable
that may be prexed by an arbitrarily long sequence of f operators.
For instance f f EU could denote the region occupied by the EU in
two years time and one can write formulas such as P(EU ; f f EU ).
The semantics of ST 1 is just that of ST 0 extended by the following
clause:
Using ST 1 we can now talk about the changing extensions of individual
region variables. For instance  that 'the
EU will never shrink'. The new construct may also be used to rene the
continuity assumption by requiring that
i.e., 'regions X and f X either coincide or overlap.' We can also express
the condition that the extension of a region variable X is xed for the
future:  or that it has at most two distinct states, one
on even days, another on odd ones:  X). Note, that the
only in models based on
innite topological spaces, whereas for formulas of ST 0 (and of course
nite topological spaces always su-ce.
It may appear that ST 1 can compare regions that are separated
in time only by limited sequences of time points. However, using an
auxiliary variable, whose extension is constrained to be constant over
time, we can write, for instance,
which is satisable i 'someday in the future the present territory
of Russia will be part of the EU.' This contrasts with the formula
meaning that there will be a day when Russia (its
territory on that day | perhaps without Chechnya but with Byellorus-
sia) becomes part of the EU.
Imagine now that we want to say that every location in Europe will
pass through the Euro-zone, but only the land currently occupied by
Germany will use the Euro forever. Unfortunately, we do not know
which countries will form within Europe in the future, so we can't
simply write down all formulas of the form  What
we need is the possibility of constructing regions  containing all the
points that will belong to region X at some time in the future and
containing just those points included in all future states of X . Then we
can write: P(Europe;
Similarly, the formula P(Russia;  that all points of the
present territory of Russia will belong to the EU at some time in the
future (but perhaps at dierent moments of time).
To permit fully general application of temporal operators to region
variables we dene the language ST 2 in which region variables may be
prexed by arbitrary strings of the operators f ,  . The semantics
of the new operators are given by:
k>n a(t; k)),
k>n a(t; k)).
Finally, we can make our languages ST i , for even more
expressive by allowing applications of the Boolean operations to region
terms. Their semantical meaning is dened as follows:
i be the resulting family of languages. In these languages we
can write formulas such as EQ(UK,Great Britain _ Northern Ireland),
meaning that the extension of the UK is the sum of the extensions of
Great Britain and Northern Ireland.
4. Modal Encoding of ST +The decidability and complexity results for the ST i languages were
proved in (Wolter and Zakharyaschev, 2000b) by embedding them into
the two-dimensional propositional modal logic S4 u PTL, the Cartesian
product of the logics S4 u and PTL. We call this logic Propositional
Spatio-Temporal Logic or PSTL. Its connectives are: the Booleans,
the necessity and possibility operators I and C of S4, the universal
necessity and possibility operators 8 and 9, and the temporal operators
S and U . It is not known whether the full PSTL (or even S4PTL) is
decidable. However, its fragments corresponding to the ST i languages
are quite manageable.
The modal translation from ST
into PSTL is dened by extending
the y transformation specied in Section 2 to handle region terms containing
Boolean and temporal operators. The region terms are already
ostensibly formulas of PSTL; however, we must bear in mind that
these terms are intended to denote only regular closed subsets of the
space. The easiest way to take this into account is to prex CI to every
subterm occurring in an ST +-formula.
What is the intended semantics of PSTL? As we have seen, when
encoding pure RCC-8 into S4 u we can specify the semantics with
either topological models or Kripke models and these are equivalent
in terms of validity. However, the addition of the temporal component
makes the situation more complicated in that the topological and
Kripke semantics do not perfectly agree on the class of valid formulas.
Let us dene these two types of model structures:
Denition 3. A Kripke PSTL-model is a triple
is a quasi-order (a frame for S4) and V, a valuation, is a
map associating with every propositional variable p and every n 2 N a
subset V(p; n)  W . For each spatial point u 2 W and each time point
N, the truth-relation (u; n)
(u; n)
(u; n)
(u; n) such that uRv,
(u; n) there is k > n such that
plus the standard clauses for S and the Booleans. A PSTL-formula '
is satised in K if (u; n)
Denition 4. A topological PSTL-model is a structure
in which is a topological space and U is a map associating
with every propositional variable p and every n 2 N a set U(p; n)  U . U
is then extended to arbitrary PSTL-formulas in the following way:
there is a k > n such that x 2 U(;
m) for all m; n < m < k.
Consequently the dened temporal operators are interpreted by
A PSTL-formula ' is satised in N if U('; n) 6= ; for some n 2 N.
The sets of PSTL-formulas satisable in Kripke models and topological
models turn out to be dierent. Of course, every Kripke model
is equivalent to some topological model. But the converse does not
hold. A good example is provided by the formula
This is valid in every Kripke PSTL-model because from any space-time
point in such a structure any given other point is reachable by
forward transition along the time line followed by transition along the
accessibility relation of F just in case it is reachable by rst moving
along the accessibility relation and then forward along the time dimension
(since the accessibility relation remains constant for all time
points). However, in certain innite topological spaces (e.g. R) one can
construct innite sequences X n of closed sets such that S
closed. In a topological model based on such a space  need not
have the same denotation as C + p. This subtlety concerning innite
unions is not accounted for by the Kripke approach.
The divergence between topological and Kripke PSTL-models is
problematic because whereas the topological models correspond to the
desired spatial interpretation, most currently known methods of determining
decidability and complexity are based on Kripke models.
Fortunately, Wolter and Zakharyaschev (2000b) have been able to show
that the two semantics agree on the satisability of ST +-formulas as
long as we adopt a reasonably natural Finite State Assumption (FSA).
The FSA requires that over the innite sequence of time points each
region that one can refer to can have only nitely many distinct extensions
(but it may change its extension innitely often). Although this
restriction rules out many mathematically interesting possibilities, it
is perfectly satisfactory for a wide range of practical applications (for
example planning tasks where we want to get from an initial to a nal
situation | in a nite number of steps). To formalise the FSA we dene
the following restricted class of tt-models:
Denition 5. Say that a tt-model or is an
FSA-tt-model, if for every region term t there are nitely many regular
closed sets A U such that fa(t; n) g.
It can be shown that an ST
2 -formula is satisable in an FSA-tt-
model i it is satisable in an FSA-model based on a nite topological
space.
Because of the very restricted combinations of operators that result
from translating RCC-8 predicates and their region term arguments,
the modal translations of ST
-formulas form a rather special fragment
of the modal language PSTL. As was mentioned above, Renz (1998)
showed that an RCC-8 formula ' is satisable i ' y is satisable in
a Kripke model based on an S4-frame of depth  1 and width  2
(which means that it contains no chains of more than 2 distinct points,
and no point has more than 2 distinct successors); and it turns out that
this result can be generalised to formulas of ST +and ST +:
Theorem 2.
a) An ST
-formula ' is satisable in a FSA-tt-model i ' y is sat-
isable in a Kripke PSTL-model (which also satises FSA) whose
underlying S4-frame is of depth  1 and width  2. 4
-formula ' is satisable in a tt-model i ' y is satisable in
a Kripke PSTL-model of depth  1 and width  2.
This result makes it possible to use the method of quasi-models
(Wolter and Zakharyaschev, 1999) to prove that the satisability problem
for all the languages ST
in tt-models is decidable.
Given the rather weak interaction between time and space in ST 0 it
is not hard to show that the satisability problem for ST 0 formulas
in tt-models is PSPACE-complete (the same as that of PTL). The
satisability problem for ST 1 formulas in tt-models is decidable in
EXPSPACE (and becomes NP-complete for the sublanguage of ST 1
with only the temporal operator f ). If we restrict the admissible models
to FSA-models then the satisability problem for ST 2 formulas
is decidable in EXPSPACE. Moreover, all the complexity results just
given remain valid after replacing ST i with ST
4 Actually, since occurrences of  + within the region terms of ST
are always
regularised by adding the prex CI, one might conjecture that the FSA is not
necessary. However, at present we cannot envisage how to prove this.
The topological temporal models we were considering above are
based on the discrete
ow of time N. By replacing N with Q, R, or
any other strict linear order we can extend our semantics to cover
dierent
ows of time. But then the question arises as to whether the
decidability and complexity results proved for N can be extended to,
say, the logic determined by the class of arbitrary strict linear orders,
by the reals R, or by the rationals Q. It turns out that for the language
of ST 0 we can easily extend the decidability proof for N by using the
fact that the propositional temporal logics based on those
ows of time
are decidable (Gabbay et al., 1994). As concerns ST 1 , observe that the
operator f is meaningless for dense linear orders|thus for Q and R this
language reduces to ST 0 . Decidability of ST 1 interpreted in arbitrary
linear orders is an open problem. And nothing is known about the
decidability of ST 2 interpreted in
ows of time dierent from N. We
conjecture, however, that the methods developed in (Hodkinson et al.,
2000) can be used to prove the decidability of ST 2 based on any of the
ows of time mentioned above (under FSA).
5. RCC-8 and Interval Temporal Logic
We have seen how the RCC-8 theory can be temporalised by combining
it with a point-based temporal logic. However, since the region-based
approach to spatial reasoning was inspired by and closely mirrors
the interval-based approach to temporal reasoning (Allen, 1981; Allen,
1984) (they both take extended entities, rather than points as primi-
tives) it would seem far more natural to temporalise RCC-8 by combining
it with an interval-based logic. In this section we show that this
can indeed be done; and moreover, that the resulting system can in fact
be embedded by suitable syntactic denitions within the point-based
logic PSTL dened above.
We remind the reader that Allen's logic has thirteen basic relations
between time intervals | Before(i; j), Meets(i; j), Overlaps(i; j),
The set of formulas constructed using these predicates and the Booleans
can be regarded as a temporal 'twin' of RCC-8.
Following Allen (1984), we write HOLDS(R; i) to say that the relation
R holds during some time interval i. Thus HOLDS(PO(X; Y ); i)
means that during interval i regions X and Y partially overlap. Let
us call an ARCC-8 formula any Boolean combination of basic temporal
predicates and formulas of the form HOLDS('; i) where ' is an
RCC-8 formula. Here is a simple example of a valid entailment in this
unsophisticated language:
HOLDS(TPP(Hong Kong
HOLDS(DC(Hong Kong ; UK); j);
There are dierent views on how intervals should be modelled in
dierent time
ows. A common interpretation is that the intervals
are treated as ordered pairs of distinct points of the domain Q or R.
Within our framework we can in fact adopt any of these models; but,
for simplicity of presentation it is convenient to employ a semantics
where intervals are arbitrary convex non-empty subsets of the time
points of an arbitrary time
ow. Thus we give the following semantics
for ARCC-8:
Denition 6. An it-model (interval topological model) is the triple
is a strict linear order (modelling the
intended
ow of time); is a topological space; and assignment
a associates with every interval variable i a non-empty convex subset
of W and with every region variable X and every moment of time u it
associates a regular closed set a(X; u) in T.
The truth-relation is dened inductively as follows (clauses for the
Booleans are standard):
and not M j= a Before(i; j);
The other interval relations are dened similarly;
M j= a HOLDS('; i) i for every point u 2 a(i) we have T
We now show how by using some ideas of Blackburn (1992) the
language ARCC-8 can be directly embedded into PSTL. For convenience
we dene undirected universal and existential modalities over
time: is true at every moment) and
We extend the translation function y dened above to
encode the interval relations and HOLDS predicate. For example, we
replace in '
and the other Allen relations can be encoded in similar fashion. Here
the variables t i are just ordinary propositional variables; however, we
need to constrain their interpretation so that they can be employed
to stand for intervals. Therefore, we add to the resulting formula the
conjuncts
for every interval variable i occurring in ', thus obtaining ' y . The rst
conjunct ensures that t i is non-empty; 5 the second that it is a convex
interval of the time series; and the nal conjunct means that the value
of t i is constant relative to the spatial dimension.
It can be shown that an ARCC-8 formula ' is satisable in an
it-model just in case its modal translation ' y is satisable in a Kripke
PSTL-model. Moreover, the satisability problem for ARCC-8 formulas
in it-models is NP-complete. Thus ARCC-8 has the same computational
complexity as both RCC-8 and the constraint language of
Allen's temporal interval predicates (Vilain et al., 1986).
6. How Far Can Multi-Dimensional Modal Logic Take Us?
We have seen how the 2-dimensional language PSTL provides an expressive
formalism for representing spatio-temporal information, which
encompasses both topological constraints and linear temporal logic. We
now consider what other concepts one might want to represent and note
some di-culties that arise due to known complexity results.
A concept that is very useful for describing real situations is that
of spatial convexity. The addition to the rst-order RCC formalism
of a function giving the 'convex-hull' of a region proposed in (Randell
et al., 1992a) (such a function and a convexity predicate true of convex
regions are interdenable). First-order languages including topological
relations and a convexity predicate have been found to be highly
expressive (Pratt, 1999). Although satisability of a combination of
5 If we replace this conjunct by out 'intervals'
consisting of a single time point.
RCC-8 relations and convexity predicates is known to be decidable
is has also been shown to be as hard as solving systems of non-linear
constraints over R (Davis et al., 1999). It is unclear whether modal
logics can contribute to reasoning about convexity. The obvious models
of multi-dimensional space within which convexity constraints could
be specied involve cross products of linearly ordered innite frames
corresponding to coordinate axes of the space. However, it is known
that all modal logics of such products are undecidable (Reynolds and
Zakharyaschev, 2001). Balbiani et al. (1997) have given a modal logic
of incidence geometry within which one can express collinearity and
betweenness (and hence convexity) but it is not known whether this
logic is decidable.
Another concept crucial to real situation descriptions is that of connectedness
of regions. The objects we normally think and talk about
are connected in the sense that any two points within an object can be
joined by a path that lies entirely within the object. One of the most
important open problems in spatial reasoning is whether there is a decision
procedure for testing satisability of sets of topological relations
holding among connected planar regions. A lower exponential complexity
bound follows from the results of (Kratochvl, 1991; Kratochvl and
Matousek, 1991) concerning an analogous problem for planar graphs;
and this result applies even in the case where we deal with only the
basic non-disjunctive relations of RCC-8. We speculate that a modal
analysis might shed some light on this decision problem.
One might also want to introduce more expressive power in the
temporal dimension. In order to describe continuous changes more adequately
one may want to employ a logic based on a dense model of
time (Barringer et al., 1986). Within such a time
ow, we must consider
whether spatial relationships hold over open or closed intervals.
This problem has be examined by Galton (1997,2000), who argues that
whether a spatial relation is true at the bounding point of an interval
over which it holds depends on the nature of the relation in question.
This analysis may allow for more detailed description of changing spatial
relationships than is possible within Allen's (1984) treatment. Also,
rather than treating time as a linear ordering one might like to model
alternative possible histories in terms of some branching structure,
such as is described by the logic CTL  (Emerson and Halpern, 1986).
Semantically it is straightforward to combine the spatial interpretation
of S4 u with any reasonable temporal logic; but so far nothing is known
about the complexity of combinations with non-linear time-
ows.
In considering decidability and complexity of multi-modal systems,
logicians have almost always looked at the problem for arbitrary formulas
of the resulting modal language. However, as we saw in the case
of PSTL, sub-languages with severely restricted syntax (e.g. ST (+)
may be able to express a signicant vocabulary su-cient for many
applications. Thus we suggest that looking for such sub-languages is a
research area of great potential.
In order to really demonstrate the utility of multi-dimensional logics
one would need to develop and implement reasoning algorithms capable
of carrying out useful reasoning tasks. Automated reasoning with multi-modal
logics is still in its infancy; but recently there have been some
successes in developing proof methods (Dixon et al., 1998; Hustadt
et al., 2000). A tableau calculus for the local cubic logic LC 2 , which is
closely related to S5S5, has been implemented by Marx et al. (1999).
7. Conclusion
We have outlined the general structure of a knowledge representation
formalism, based on multi-dimensional modal logics. This framework
seems to be well suited for representing a large vocabulary of useful
high-level spatio-temporal relations. Our decidability and complexity
results for the languages ST (+)
i and ARCC-8 show that this approach
enables one to construct very expressive yet eective spatio-temporal
languages. We hope that the reader will take from this paper not only
the particular details of the language PSTL but a wider appreciation
of the possibilities of applying multi-dimensional modal logics to the
development of Articial Intelligence. We would also like to suggest that
spatio-temporal reasoning is an area within which cooperation between
pure logicians and researchers tackling specic reasoning problems arising
in applications can lead to both interesting theorems and powerful
practical algorithms.



--R











Modal Logic.
'A calculus of individuals based on 'connection

Representations of Commonsense Knowledge.





Principles of Knowledge Representation and Reasoning:

International Journal of Geographical Information Systems 5(2)

Reasoning About Knowledge.


Temporal Logic: mathematical foundations and computational aspects


Fibring Logics.















Formal Theories of the Commonsense World.









Journal of Combinatorial Theory



The temporal logic of reactive and concurrent systems.












Principles of Knowledge Representation and Reasoning:






Journal of Logic and Computation






Casopis pro p





Revised version in (Weld and De Kleer

Readings in Qualitative Reasoning About Physical Systems.
The decision problem for combined modal logics.


Fundamenta Informaticae



Frontiers of Combining Systems 2.
--TR

--CTR
Alfredo Burrieza , Manuel Ojeda-Aciego, A Multimodal Logic Approach to Order of Magnitude Qualitative Reasoning with Comparability and Negligibility Relations, Fundamenta Informaticae, v.68 n.1-2, p.21-46, January 2005
Andrzej Skowron , Piotr Synak, Complex Patterns, Fundamenta Informaticae, v.60 n.1-4, p.351-366, January 2004
Norihiro Kamide, Linear and affine logics with temporal, spatial and epistemic operators, Theoretical Computer Science, v.353 n.1, p.165-207, 14 March 2006
Andreas Schfer, Axiomatisation and decidability of multi-dimensional Duration Calculus, Information and Computation, v.205 n.1, p.25-64, January, 2007
Stphane Demri , Deepak D'Souza, An automata-theoretic approach to constraint LTL, Information and Computation, v.205 n.3, p.380-415, March, 2007
Frank Wolter , Michael Zakharyaschev, Qualitative spatiotemporal representation and reasoning: a computational perspective, Exploring artificial intelligence in the new millennium, Morgan Kaufmann Publishers Inc., San Francisco, CA,
modal logic;multi-dimensional logic;spatio-temporal reasoning