Abstract:
In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and `computational realisability' within the hierarchy. We demonstrate how different combining principles as well as spatial and temporal primitives can produce NP-, PSPACE-, EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal logics out of components that are at most NP- or PSPACE-complete.

---

Extracted Text

 


 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity

 
Journal of Artificial Intelligence Research 23 (2005) 167-243
Submitted 07/04; published 02/05
Combining Spatial and Temporal Logics:
Expressiveness vs. Complexity
David Gabelaia
gabelaia@dcs.kcl.ac.uk
Roman Kontchakov
romanvk@dcs.kcl.ac.uk
Agi Kurucz
kuag@dcs.kcl.ac.uk
Department of Computer Science, King’s College LondonStrand, London WC2R 2LS, U.K.
Frank Wolter
frank@csc.liv.ac.uk
Department of Computer Science, University of LiverpoolLiverpool L69 7ZF, U.K.
Michael Zakharyaschev
mz@dcs.kcl.ac.uk
Department of Computer Science, King’s College London
Strand, London WC2R 2LS, U.K.
Abstract
In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms
that result from various combinations of propositional spatial and temporal logics such asthe propositional temporal logic PT L, the spatial logics RCC-8, BRCC-8, S4u and theirfragments. The obtained results give a clear picture of the trade-off between expressivenessand ‘computational realisability’ within the hierarchy. We demonstrate how different com-bining principles as well as spatial and temporal primitives can produce NP-, PSPACE-,EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal logics out ofcomponents that are at most NP- or PSPACE-complete.
1. Introduction
Qualitative representation and reasoning has been quite successful in dealing with bothtime and space. There exists a wide spectrum of temporal logics (see, e.g., Allen, 1983;Clarke & Emerson, 1981; Manna & Pnueli, 1992; Gabbay, Hodkinson, & Reynolds, 1994;van Benthem, 1995). There is a variety of spatial formalisms (e.g., Clarke, 1981; Egenhofer& Franzosa, 1991; Randell, Cui, & Cohn, 1992; Asher & Vieu, 1995; Lemon & Pratt,1998). In both cases determining the computational complexity of the respective reasoningproblems has been one of the most important research issues. For example, Renz and Nebel(1999) analysed the complexity of RCC-8, a fragment of the region connection calculus RCCwith eight jointly exhaustive and pairwise disjoint base relations between spatial regionsintroduced by Egenhofer and Franzosa (1991) and Randell and his colleagues (1992); Nebeland B¨
urckert (1995) investigated the complexity of Allen’s interval algebra; numerous results
on the computational complexity of the point-based propositional linear temporal logic PT Lover various flows of time were obtained by Sistla and Clarke (1985) and Reynolds (2003,2004). In many cases these investigations resulted in the development and implementationof effective reasoning algorithms (see, e.g., Wolper, 1985; Smith & Park, 1992; Egenhofer& Sharma, 1993; Schwendimann, 1998; Fisher, Dixon, & Peim, 2001; Renz & Nebel, 2001;Hustadt & Konev, 2003).
c 2005 AI Access Foundation. All rights reserved.

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
.
space
X
X
X
X
X
.
F
E
0
1
2
3
time
Figure 1: Topological temporal model.
The next apparent and natural step is to combine these two kinds of reasoning. Of
course, there have been attempts to construct spatio-temporal hybrids. For example, theintended interpretation of Clarke’s (1981, 1985) region-based calculus was spatio-temporal.Region connection calculus RCC (Randell et al., 1992) contained a function space(X, t)for representing the space occupied by object X at moment of time t. Muller (1998a)developed a first-order theory for reasoning about motion of spatial entities. However, allof these formalisms turn out to be ‘too expressive’ from the computational point of view:they are undecidable. Moreover, as far as we know, no serious attempts to investigate andimplement partial (say, incomplete) algorithms capable of spatio-temporal reasoning withthese logics have been made.
The problem of constructing spatio-temporal logics with better algorithmic proper-
ties and analysing their computational complexity was first attacked by Wolter and Za-kharyaschev (2000b); see also the ‘popular’ and extended version (Wolter & Zakharyaschev,2002) of that conference paper, as well as (Bennett & Cohn, 1999; Bennett, Cohn, Wolter,& Zakharyschev, 2002; Gerevini & Nebel, 2002).
The main idea underlying all these papers is to consider various combinations of ‘well-
behaved’ spatial and temporal logics.
The intended spatio-temporal structures can be
regarded then as the Cartesian products of the intended time-line and topological (or someother) spaces that are used to model the spatial dimension. Figure 1 shows such a product(of the flow of time F = N, < and the two-dimensional Euclidean space T) with a movingspatial object X. The moving object can be viewed either as a 3D spatio-temporal entity(in this particular case) or as the collection of the ‘snapshots’ or slices of this entity at eachmoment of time; for a discussion see, e.g., (Muller, 1998b) and references therein. In thispaper, we use the snapshot terminology and understand by a moving spatial object (or,more precisely, interpret such an object as) any set of pairs X, t where, for each point t
168

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
of the flow of time, X is a subset of the topological space—the state of the spatial object atmoment t.
The expressive power (and consequently the computational complexity) of the combined
spatio-temporal formalisms obviously depends on three parameters:
1. the expressivity of the spatial component,
2. the expressivity of the temporal component, and
3. the interaction between the two components allowed in the combined logic.
Regardless of the chosen component languages, the minimal requirement for a spatio-temporal combination to be useful is its ability to
express changes in time of the truth-values of purely spatial propositions.
(PC)
Typical examples of logics meeting this spatial propositions’ truth change principle are thecombinations of RCC-8 and Allen’s interval calculus (Bennett et al., 2002; Gerevini & Nebel,2002) and those combinations of RCC-8 and PT L introduced by Wolter and Zakharyaschev(2000b) that allow applications of temporal operators to Boolean combinations of RCC-8 re-lations. Languages satisfying (PC) can capture, for instance, some aspects of the continuityof change principle (see, e.g., Cohn, 1997) such as
(A) if two images on the computer screen are disconnected now, then they either remain
disconnected or become externally connected in one quantum of the computer’s time.
Another example is the following statement about the geography of Europe:
(B) Kaliningrad is disconnected from the EU until the moment when Poland becomes
a tangential proper part of the EU, after which Kaliningrad and the EU will beexternally connected forever.
However, languages meeting (PC) do not necessarily satisfy our second fundamental
spatial object change principle according to which we should be able to
express changes or evolutions of spatial objects in time.
(OC)
In logical terms, (PC) refers to the change of truth-values of propositions, while (OC) tothe change of extensions of predicates; see Fig. 2 where
X at moment t denotes the state
of X at moment t + 1. Here are some examples motivating (OC):
(C) Continuity of change: ‘the cyclone’s current position overlaps its position in an hour.’
(D) Two physical objects cannot occupy the same space: ‘if tomorrow object X is at the
place where object Y is today, then Y will have to move by tomorrow.’
(E) Geographic regions change: ‘the space occupied by Europe never changes.’
(F) Geographic regions change: ‘in two years the EU will be extended with Romania and
Bulgaria.’
(G) Fairness conditions on regions: ‘it will be raining over every part of England ever and
ever again.’
169

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
.
X
space
X
X
X
X
T
T
T
.
F
E
t
t + 1
t + 2
time
Figure 2: Temporal operators on regions.
(H) Mutual exclusion: ‘if Earth consists of water and land, and the space occupied by
water expands, then the space occupied by land shrinks.’
It should be clear that to represent these statements we have to refer to the evolution ofspatial objects in time (say, to compare objects X and
X)—it is not enough to only take
into account the change of the truth-values of propositions speaking about spatial objects.
The main aim of this paper is to investigate the trade-off between the expressive power
and the computational behaviour of spatio-temporal hybrids satisfying the (PC) and (OC)principles and interpreted in various spatio-temporal structures. Our purpose is to showwhat computational obstacles one can expect if the application domain requires this or thatkind of interactions between temporal and spatial operators.
The spatio-temporal logics we consider below are combinations of fragments of PT L
interpreted over different flows of time with fragments of the propositional spatial logic S4u(equipped with the interior and closure operators, the universal and existential quantifiersover points in space as well as the Booleans) interpreted in topological spaces. This choiceis motivated by the following reasons:
• The component logics are well understood and established in temporal and spatial
knowledge representation; all of them are supported by reasonably effective reasoningprocedures.
• By definition, implicit or explicit temporal quantification is necessary to capture (OC),
and fragments of PT L are the weakest languages with such quantification we know of.
170

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Allen’s interval calculus, for example, does not provide means for any quantificationover intervals. It is certainly suitable for spatio-temporal hybrids satisfying (PC) (seeBennett et al., 2002; Gerevini & Nebel, 2002) but there is no natural conservativeway of combining it with spatial formalisms to meet (OC). On the other hand, it isembedded in PT L (Blackburn, 1992). A natural alternative to PT L would be theextension of Allen’s calculus by means of quantification over intervals introduced byHalpern and Shoham (1986), but unfortunately this temporal logic turns out to behighly undecidable.
• Although the logic S4u was originally introduced in the realm of modal logic (see
below for details), the work of Bennett (1994), Nutt (1999), Renz (2002) and Wolterand Zakharyaschev (2000a) showed that it can be regarded as a unifying languagethat contains many spatial formalisms like RCC-8, BRCC-8 or the 9-intersections ofEgenhofer and Herring (1991) as fragments.
Apart from the choice of component languages and the level of their interaction, the ex-
pressive power and the computational complexity of spatio-temporal logics strongly dependon the restrictions we may want to impose on the intended spatio-temporal structures andthe interpretations of spatial objects.
• We can choose among different flows of time (say, discrete or dense, infinite or finite)
• and among different topological spaces (say, arbitrary, Euclidean or Aleksandrov).
• At each time point we can interpret spatial objects as arbitrary subsets of the topo-
logical space, as regular closed (or open) ones, as polygons, etc.
• To represent the assumption that everything eventually comes to an end, we only
do not know when, one can restrict the class of intended models by imposing thefinite change assumption which states that no spatial object can change its spatialconfiguration infinitely often, or the more ‘liberal’ finite state assumption accordingto which every spatial object can have only finitely many possible states (although itmay change its states infinitely often).
The paper is organised as follows. In Section 2 we introduce in full detail the component
spatial and temporal logics to be combined later on. In particular, besides the standardspatial logics like RCC-8 or the 9-intersections of Egenhofer and Herring (1991), we considertheir generalisations in the framework of S4u and investigate the computational complex-ity. For example, we show that the maximal fragment of S4u dealing with regular closedspatial objects turns out to be PSPACE-complete, while a natural generalisation of the9-intersections is still in NP. In Section 3 we introduce a hierarchy of spatio-temporal logicsoutlined above, provide them with a topological-temporal semantics, and analyse their com-putational properties. First we show that spatio-temporal logics satisfying only the (PC)principle are not more complex than their components. Then we consider ‘maximal’ com-binations of S4u with (fragments of) PT L meeting both (PC) and (OC) and see that thisstraightforward approach does not work: the resulting logics turn out to be undecidable.Finally, we systematically investigate the trade-off between expressivity and complexity ofspatio-temporal formalisms and construct a hierarchy of decidable logics satisfying (PC)
171

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
and (OC) whose complexity ranges from PSPACE to 2EXPSPACE. These and other res-ults, possible implementations as well as open problems are discussed in Section 4. For thereader’s convenience most important (un)decidability and complexity results obtained inthis paper are summarised in Table 1 on page 193. All technical definitions and detailedproofs can be found in the appendices.
2. Propositional Logics of Space and Time
We begin by introducing and discussing the spatial and the temporal formalisms we aregoing to combine later on in this paper.
2.1 Logics of Space
We will be dealing with a number of logics suitable for qualitative spatial representationand reasoning: the well-known RCC-8, BRCC-8 and S4u, as well as certain fragments of thelast one. The intended interpretations for all of these logics are topological spaces.
A topological space is a pair T = U, I in which U is a nonempty set, the universe of
the space, and I is the interior operator on U satisfying the standard Kuratowski axioms:for all X, Y ⊆ U ,
I(X ∩ Y ) = IX ∩ IY,
IX ⊆ IIX,
IX ⊆ X
and
IU = U.
The operator dual to I is called the closure operator and denoted by C: for every X ⊆ U ,we have CX = U − I(U − X). Thus, IX is the interior of a set X, while CX is its closure.X is called open if X = IX and closed if X = CX. The complement of an open set isclosed and vice versa. The boundary of a set X ⊆ U is defined as CX − IX. Note that Xand U − X have the same boundary.
2.1.1 S4u
Our most expressive spatial formalism is S4u—i.e., the propositional modal logic S4 ex-tended with the universal modalities. The ‘pedigree’ of this logic is quite unusual. S4 wasintroduced independently by Orlov (1928), Lewis (in Lewis & Langford, 1932), and G¨
odel
(1933) without any intention to reason about space. Orlov and G¨
odel understood it as
a logic of ‘provability’ (in order to provide a classical interpretation for the intuitionisticlogic of Brouwer and Heyting) and Lewis as a logic of necessity and possibility, that is, asa modal logic. Besides the Boolean connectives and propositional variables, the language ofS4 contains two modal operators: I (it is necessary or provable) and C, the dual of I (it ispossible or consistent). In other words, the formulas of S4 can be defined as follows:
τ
::=
p
|
τ
|
τ1
τ2
|
Iτ,
(1)
where the p are variables. Set Cτ = Iτ . We denote the modal operators by I and C(rather than the conventional 2 and 3) because we understand, following an observationmade by several logicians in the late thirties and early forties (Stone, 1937; Tarski, 1938;Tsao Chen, 1938; McKinsey, 1941), S4 as a logic of topological spaces: if we interpret thepropositional variables as subsets of a topological space, the Booleans as the standard set-theoretic operations, and I and C as, respectively, the interior and the closure operators
172

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
on the space, then an S4-formula is modally consistent if and only if it is satisfiable in atopological space—i.e., its value is not empty under some interpretation.1
More precisely, a topological model is a pair of the form M = T, U , where T = U, I
is a topological space and U, a valuation, is a map associating with every variable p a setU(p) ⊆ U . Then the valuation U is inductively extended to arbitrary S4-formulas by taking:
U(τ ) = U − U(τ ),
U(τ1
τ2) = U(τ1) ∩ U(τ2),
U(Iτ ) = IU(τ ).
Expressions τ of the form (1) are interpreted as subsets of topological spaces; that is why wewill call them spatial terms. In particular, propositional variables of S4 will be understoodas spatial variables.
The language of S4u extends S4 with the universal and the existential quantifiers 2
∀
and 3
∃ , respectively (known in modal logic as the universal modalities ). Given a spatial
term τ , we write 3
∃ τ to say that the part of space (represented by) τ is not empty (there is
at least one point in τ ); 2
∀ τ means that τ occupies the whole space (all points belong to τ ).
By taking Boolean combinations of such expressions we arrive at what will be called spatialformulas. A BNF definition looks as follows:2
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2,
where the τ are spatial terms. Set 3
∃ τ = ¬2
∀ τ . Spatial formulas can be either true or false in
topological models. The truth-relation M |= ϕ—a spatial formula ϕ is true in a topologicalmodel M—is defined in the standard way:
• M |= 2∀τ
iff
U(τ ) = U ,
• M |= ¬ϕ
iff
M |= ϕ,
• M |= ϕ1 ∧ ϕ2
iff
M |= ϕ1 and M |= ϕ2.
Say that a spatial formula ϕ is satisfiable if there is a topological model M such that M |= ϕ.
The seemingly simple ‘query language’ S4u can express rather complex relations between
sets in topological spaces. For example, the formula
2∀(q
p) ∧ 2
∀ (p
Cq) ∧ 3
∃ p ∧ ¬3
∃ Iq
says that a set q is dense in a nonempty set p, but has no interior (here τ1
τ2 is an
abbreviation for τ1
τ2).
The following ‘folklore’ complexity result has been proved in different settings (see, e.g.,
Nutt, 1999; Areces, Blackburn, & Marx, 2000):
Theorem 2.1. (i) S4u enjoys the exponential finite model property; i.e., every satisfiablespatial formula ϕ is satisfiable in a topological space whose size is at most exponential inthe size of ϕ.
(ii) Satisfiability of spatial formulas in topological models is PSPACE-complete.
1. Moreover, according to McKinsey (1941) and McKinsey and Tarski (1944), any n-dimensional Euclidean
space, for n ≥ 1, is enough to satisfy all consistent S4-formulas.
2. Formally, the language of S4u as defined above is weaker than the standard one, say, that of Goranko
and Passy (1992). However, one can easily show that they have precisely the same expressive power:see, e.g., (Hughes & Cresswell, 1996) or (Aiello & van Benthem, 2002b).
173

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
One way of proving this theorem is first to observe that every satisfiable spatial formula
is satisfied in an Aleksandrov model, i.e., a model based on an Aleksandrov topologicalspace—alias a standard Kripke frame for S4 (see, e.g., McKinsey & Tarski, 1944; Goranko& Passy, 1992).
We remind the reader that a topological space is called an Aleksandrov space (Alexan-
droff, 1937) if arbitrary (not only finite) intersections of open sets are open. A Kripke frame(or simply a frame) for S4 is a pair the form G = V, R , where V is a nonempty set andR a transitive and reflexive relation (i.e., a quasi-order ) on V . Every such frame G inducesthe interior operator IG on V : for every X ⊆ V ,
IGX = x ∈ X | ∀y ∈ V (xRy → y ∈ X).
In other words, the open sets of the topological space TG = V, IG are the upward closed(or R-closed ) subsets of V . The minimal neighbourhood of a point x in TG (that is theminimal open set to contain x) consists of all those points that are R-accessible from x. Itis well-known (see, e.g., Bourbaki, 1966) that TG is an Aleksandrov space and, conversely,every Aleksandrov space is induced by a quasi-order.
Now, to complete the proof, it suffices to recall that S4 is PSPACE-hard (Ladner,
1977) and use, say, the standard tableau technique to establish the exponential finite modelproperty and construct a PSPACE satisfiability checking algorithm for spatial formulas.
Although being of the same computational complexity as S4, the logic S4u is more
expressive. A standard example is that spatial formulas can distinguish between arbitraryand connected3 topological spaces. Consider, for instance, the formula
2∀(Cp
p) ∧ 2
∀ (p
Ip) ∧ 3
∃ p ∧ ¬2
∀ p
(2)
saying that p is both closed and open, nonempty and does not coincide with the whole space.It can be satisfied only in a model whose underlying topological space is not connected, whileall satisfiable S4-formulas are satisfied in connected (e.g., Euclidean) spaces.
Another example illustrating the expressive power of S4u is the formula
3∃p ∧ 2∀(p
Cp) ∧ 2
∀ (p
Cp)
(3)
defining a nonempty set p such that both p and p have empty interiors. In fact, the secondand the third conjuncts say that p and p consist of boundary points only.
2.1.2 RCC-8 as a Fragment of S4u
In qualitative spatial representation and reasoning, it is quite often assumed that spatialterms can only be interpreted by regular closed (or open) sets of topological spaces (see,e.g., Davis, 1990; Asher & Vieu, 1995; Gotts, 1996). One of the reasons for imposing thisrestriction is to exclude from consideration such ‘pathological’ sets as p in (3). Recall that aset X is regular closed if X = CIX, which clearly does not hold for any set p satisfying (3).Another reason is to ensure that the space occupied by a physical body is homogeneousin the sense that it does not contain parts of ‘different dimensionality.’ For example, the
3. We remind the reader that a topological space is connected if its universe cannot be represented as the
union of two disjoint nonempty open sets.
174

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
.
X
IX
CIX
.
Figure 3: Regular closure.
subset X of the Euclidean plane in Fig. 3 consists of three parts: a 2D ellipse with a hole, a2D circle, and a 1D curve connecting them. This curve disappears if we form the set CIX,which is regular closed because CICIX = CIX, for every X and every topological space.
In this paper, we will consider several fragments of S4u dealing with regular closed sets.
From now on we will call such sets regions. Perhaps, the best known language devisedfor speaking about regions is RCC-8 which was introduced in the area of GeographicalInformation Systems (see Egenhofer & Franzosa, 1991; Smith & Park, 1992) and as adecidable subset of Region Connection Calculus RCC (Randell et al., 1992). The syntax ofRCC-8 contains eight binary predicates,
• DC(X, Y ) — regions X and Y are disconnected,
• EC(X, Y ) — X and Y are externally connected,
• EQ(X, Y ) — X and Y are equal,
• PO(X, Y ) — X and Y partially overlap,
• TPP(X, Y ) — X is a tangential proper part of Y ,
• NTPP(X, Y ) — X is a nontangential proper part of Y ,
• the inverses of the last two—TPPi(X, Y ) and NTPPi(X, Y ),
which can be combined using the Boolean connectives. For example, given a spatial databasedescribing the geography of Europe, we can query whether the United Kingdom and theRepublic of Ireland share a common border. The answer can be found by checking whetherthe RCC-8 formula EC(UK, RoI) follows from the database.
The arguments of the RCC-8 predicates are called region variables; they are interpreted
by regular closed sets—i.e., regions—of topological spaces. The satisfiability problem forRCC-8 formulas under such interpretations is NP-complete (Renz & Nebel, 1999).
The expressive power of RCC-8 is rather limited. It only operates with ‘simple’ re-
gions and does not distinguish between connected and disconnected ones, regions with andwithout holes, etc. (Egenhofer & Herring, 1991). Nor can RCC-8 represent complex rela-tions between more than two regions. Consider, for example, three countries (say, Russia,Lithuania and Poland) such that not only each one of them is adjacent to the others, butthere is a point where all the three meet. To express this fact we may need a ternarypredicate like
EC3(Russia, Lithuania, Poland).
(4)
175

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
To analyse possible ways of extending the expressive power of RCC-8, it will be conveni-
ent to view it as a fragment of S4u (that RCC-8 can be embedded into S4u was first shownby Bennett, 1994). Observe first that, for every spatial variable p, the spatial term
CIp
(5)
is interpreted as a regular closed set in every topological model. So, with every regionvariable X of RCC-8 we can associate the spatial term X = CIpX , where pX is a spatialvariable, and then translate the RCC-8 predicates into spatial formulas by taking:
EC(X, Y ) = 3
∃ ( X
Y ) ∧ ¬3
∃ (I X
I Y ),
DC(X, Y ) = ¬3
∃ ( X
Y ),
EQ(X, Y ) = 2
∀ ( X
Y ) ∧ 2
∀ ( Y
X ),
PO(X, Y ) = 3
∃ (I X
I Y ) ∧ ¬2
∀ ( X
Y ) ∧ ¬2
∀ ( Y
X ),
TPP(X, Y ) = 2
∀ ( X
Y ) ∧ ¬2
∀ ( Y
X ) ∧ ¬2
∀ ( X
I Y ),
NTPP(X, Y ) = 2
∀ ( X
I Y ) ∧ ¬2
∀ ( Y
X )
(TPPi and NTPPi are the mirror images of TPP and NTPP, respectively). The first of theseformulas, for instance, says that two regions are externally connected iff the intersection ofthe regions is not empty, whereas the intersection of their interiors is. It should be clearthat an RCC-8 formula is satisfiable in a topological space if and only if its translation intoS4u defined above is satisfiable in a topological model.
This translation also shows that in RCC-8 any two regions can be related in terms of
truth/falsity of atomic spatial formulas of the form
2∀( 1
2),
2∀(I 1 I 2),
2∀( 1
2)
and
2∀( 1
I 2),
where 1 and 2 are spatial terms of the form (5). For example, the first of these formulassays that the intersection of two regions is empty, whereas the last one states that one regionis contained in the interior of another one. In other words, RCC-8 can be regarded as partof the following fragment of S4u:
::=
CIp,
τ
::=
1
2
|
I 1
I 2
|
1
2
|
1
I 2,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2.
Here we distinguish between two types of spatial terms.
Those of the form
will be
called atomic region terms—they represent the (regular closed) regions we want to compare.Spatial terms of the form τ are used to relate regions to each other (note that their extensionsare not necessarily regular closed).
Actually, the fragment introduced above is a bit more expressive than RCC-8: for ex-
ample, it contains (appropriately modified) formula (2) which can be satisfied only in dis-connected topological spaces, while all satisfiable RCC-8 formulas are satisfiable in anyEuclidean space (Renz, 1998). However, it will be convenient for us not to distinguishbetween these two spatial logics. First, it will turn out that the same technical results re-garding their computational complexity hold for them even when combined with temporal
176

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
logics. And second, the more intuitive and concise language of RCC-8 is more suitable forillustrations. For instance, we do not distinguish between the region variable X and theregion term X and use DC( 1, 2) as an abbreviation for ¬3
∃ ( 1
2).
The definition above suggests two ways of increasing the expressive power of RCC-8
(while keeping all regions regular closed):
(i) by allowing more complex region terms , and
(ii) by allowing more ways of relating them (i.e., more complex terms τ ).
2.1.3 BRCC-8 as a Fragment of S4u
The language BRCC-8 of Wolter and Zakharyaschev (2000a) (see also Balbiani, Tinchev, &Vakarelov, 2004) extends RCC-8 in direction (i). It uses the same eight binary predicatesas RCC-8 and allows not only atomic regions but also their intersections, unions and com-plements. For instance, in BRCC-8 we can express the fact that a region (say, the SwissAlps) is the intersection of two other regions (Switzerland and the Alps in this case):
EQ(SwissAlps, Switzerland
Alps).
(6)
We can embed BRCC-8 to S4u by using almost the same translation as in the case of RCC-8.The only difference is that now, since Boolean combinations of regular closed sets are notnecessarily regular closed, we should prefix compound spatial terms with CI. This way wecan obtain, for example, the spatial term
CI (Switzerland
Alps)
representing the Swiss Alps. In the same manner we can treat other set-theoretic operations,which leads us to the following definition of Boolean region terms:
::=
CIp
|
CI
|
CI( 1
2).
In other words, Boolean region terms denote precisely the members of the well-knownBoolean algebra of regular closed sets. (The union
is expressible via intersection and
complement in the usual way.) To simplify notation, given a spatial term τ , we write τto denote the result of prefixing CI to every subterm of τ ; in particular,
p = CIp,
τ = CI τ
and
τ1
τ2 = CI( τ1
τ2 ).
Note that τ
is (equivalent to) a Boolean region term, for every spatial term τ . Now the
Swiss Alps from the example above can be represented as Switzerland
Alps .
It is of interest to note that Boolean region terms do not increase the complexity of
reasoning in arbitrary topological models: the satisfiability problem for BRCC-8 formulas isstill NP-complete (however, it becomes PSPACE-complete if all intended models are basedon connected spaces). On the other hand, BRCC-8 allows some restricted comparisons ofmore than two regions as, e.g., in (6). Nevertheless, as we shall see below, ternary relationslike (4) are still unavailable in BRCC-8: they require different ways of comparing regions;cf. (ii).
177

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
2.1.4 RC
Egenhofer and Herring (1991) proposed to relate any two regions in terms of the 9-inter-sections—3×3-matrix specifying emptiness/nonemptiness of all (nine) possible intersectionsof the interiors, boundaries and exteriors of the regions. Recall that, for a region X, thesethree disjoint parts of the space U, I can be represented as
IX,
X ∩ (U − IX)
and
U − X,
respectively. By generalising this approach to any finite number of regions, we obtain thefollowing fragment RC of S4u:
::=
Boolean region terms,
τ
::=
|
I
|
τ
|
τ1
τ2,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2.
In other words, in RC we can define relations between regions in terms of emptiness/non-emptiness of sets formed by using arbitrary set-theoretic operations on regions and theirinteriors. However, nested applications of the topological operators are not allowed (anexample where such applications are required can be found in the next section).
Clearly, both RCC-8 and BRCC-8 are fragments of RC. Moreover, unlike BRCC-8, the
language of RC allows us to consider more complex relations between regions. For instance,the ternary relation required in (4) can now be defined as follows:
EC3(X, Y, Z) = 3
∃ ( X
Y
Z ) ∧ ¬3
∃ (I X
I Y ) ∧ ¬3
∃ (I Y
I Z) ∧ ¬3
∃ (I Z
I X ).
Another, more abstract, example is the formula
3∃ 1 · · ·
i ∧ I i+1
· · ·
I j
j+1
· · ·
k
I k+1
· · ·
I n
which says that
regions
1, . . . ,
i meet somewhere inside the region occupied jointly by all
i+1, . . . ,
j , but outside the regions
j+1, . . . ,
k and not inside
k+1, . . . ,
n.
Although RC is more expressive than both RCC-8 and BRCC-8, reasoning in this lan-
guage is still of the same computational complexity:
Theorem 2.2. The satisfiability problem for RC-formulas in arbitrary topological modelsis NP-complete.
This result will be proved in Appendix A. Lemma A.1 shows that every satisfiable RC-
formula can be satisfied in a model based on the Aleksandrov space that is induced by adisjoint union of n-brooms—i.e., quasi-orders of the form depicted in Fig. 4. Topologicalspaces of this kind have a rather primitive structure satisfying the following property:
(rc) only the roots of n-brooms can be boundary points, and the minimal neighbourhood
of every boundary point—i.e., the n-broom containing this point—must contain atleast one internal point and at least one external point.
178

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
˜
˜
˜
˜
depth 0
r
‰
¨
B
r
t
“

0
¨
r
¨
t

r
¨
r
t
r ˜
¨

¨
depth 1
Figure 4: n-broom (for n = 4).
For example, spatial formula (3) cannot be satisfied in a model with this property, and soit is not in RC.
By Lemma A.2, the size of such a satisfying model is polynomial (in fact, quadratical)
in the length of the input RC-formula, and so we have a nondeterministic polynomial timealgorithm. Actually, the proof is a straightforward generalisation of the complexity prooffor BRCC-8 given by Wolter and Zakharyaschev (2000a): the only difference is that in thecase of BRCC-8 it is sufficient to consider only 2-brooms (which were called forks). Thismeans, in particular, that ternary relation (4)—which is satisfiable only in a model with ann-broom, for n ≥ 3—is indeed not expressible in BRCC-8.
Remark 2.3. In topological terms, n-brooms are examples of so-called door spaces whereevery subset is either open or closed. However, the modal theory of n-brooms defines awider and more interesting topological class known as submaximal spaces in which everydense subset is open. Submaximal spaces have been around since the early 1960s and havegenerated interesting and challenging problems in topology. For a survey and a systematicstudy of these spaces see (Arhangel’skii & Collins, 1995) and references therein.
2.1.5 RCmax
One could go even further in direction (ii) and impose no restrictions whatsoever on theways of relating Boolean region terms. This leads us to the maximal fragment RCmax ofS4u in which spatial terms are interpreted by regular closed sets. Its syntax is defined asfollows:
::=
Boolean region terms,
τ
::=
|
τ
|
τ1
τ2
|
Iτ,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2,
To understand the difference between RC and RCmax, consider the RCmax-formula
3∃ q1
I q1
∧ 2∀
q1
I q1
C I q1
q2
I q2
.
(7)
It says that the boundary of
q1 is not empty and that every neighbourhood of every
point in this boundary contains an internal point of q1 that belongs to the boundary of
q2 (compare with property (rc) above). The simplest Aleksandrov model satisfying this
formula is of depth 2; it is shown in Fig. 5.
The price we have to pay for this expressivity is that the complexity of RCmax is the
same as that of full S4u:
179

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
q1 q˜2
q1 q
˜ 2
q1 q
˜ 2
depth 0
t
“

0


0
t


t
q
˜
1 q2

depth 1

t
“
t

t
q
˜
1 q2
depth 2
Figure 5: Model satisfying formula (7).
Theorem 2.4. The satisfiability problem for RCmax-formulas is PSPACE-complete.
The upper bound follows from Theorem 2.1 and the lower bound is proved in Ap-
pendix A, where we construct a sequence of RCmax-formulas such that each of them issatisfiable in an Aleksandrov space of cardinality at least exponential in the length of theformula. The first formula of the sequence is similar to (7) above.
It is of interest to note, however, that RCmax is still not expressive enough to define such
‘pathological’ sets as p in (3) which is clearly not regular closed.
To conclude this section, we summarise the inclusions between the spatial languages
introduced above:
RCC-8
BRCC-8
RC
RCmax
S4u.
For more discussions of spatial logics of this kind we refer the reader to the paper (Pratt-Hartmann, 2002).
2.2 Temporal Logics
As was said in the introduction, the temporal components of our spatio-temporal hybridsare (fragments of) the propositional temporal logic PT L interpreted in various flows of timewhich are modelled by strict linear orders F = W, < , where W is a nonempty set of timepoints and < is a (connected, transitive and irreflexive) precedence relation on W .
The language PT L is based on the following alphabet:
• propositional variables p0, p1, . . . ,
• the Booleans ¬ and ∧, and
• the binary temporal operators U (‘until’) and S (‘since’).
The set of PT L-formulas is defined in the standard way:
ϕ
::=
p
|
¬ϕ
|
ϕ1 ∧ ϕ2
|
ϕ1 U ϕ2
|
ϕ1 S ϕ2.
PT L-models are pairs of the form M = F, V such that F = W, < is a flow of timeand V, a valuation, is a map associating with each variable p a set V(p) ⊆ W of timepoints (where p is supposed to be true). The truth-relation (M, w) |= ϕ, for an arbitraryPT L-formula ϕ and w ∈ W , is defined inductively as follows, where (u, v) denotes the openinterval w ∈ W | u < w < v:
180

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
• (M, w) |= p
iff
w ∈ V(p),
• (M, w) |= ¬ϕ
iff
(M, w) |= ϕ,
• (M, w) |= ϕ1 ∧ ϕ2
iff
(M, w) |= ϕ1 and (M, w) |= ϕ2,
• (M, w) |= ϕ1 U ϕ2
iff
there is v > w such that (M, v) |= ϕ2 and (M, u) |= ϕ1 for
all u ∈ (w, v),
• (M, w) |= ϕ1 S ϕ2
iff
there is v < w such that (M, v) |= ϕ2 and (M, u) |= ϕ1 for
all u ∈ (v, w).
A PT L-formula ϕ is satisfied in M if (M, w) |= ϕ for some w ∈ W .
We took the operators U and S as primitive simply because all other important temporal
operators can be defined via them. For example, 3F (‘sometime in the future’) and 2F(‘always in the future’) are expressible via U as
3F ϕ = U ϕ,
2F ϕ = ¬3F ¬ϕ,
(
is the logical constant ‘true’) which means that
• (M, w) |= 3F ϕ
iff
there is v > w such that (M, v) |= ϕ,
• (M, w) |= 2F ϕ
iff
(M, v) |= ϕ for all v > w.
As our intended flows of time are strict linear orders, the ‘next-time’ operator
is also
definable via U by taking
ϕ = ⊥ U ϕ
(⊥ is the logical constant ‘false’) which perfectly reflects our intuition: if F is discrete then
• (M, w) |=
ψ
iff
(M, w + 1) |= ψ,
where w + 1 is the immediate successor of w in F. The reader should not have problems indefining the ‘past’ versions of 3F , 2F and
.
The following results are due to Sistla and Clarke (1985) and Reynolds (2003, 2004):
Theorem 2.5. The satisfiability problem for PT L-formulas is PSPACE-complete for eachof the following classes of flows of time: all strict linear orders, all finite strict linear orders,
N, < , Z, < , Q, < , R, < .
Note, however, that reasoning becomes somewhat simpler if we take 3F , 2F and their
past counterparts (but no
, U and S) as the only temporal primitives. Denote by PT L2
the corresponding fragment of PT L. Then, according to the results of Ono and Nakamura(1980), Sistla and Clarke (1985), and Wolter (1996), we have:
Theorem 2.6. The satisfiability problem for PT L2-formulas is NP-complete for each ofthe classes of flows of time mentioned in Theorem 2.5.
181

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
3. Combinations of Spatial and Temporal Logics
In this section we introduce and discuss various ways of combining logics of space and time.First we construct spatio-temporal logics satisfying only the (PC) principle (see the intro-duction) and show that they inherit good computational properties of their components.Being encouraged by these results, we then consider ‘maximal’ combinations of S4u with(fragments of) PT L meeting both (PC) and (OC) and see that such a straightforward ap-proach does not work: we end up with undecidable logics. This leads us to a systematicinvestigation of the trade-off between expressivity and computational complexity of spatio-temporal formalisms. The result is a hierarchy of decidable logics satisfying (PC) and (OC)whose complexity ranges from PSPACE to 2EXPSPACE.
3.1 Spatio-Temporal Logics with (PC)
We begin our investigation of combinations of the spatial and temporal logics introducedabove by considering the language PT L[S4u] in which the temporal operators can be appliedto spatial formulas but not to spatial terms (this way of ‘temporalising’ a logic was firstintroduced by Finger and Gabbay, 1992). A precise syntactic definition of PT L[S4u]-termsτ and PT L[S4u]-formulas ϕ is as follows:
τ
::=
p
|
τ
|
τ1
τ2
|
Iτ,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2 | ϕ1 U ϕ2 | ϕ1 S ϕ2.
Note that the definition of PT L[S4u]-terms coincides with the definition of spatial termsin S4u which reflects the fact that PT L[S4u] cannot capture the change of spatial objectsin time. We have imposed no restrictions upon the temporal operators in formulas—so thecombined language still has the full expressive power of PT L. (Clearly, S4u is a fragmentof PT L[S4u].)
In a similar way we can introduce spatio-temporal logics based on all other spatial
languages we are dealing with: RCC-8, BRCC-8, RC and RCmax. For example, the tem-poralisation PT L[BRCC-8] of BRCC-8 (denoted by ST 0 in the hierarchy of Wolter andZakharyaschev 2002) allows applications of the temporal operators to RCC-8 predicates butnot to Boolean region terms. These languages can be regarded as fragments of PT L[S4u]in precisely the same way as their spatial components were treated as fragments of S4u.
We illustrate the expressive power of PT L[RCC-8] by formalising sentences (A) and (B)
from the introduction:
DC(Image1, Image2) → DC(Image1, Image2) ∨ EC(Image1, Image2),
(A)
DC(Kaliningrad, EU) U TPP(Poland, EU) ∧
(B)
2F TPP(Poland, EU) → EC(Kaliningrad, EU) .
Sentences (C)–(H) cannot be expressed in this language (or even in PT L[S4u]): they requirecomparisons of states of spatial objects at different time instants.
The intended semantics of PT L[S4u] (and all other spatio-temporal logics considered
in this paper) is rather straightforward. A topological temporal model (a tt-model, for short)is a triple of the form M = F, T, U , where F = W, < is a flow of time, T = U, I a
182

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
topological space, and U, a valuation, is a map associating with every spatial variable pand every time point w ∈ W a set U(p, w) ⊆ U —the ‘space’ occupied by p at momentw; see Fig. 1. The valuation U is inductively extended to arbitrary PT L[S4u]-terms (i.e.,spatial terms) in precisely the same way as for S4u, we only have to add a time point as aparameter:
U(τ , w) = U − U(τ, w),
U(τ1
τ2, w) = U(τ1, w) ∩ U(τ2, w),
U(Iτ, w) = IU(τ, w).
The truth-values of PT L[S4u]-formulas are defined in the same way as for PT L:
• (M, w) |= 2∀τ
iff
U(τ, w) = U ,
• (M, w) |= ¬ϕ
iff
(M, w) |= ϕ,
• (M, w) |= ϕ1 ∧ ϕ2
iff
(M, w) |= ϕ1
and
(M, w) |= ϕ2,
• (M, w) |= ϕ1 U ϕ2
iff
there is v > w such that (M, v) |= ϕ2 and (M, u) |= ϕ1 for
all u ∈ (w, v),
• (M, w) |= ϕ1 S ϕ2
iff
there is v < w such that (M, v) |= ϕ2 and (M, u) |= ϕ1 for
all u ∈ (v, w).
And as in the pure temporal case, the operators 2F , 3F ,
as well as their past counterparts
can be defined in terms of U and S.
A PT L[S4u]-formula ϕ is said to be satisfiable if there exists a tt-model M such that
(M, w) |= ϕ for some time point w.
The following optimal complexity result will be obtained in Appendix B.1:
Theorem 3.1. The satisfiability problem for PT L[S4u]-formulas in tt-models based onarbitrary flows of time, (arbitrary) finite flows of time, N, < , Z, < , Q, < , or R, < , isPSPACE-complete.
The proof of this theorem is based on the fact that the interaction between spatial and
temporal components of PT L[S4u] is very restricted. In fact, for every PT L[S4u]-formula ϕone can construct a PT L-formula ϕ∗ by replacing every occurrence of a (spatial) subformula2∀τ in ϕ with a fresh propositional variable pτ. Then, given a PT L-model N = F, V forϕ∗ and a moment of time w, we take the set
Φw = 2
∀ τ | (N, w) |= pτ  ∪ ¬2
∀ τ | (N, w) |= ¬pτ 
of spatial formulas. It is not hard to see that if Φw is satisfiable for every w in F, then thereis a tt-model satisfying ϕ and based on the flow F. Now, to check whether ϕ is satisfiable,it suffices to use a suitable nondeterministic algorithm (see, e.g., Sistla & Clarke, 1985;Reynolds, 2003, 2004) which guesses a PT L-model for ϕ∗ and then, for each time point w,to check satisfiability of Φw. This can be done using polynomial space in the length of ϕ.
Theorem 3.1 (together with Theorem 2.5) shows that all spatio-temporal logics of the
form PT L[L], for L ∈ RCC-8, BRCC-8, RC, RCmax, are also PSPACE-complete over thestandard flows of time.
183

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Now let us consider temporalisations of spatial logics with the (NP-complete) frag-
ment PT L2 of PT L. By Theorems 2.4 and 3.1, both PT L2[S4u] and PT L2[RCmax] arePSPACE-complete. However, for simpler (NP-complete) spatial components we obtain abetter result:
Theorem 3.2. The satisfiability problem for PT L2[RC]-formulas in tt-models based oneach of the classes of flows of time mentioned in Theorem 3.1 is NP-complete.
The proof is essentially the same as that of Theorem 3.1, but now nondeterministic
polynomial-time algorithms for the component logics are available. It follows from The-orem 3.2 that PT L2[RCC-8] and PT L2[BRCC-8] are NP-complete as well.
3.2 ‘Maximal’ Combinations with (PC) and (OC)
As we saw in the previous section, the computational complexity of spatio-temporal logicswithout (OC) is the maximum of the complexity of their components, which reflects thevery limited interaction between spatial and temporal operators in languages without anymeans of expressing (OC).
A ‘maximalist’ approach to constructing spatio-temporal logics capable of capturing
both (PC) and (OC) is to allow unrestricted applications of the Booleans, the topologicaland the temporal operators to form spatio-temporal terms.
Denote by PT L × S4u the spatio-temporal language given by the following definition:
τ
::=
p
|
τ
|
τ1
τ2
|
Iτ
|
τ1 U τ2
|
τ1 S τ2,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2 | ϕ1 U ϕ2 | ϕ1 S ϕ2.
Expressions of the form τ will be called spatio-temporal terms. Unlike the previous section,these terms can be time-dependent. The definition of expressions of the form ϕ is thesame as for PT L[S4u]; they will be called PT L × S4u-formulas. All of the languages fromSection 3.1, including PT L[S4u], are clearly fragments of PT L × S4u.
As before, we can introduce the temporal operators 2F , 3F ,
as well as their past
counterparts applicable to formulas. Moreover, these operators can now be used to formspatio-temporal terms: for example,
3F τ = U τ,
2F τ = ¬3F τ and
τ = ⊥ U τ,
where ⊥ denotes the empty set and
the whole space.
Spatio-temporal formulas are supposed to represent propositions speaking about moving
spatial objects represented by spatio-temporal terms. The truth-values of propositions inspatio-temporal structures can vary in time, but do not depend on points of spaces—theyare defined in precisely the same way as in the case of PT L[S4u]. But how to understandtemporalised terms?
The meaning of
τ should be clear: at moment w, it denotes the space occupied by τ
at the next moment w + 1 (see Fig. 2). For example, we can write
3∃ I Cyclone
I
Cyclone
(C)
184

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
to say that regions Cyclone and
Cyclone overlap (thereby formalising sentence (C) from
the introduction). The formula
EQ(
EU, EU
Romania
Bulgaria)
(F)
says that in two years the EU (as it is today) will be extended with Romania and Bulgaria.Note that
EQ(EU, EU
Romania
Bulgaria) has a different meaning because the EU
may expand or shrink in a year. It is also not hard to formalise sentences (D), (E) and (H)from the introduction:
EQ( X, Y ) → ¬EQ(Y,
Y ),
(D)
2F EQ( Europe, Europe),
(E)
EQ(Earth, W
L) ∧ EC(W, L) ∧ P(W,
W ) → P( L, L),
(H)
where P(X, Y )—‘X is a part of Y ’—denotes the disjunction of EQ(X, Y ), TPP(X, Y ) andNTPP(X, Y ).
The intended interpretation of terms of the form 3F τ , 2F τ (and their past counterparts)
is a bit more sophisticated. It reflects the standard temporal meanings of propositions‘3F x ∈ τ ’ and ‘2F x ∈ τ ,’ for all points x in the topological space:
• at moment w, term 3F τ is interpreted as the union of all spatial extensions of τ at
moments v > w;
• at moment w, term 2F τ is interpreted as the intersection of all spatial extensions of
τ at moments v > w.
For example, consider Fig. 2 with moving spatial object X depicted on it at three consecutivemoments of time (it does not change after t + 2). Then 3F X at t is the union of
X and
X at t and 2F X at t is the intersection of
X and
X at t (i.e.,
X).
As another example, take the spatial object Rain. Then
• 3F Rain at moment w occupies the space where it will be raining at some time points
v > w (which may be different for different places). 2F Rain at w occupies the spacewhere it will always be raining after w.
• 2F 3F Rain at w is the space where it will be raining ever and ever again after w,
while 3F 2F Rain comprises all places where it will always be raining starting fromsome future moments of time.
This interpretation shows how to formalise sentence (G) from the introduction:
P(England, 2F 3F Rain).
(G)
Now, what can be the meaning of Rain U Snow? Similarly to the readings of 2F τ and
3F τ above, we adopt the following definition:
• at moment w, the spatial extension of τ1Uτ2 consists of those points x of the topological
space for which there is v > w such that x belongs to τ2 at moment v and x is in τ1at all u whenever w < u < v.
185

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
The past counterpart of U —i.e., the operator ‘since’ S—can be used to say that the part ofRussia that has been remaining Russian since 1917 is not connected to the part of Germany(K¨
onigsberg) that became Russian after the Second World War (Kaliningrad):
DC(Russia S Russian Empire, Russia S Germany).
The models M = F, T, U for PT L × S4u are precisely the same topological temporal
models we introduced for PT L[S4u]. However, now we need additional clauses definingextensions of spatio-temporal terms:
• U(τ1 U τ2, w) =
U(τ2, v) ∩
U(τ1, u) ,
v>w
u∈(w,v)
• U(τ1 S τ2, w) =
U(τ2, v) ∩
U(τ1, u) .
v<w
u∈(v,w)
Then we also have:
U(3F τ, w) =
U(τ, v)
and
U(2F τ, w) =
U(τ, v),
v>w
v>w
and, for discrete F,
U( τ, w) = U(τ, w + 1).
The truth-values of PT L × S4u-formulas are computed in precisely the same way as in thecase of PT L[S4u]. A PT L × S4u-formula ϕ is called satisfiable if there exists a tt-modelM such that (M, w) |= ϕ for some time point w.
At first sight it may appear that the computational properties of the constructed lo-
gic should not be too bad—after all, its spatial and temporal components are PSPACE-complete. It turns out, however, that this is not the case:
Theorem 3.3. The satisfiability problem for PT L × S4u-formulas in tt-models based onthe flows of time N, < or Z, < is undecidable.
Without going into details of the proof of this theorem, one might immediately con-
jecture that it is the use of the infinitary operators U , 2F and 3F in the construction ofspatio-temporal terms that makes the logic ‘over-expressive.’ Moreover, the whole idea oftopological temporal models based on infinite flows of time may look counterintuitive inthe context of spatio-temporal representation and reasoning (unlike, say, models used torepresent the behaviour of reactive computer systems).
There are different approaches to avoid infinity in tt-models. The most radical one is to
allow only finite flows of time. A more cautious approach is to impose the following finitechange assumption on models (based on infinite flows of time):
FCA No term can change its spatial extension infinitely often.
This means that under FCA we consider only those valuations U in tt-models F, T, Uthat satisfy the following condition: for every spatio-temporal term τ , there are pairwisedisjoint intervals I1, . . . , In of F = W, < such that W = I1 ∪ · · · ∪ In and the state of τremains constant on each Ij, i.e., U(τ, u) = U(τ, v) for any u, v ∈ Ij. It turns out, however,
186

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
that in the case of discrete flows of time FCA does not give us anything new as comparedto arbitrary finite flows of time. More precisely, one can easily show that the satisfiabilityproblem for PT L × S4u-formulas in tt-models satisfying FCA and based on N, < or
Z, < is polynomially reducible to satisfiability in tt-models based on finite flows of time,
and the other way round. Note also that for the flows of time mentioned above, FCA canbe captured by the formulas 3F 2F EQ(τ, F τ ) (and its past counterpart for Z, < ), forevery spatio-temporal term τ .
A more ‘liberal’ way of reducing infinite unions and intersections to finite ones is to
adopt the finite state assumption:
FSA Every term may have only finitely many possible states (although it may
change its states infinitely often).
Say that a tt-model F, T, U satisfies FSA if, for every spatio-temporal term τ , there arefinitely many sets A1, . . . , Am in the space T such that U(τ, w) | w ∈ W  = A1, . . . , Am.Such models can be used, for instance, to capture periodic fluctuations due to season orclimate changes, say, a daily tide. Similarly to FCA finitising the flow of time, FSAvirtually makes the underlying topological space finite. The following proposition will beproved in Appendix B:
Proposition 3.4. A PT L × S4u-formula is satisfiable in a tt-model with FSA and baseda flow of time F iff it is satisfiable in a tt-model based on F and a finite (Aleksandrov )topological space.
Unfortunately, none of these approaches works for PT L × S4u—we still have:
Theorem 3.5. (i) The satisfiability problem for PT L × S4u-formulas in tt-models basedon (arbitrary) finite flows of time is undecidable.
(ii) The satisfiability problem for PT L × S4u-formulas in tt-models based on the flows
of time N, < or Z, < and satisfying FSA is undecidable.
The next-time operator
does not look so ‘harmful’ as the infinitary U , 2F , 3F , and
still can capture some aspects of (OC) (see formulas (C), (D), (F) and (G) above). So letus consider the fragment PT L ◦ S4u of PT L × S4u with spatio-temporal terms of the form:
τ
::=
p
|
τ
|
τ1
τ2
|
Iτ
|
τ.
In other words, PT L ◦ S4u does not allow applications of temporal operators different from
to form spatio-temporal terms (but they are still available as formula constructors). This
means that we can compare the states of a spatial object X over a bounded set of timepoints only: for any time point t and any natural numbers n, m ≥ 0, we can compare at tthe state of X at t + n with its state at t + m.
This fragment is definitely less expressive than full PT L × S4u. For instance, according
to Lemma B.1, PT L ◦ S4u-formulas do not distinguish between arbitrary tt-models andthose based on Aleksandrov topological spaces—we will call them Aleksandrov tt-models.On the other hand, the set of PT L × S4u-formulas satisfiable in Aleksandrov models isa proper subset of those satisfiable in arbitrary tt-models.
Consider, for example, the
PT L × S4u-formula
2∀(2F Ip
I2F p).
187

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
One can readily see that it is true in every Aleksandrov tt-model, but its negation can besatisfied in a topological model. For it suffices to take the flow F = N, < and the topologyT = R, I with the standard interior operator I on the real line, select a sequence Xn ofopen sets such that
X
n∈N
n is not open, e.g., Xn = (−1/n, 1/n), and put U(p, n) = Xn.
However, even this seemingly weak interaction between topological and temporal oper-
ators turns out to be dangerous:
Theorem 3.6. The satisfiability problem for PT L ◦ S4u-formulas in tt-models based onthe flows of time N, < or Z, < is undecidable. It is undecidable as well for tt-modelssatisfying FSA or based on (arbitrary) finite flows of time.
Theorem 2.6 might suggest considering the fragment PT L2 × S4u with 2F and its past
counterpart 2P as the only temporal primitives applicable both to formulas and terms:
τ
::=
p
|
τ
|
τ1
τ2
|
Iτ
|
2F τ | 2P τ,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2 | 2F ϕ | 2P ϕ.
Yet again the result is ‘negative:’
Theorem 3.7. The satisfiability problem for PT L2 × S4u-formulas in tt-models (with orwithout FSA) based on the flows of time N, < or Z, < is undecidable. It is undecidableas well for tt-models based on (arbitrary) finite flows of time.
These undecidability results (the strongest ones, Theorems 3.6 and 3.7, to be more
precise) will be proved in Appendix B.2 by a reduction of Post’s correspondence problemwhich is known to be undecidable (Post, 1946). As we will see from the proofs, thesetheorems actually hold for the ‘future fragments’ of the corresponding languages.
3.3 Decidable Spatio-Temporal Logics with (PC) and (OC)
An important lesson we learn from (the proofs of) the ‘negative’ results of Section 3.2 is thatfull S4u is too expressive for computationally well-behaved combinations with fragments ofPT L. On the other hand, as was said in Section 2.1.2, qualitative spatial representation andreasoning often requires extensions of spatial variables to be regular closed (i.e., regions).This restriction is very important for constructing decidable spatio-temporal logics with(PC) and (OC). First, the undecidability proofs from Appendix B.2 do not go throughin this case. And second, as will be shown below, decidable combinations of PT L andsome of the fragments of S4u introduced in Section 2.1 do exist. In fact, we will constructa hierarchy of decidable spatio-temporal logics of different computational complexity byimposing various restrictions on regions themselves, the ways they can be compared, andthe interactions between spatial and temporal constructors.
We begin by considering the simplest combination of PT L and RCC-8 capturing (PC)
and (OC). This logic called PT L◦RCC-8 (it was introduced under the name ST − by Wolter
1
and Zakharyaschev, 2002) operates with spatio-temporal region terms of the form
::=
CIp
|
CI
.
To relate these terms, we are allowed to use the eight binary predicates of RCC-8; then arbit-rary temporal operators and Boolean connectives can be applied to produce PT L ◦ RCC-8
188

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
formulas. Typical examples of such formulas are (A), (B), (D) and (E) above. Note that(C) can be regarded as a PT L ◦ RCC-8 formula as well (two regions overlap iff they areneither disconnected nor externally connected). On the other hand, (F), (H) and (G) arenot PT L◦RCC-8 formulas because the first two use the
operation on region terms and (G)
uses temporal operators 2F and 3F on region terms.
As before, PT L ◦ RCC-8 formulas are interpreted in topological temporal models (or
tt-models). However, only discrete flows of time do make sense for this language. Althoughthe interaction between topological and temporal operators is similar to that in PT L ◦ S4u(clearly, PT L◦RCC-8 is a fragment of PT L◦S4u), we have the following rather unexpectedand encouraging result:
Theorem 3.8. The satisfiability problem for PT L ◦ RCC-8 formulas in tt-models based on
N, < , Z, < or (arbitrary) finite flows of time is PSPACE-complete.
This theorem will be proved in Appendix C.5. The idea of the proof is similar to that of
Theorem 3.1: we consider the spatial and the temporal parts of a given formula separately.However, to take into account the interaction between these parts, we use the so-called‘completion property’ of RCC-8 (cf. Balbiani & Condotta, 2002) with respect to a certainclass C of models: given a satisfiable set Φ of RCC-8 formulas and a model in C satisfyinga subset of Φ, one can extend this ‘partial’ model to a model in C satisfying the whole Φ.
What happens if we extend the expressive power of the spatial component by allowing
Boolean operators on spatio-temporal region terms, i.e., jump from RCC-8 to BRCC-8?Define spatio-temporal Boolean region terms by taking
::=
CIp
|
CI
|
CI( 1
2)
|
CI
.
Denote by PT L ◦ BRCC-8 the language obtained from PT L ◦ RCC-8 by allowing spatio-temporal Boolean region terms as arguments of the RCC-8 predicates (this language wascalled ST 1 by Wolter and Zakharyaschev, 2002). Formulas (A)–(F) and (H) belong toPT L ◦ BRCC-8, but (G) uses the 2F and 3F operators on regions and so is not in PT L ◦BRCC-8.
Now, another surprise is that the replacement of RCC-8 with BRCC-8 in our temporal
context results in an exponential jump of the computational complexity (remember thatboth RCC-8 and BRCC-8 are NP-complete):
Theorem 3.9. The satisfiability problem for PT L ◦ BRCC-8 formulas in tt-models basedon the flows of time N, < or Z, < is EXPSPACE-complete. It is EXPSPACE-completeas well for models satisfying FSA or based on (arbitrary) finite flows of time.
The EXPSPACE upper bound (see Appendix C.3) is proved by a polynomial embed-
ding of PT L ◦ BRCC-8 into the one-variable fragment QT L1 of first-order temporal logic,which is known to be EXPSPACE-complete (Hodkinson, Kontchakov, Kurucz, Wolter, &Zakharyaschev, 2003). To construct this embedding, we first show that PT L ◦ BRCC-8 iscomplete with respect to Aleksandrov tt-models. In fact, we prove that every satisfiableformula of the more expressive logic PT L ◦ S4u introduced in Section 3.2 can be satisfiedin an Aleksandrov tt-model (see Lemma B.1 and the discussion above). Lemma C.1 thenshows that to satisfy a PT L ◦ BRCC-8 formula, it suffices to take an Aleksandrov tt-model
189

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
based on a partial order of depth 1. By Lemma C.2, the width of the partial order can bebounded by 2 (just as in the case of BRCC-8), and therefore unions of forks (or 2-brooms)are enough to satisfy PT L ◦ BRCC-8 formulas. These Aleksandrov tt-models based onunions of forks can be encoded by means of unary predicates of QT L1.
The EXPSPACE lower bound is proved in Appendix C.1 by encoding the corridor
tiling problem. It can also be established by a direct polynomial embedding of QT L1 intoPT L◦BRCC-8. To illustrate the idea, consider the QT L1-formula ∀x (P (x)∨ P (x)) sayingthat, for every point of the space, either it is in P now or will be there tomorrow. The samestatement can be expressed in PT L ◦ BRCC-8 by the formula EQ(P
P, E) ∧ DC(E, E),
where the last conjunct makes E empty.
Now let us make one more step in space and extend BRCC-8 to RC, thus obtaining the
spatio-temporal language PT L ◦ RC with the following syntax:
::=
CIp
|
CI
|
CI( 1
2)
|
CI
,
τ
::=
|
I
|
τ
|
τ1
τ2,
ϕ
::=
2∀τ | ¬ϕ | ϕ1 ∧ ϕ2 | ϕ1 U ϕ2 | ϕ2 S ϕ2.
The reader should not be surprised now (although the authors were) that the extra ex-pressivity results in one more exponential gap:
Theorem 3.10. The satisfiability problem for PT L ◦ RC-formulas in tt-models based onthe flows of time N, < or Z, < is 2EXPSPACE-complete. It is 2EXPSPACE-completeas well for models satisfying FSA or based on (arbitrary) finite flows of time.
The lower bound is established in Appendix C.1 and the upper bound in Appendix C.2.Perhaps, it is proper time now to have a closer look at the emerging landscape. What
exactly causes these exponential ‘jumps’ ? Can we locate more precise borders in the ladderPSPACE–EXPSPACE–2EXPSPACE?
By analysing the proof of Theorem 3.8 (see Appendix C.5), we note that not so much
can be added to RCC-8. In fact, the maximal spatio-temporal logic (denoted by PT L◦RC2)for which this proof goes through is based on spatio-temporal terms of the form
::=
CIp
|
CI
,
θ
::=
|
I
|
|
I ,
τ
::=
θ1
θ2.
On the other hand, even the addition of predicates of the form EQ(X, Y
Z) is enough
to make the logic EXPSPACE-hard (see Remark C.3). Thus, PT L ◦ RCC-8 (or ratherits extension PT L ◦ RC2) is located pretty close to the border between PSPACE andEXPSPACE spatio-temporal logics.
The following fragment RC− of RC indicates where the border between EXPSPACE
and 2EXPSPACE may lie:
::=
Boolean region terms,
δ
::=
|
σ,
σ
::=
I
|
δ
|
σ1
σ2,
τ
::=
δ1
· · ·
δm
|
δ
σ
|
σ.
190

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Intuitively, the δ and the σ are spatial terms interpreted by regular closed and regular open4sets, respectively (the interior of a region is regular open, the complement of a regular closedset is regular open (and vice versa), regular closed sets are closed under unions and regularopen ones are closed under intersections). Thus, δ can be regarded as a generalisation ofregion terms and σ as a generalisation of the interiors of regions. In other words, RC− isthe fragment of RC in which only the following ways of relating regions are available:
• there is a point where some regions meet;
• a region intersects the interior of another one;
• the interior of a region is not empty.
It is readily checked that BRCC-8 is a fragment of RC−. Moreover, it is a proper fragmentbecause (4) belongs to the latter but not to the former. The formula
2∀ ( NorthKorea
SouthKorea )
DmZone
(8)
(saying that the demilitarised zone between the North Korea and the South Korea consistsof the border between them along with some adjacent territories) shows that RC− is aproper subset of RC:
BRCC-8
RC−
RC.
Although RC− extends BRCC-8, it gives rise to the spatio-temporal logic of the same
computational complexity:
Theorem 3.11. The satisfiability problem for PT L ◦ RC−-formulas in tt-models based onthe flows of time N, < or Z, < is EXPSPACE-complete. It is EXPSPACE-complete aswell for models satisfying FSA or based on (arbitrary) finite flows of time.
The lower bound follows immediately from Theorem 3.9 and the proof of the upper
bound is similar to that of Theorem 3.9 (see Appendix C.3). Again, due to the restrictionon possible ways of relating regions, we can polynomially bound the width n of n-broomsthat are required to satisfy PT L◦RC−-formulas (cf. Lemma C.2). In fact, we need formulassimilar to (8) in order to increase complexity to 2EXPSPACE.
The constructed hierarchy of decidable spatio-temporal logics still leaves at least one
important question: do there exist decidable spatio-temporal logics that allow applicationsof the temporal operators U , 2F , 3F to region terms and what is their complexity? Considerthe languages PT L × L, for L ∈ BRCC-8, RC−, RC, which differ from PT L ◦ L only inthe definition of spatio-temporal region terms:
::=
CIp
|
CI
|
CI( 1
2)
|
CI( 1 U 2)
|
CI( 1 S 2).
The following two theorems provide a positive (though partial) answer to this question:
Theorem 3.12. The satisfiability problem for PT L × BRCC-8 and PT L × RC−-formulasin tt-models based on N, < or Z, < and satisfying FSA, or based on (arbitrary) finiteflows of time is EXPSPACE-complete.
4. Remember that a set X is regular open if ICX = X.
191

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Theorem 3.13. The satisfiability problem for PT L × RC-formulas in tt-models basedon N, < or Z, < and satisfying FSA, or based on (arbitrary) finite flows of time is2EXPSPACE-complete.
The upper bounds mentioned in these two theorems are proved in Appendices C.3 and
C.2, respectively. The lower bounds follow from the results for PT L◦BRCC-8 (Theorem 3.9)and PT L ◦ RC− (Theorem 3.10).
To appreciate the following theorem, the reader should recall that both PT L2 and RC−
are NP-complete:
Theorem 3.14. The satisfiability problem for PT L2×BRCC-8 and PT L2×RC−-formulasin tt-models based on N, < or Z, < and satisfying FSA, or based on (arbitrary) finiteflows of time is EXPSPACE-complete.
Actually it is a consequence of the EXPSPACE-hardness of QT L1 with the sole temporal
operator 2F (see Hodkinson et al., 2003).
Unfortunately, very little is known about the complexity of our spatio-temporal lan-
guages interpreted in tt-models based on dense or arbitrary flows of time. In fact, the onlyresult we know of can be proved using the recent work (Hodkinson, 2004; Hodkinson et al.,2003):
Theorem 3.15. The satisfiability problem for PT L × BRCC-8 and PT L × RC−-formulasin tt-models satisfying FSA and based on Q, < , R, < or arbitrary flows of time belongsto 2EXPTIME and is EXPSPACE-hard.
4. Conclusion
We have provided an in-depth analysis of the computational complexity of various spatio-temporal logics interpreted in Cartesian products of flows of time and topological spaces.Some of these results are collected in Table 1. The design of the languages was driven by theidea to cover the most basic features of spatio-temporal hybrids combining standard logicsof time and mereotopology, with the aim being to see how complex reasoning with thesehybrids could be. We did not try to fine-tune the languages for real-world applications. Onthe contrary, we tried to keep them as ‘pure’ and representative as possible and determinecomputational challenges which any multi-dimensional approach to reasoning about spaceand time would face. With this research objective in mind, we discuss now some conclusionsthat can be drawn from Table 1.
The conclusion to be drawn from the undecidability results is easy: do not try to
implement a sound, complete and terminating algorithm which is supposed to decide thesatisfiability problem for PT L × S4u, PT L ◦ S4u or PT L2 × S4u—you will never succeed.If decision procedures are required, then alternative languages have to be devised.
The interpretation of the complexity results for decidable logics is not so transparent:
it is well-known that such results do not provide us with immediate conclusions regardingthe behaviour of implemented systems. For example, sometimes algorithms running inexponential time in the worst-case perform better on practical problems than worst-caseoptimal algorithms that run in polynomial time. Indeed, the complexity results should beanalysed together with their proofs—if significant conclusions are required (cf. Nebel, 1996).
192

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
flow
spatial component L
guage
of time
lan
RCC-8
BRCC-8
RC
RCmax
S4u
L
n/a
NP
NP
PSPACE
PSPACE
(Thm. 2.2)
(Thm. 2.4)
(Thm. 2.1)
][L N, Z,Q, R,
2L
finite
NP
PSPACE
T
or
P
(Thm. 3.2)
(Thm. 3.1)
arbitrary
] N, Z,Q, R,
[LL
finite
PSPACE
T
or
P
(Thm. 3.1)
arbitrary
PSPACE
L
N, Z
◦
(Thm. 3.8)
EXPSPACE
2EXPSPACE
undecidable
L
finite
?
T
≤ EXPSPACE
(Thm. 3.9)
(Thm. 3.10)
(Thm. 3.6)
P
or
≥ PSPACE
N, Z+FSA
N, Z
?
undecidable
finite
L
≤ EXPSPACE
≤ 2EXPSPACE
(Thm. 3.7)
or
EXPSPACE
?
×
≥ NP
(Thm. 3.14)
≥ EXPSPACE
2 N, Z+FSA
LT
arbitrary
P
or
≤ 2EXPTIME
≤ 2EXPTIME
?
?
?
Q, R
≥ NP
≥ EXPSPACE
with FSA
N, Z
?
undecidable
(Thm. 3.3)
finite
L
≤ EXPSPACE
EXPSPACE
2EXPSPACE
×
or
?
undecidable
≥ PSPACE
L
(Thm. 3.12)
(Thm. 3.13)
(Thm. 3.5)
N, Z+FSA
T
arbitrary
P
≤
or
≤
2EXPTIME
2EXPTIME
≥ EXPSPACE
?
?
?
Q, R
≥ PSPACE
(Thm. 3.15)
with FSA
Table 1: Complexity of the satisfiability problem for spatial and spatio-temporal logics.
193

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Only the proofs show where the sources of the complexity are and whether they could berelevant for practical problems and the implementation of algorithms.
In this respect our proofs are actually rather informative. The decidability proof for
PT L[S4u] immediately provides us with a modular algorithm combining any known pro-cedures for the components. The EXPSPACE-completeness results for PT L × BRCC-8(with FSA) and PT L ◦ BRCC-8 show an extremely close link between the spatio-temporallanguages and the one-variable fragment of first-order temporal logic.
The algorithmic
problems investigated in the context of first-order temporal logic are, therefore, of the samecharacter as those we deal with in the spatio-temporal context. Thus, the experience ofworking with algorithms for (fragments of) first-order temporal logics (Hodkinson, Wolter,& Zakharyaschev, 2000; Degtyarev, Fisher, & Konev, 2003; Kontchakov, Lutz, Wolter, &Zakharyaschev, 2004) about which we have a pretty good knowledge by now almost directlytranslates to insights into possible algorithms for spatio-temporal logics. The PSPACE-completeness result for PT L ◦ RCC-8 is obtained by means of a reduction (modulo RCC-8reasoning) to PT L. So we can conclude from the proof that it will be sufficient to havegood solvers for RCC-8 and PT L to obtain a reasonable prover for PT L ◦ RCC-8. Theinteraction between the two components turned out to be rather weak.
In conclusion, the complexity proofs clearly show the algorithmic problems to be solved
when dealing with the spatio-temporal logics presented in this paper. In particular, devisingalgorithms for these logics should be conceived as part of the more general enterprise ofdeveloping algorithms for propositional and the one-variable fragment of first-order temporallogic.
Here are some comments on and explanations of the most important results in Table 1:
1. The undecidability result for PT L × S4u, PT L ◦ S4u and PT L2 × S4u solves a major
open problem of Wolter and Zakharyaschev (2002). It shows that, while S4u is asuitable candidate for efficient pure spatial reasoning (Bennett, 1996; Renz & Nebel,1998; Aiello & van Benthem, 2002a), its temporal extensions satisfying both (PC)and (OC) are not suitable for practical spatio-temporal representation and reasoning.
2. Logics like PT L × BRCC-8 may turn out to be undecidable when interpreted in
arbitrary topological temporal models. One of the main origins of their expressivepower is a possibility to form infinite intersections and unions of regions. However, wecan ‘tame’ the computational behaviour of these logics by imposing natural restrictionson the classes of admissible models such as FSA.
3. The PSPACE upper bound for PT L ◦ RCC-8 and the EXPSPACE lower bound for
PT L ◦ BRCC-8 solve two other major open problems of Wolter and Zakharyaschev(2002).
It is of interest to note that the spatial fragments of PT L ◦ RCC-8 and
PT L ◦ BRCC-8 have the same computational complexity: both are NP-completeover arbitrary topological spaces. Thus the additional Boolean connectives on spatialregions interacting with the next-time operator
can make the logic substantially
more complex.
4. The 2EXPSPACE-completeness result for PT L × RC with FSA and PT L ◦ RC is an-
other example when a seemingly tiny increase of expressiveness results in a significantjump of complexity.
194

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
5. PSPACE-completeness of PT L ◦ RCC-8 is a particularly ‘good news,’ since it shows
that this combination of PT L and RCC-8 has the same computational complexityas PT L itself, for which surprisingly fast systems have been implemented (Schwendi-mann, 1998; Hustadt & Konev, 2003). This gives us hope that ‘practical’ algorithmsfor PT L◦RCC-8 can be implemented. Indeed, the proof shows that it may be possibleto encode the satisfiability problem for PT L◦RCC-8 into the satisfiability problem forPT L and then use PT L provers. We note that this complexity result has been con-jectured by Demri and D’Souza (2002) and that our proof uses some ideas of Balbianiand Condotta (2002).
6. On the other hand, the EXPSPACE lower bounds for PT L × BRCC-8 with FSA and
PT L◦BRCC-8 do not necessarily mean that reasoning with these logics is hopeless. Infact, we show that both of them can be regarded as fragments of the one-variable first-order temporal logic, for which tableau- and resolution-based decision procedures havebeen developed and implemented (Degtyarev et al., 2003; Kontchakov et al., 2004).
Of course, there are many directions of further research in spatio-temporal knowledge rep-resentation and reasoning. Here we mention only some of them that are closely related tothe logics we have considered above.
• In this paper, we confined ourselves to considering linear flows of time. It may be
of interest, however, to investigate the computational properties of spatio-temporallogics based on the branching time paradigm (see, e.g., Clarke & Emerson, 1981;Emerson & Halpern, 1985) in order to model uncertainty about the future. Recentresults by Hodkinson, Wolter and Zakharyaschev (2001, 2002) give hope that suchlogics can be decidable.
• We confined ourselves to considering only mereotopological formalisms for the spatial
dimension. It would be also of interest to consider spatial logics of directions (Ligozat,1998), shape (Galton & Meathrel, 1999), size (Zimmermann, 1995), position (Clem-entini, Di Felice, & Hern´
andez, 1997), or even their hybrids (Gerevini & Renz, 2002).
We note that some results in this direction have been recently obtained by Balbianiand Condotta (2002) and Demri and D’Souza (2002).
• Another interesting and important perspective in both spatial and spatio-temporal
representation and reasoning is to move from arbitrary topological spaces to thoseinduced by metric spaces and introduce explicit and/or implicit numerical parameters.First encouraging steps in this direction have been made in the work (Kutz, Sturm,Suzuki, Wolter, & Zakharyaschev, 2003).
We conclude the paper with a number of open problems:
1. What is the precise computational complexity of PT L × BRCC-8 with FSA over
dense flows of time and arbitrary strict linear orders?
2. Are logics of the form PT L × L and PT L2 × L, for L ∈ RC, BRCC-8, RCC-8,
decidable without FSA?
195

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
3. Are combinations of PT L and PT L2 with RCmax (satisfying both (PC) and (OC))
decidable?
4. Is PT L × S4u undecidable over dense flows of time and arbitrary strict linear orders?
5. Is PT L × RCC-8 with FSA decidable in PSPACE?
Acknowledgments
The work on this paper was partially supported by U.K. EPSRC grants no. GR/R45369/01,GR/R42474/01, GR/S61966/01 and GR/S63182/01. The work of the third author was alsopartially supported by Hungarian Foundation for Scientific Research grants T30314 and035192.
Special thanks are due to the referees of the first version of this paper whose remarks,
criticism and constructive suggestions have led to many days of intensive and excitingresearch, new results and, hopefully, a better paper.
Appendix A. Complexity of Spatial Logics
In this appendix we prove Theorems 2.2 and 2.4. In these proofs we use the fact that S4u(as well as its fragments) is complete with respect to (finite) Aleksandrov topological spaces(McKinsey & Tarski, 1944; Goranko & Passy, 1992). Recall from p. 174 that an Aleksandrov(topological ) model is a pair of the form M = G, V , where G = V, R is a quasi-orderand V is a map from the set of spatial variables into 2V . It will be more convenient for usto unify notation for spatial formulas and spatial terms and write (M, x) |= τ instead ofx ∈ V(τ ), for τ a spatial term and x a point in V . In particular, by the definition of theinterior and closure operators in Aleksandrov spaces,
(M, x) |= Iτ
iff
∀y ∈ V xRy → (M, y) |= τ ,
(M, x) |= Cτ
iff
∃y ∈ V xRy ∧ (M, y) |= τ .
By the length (ϕ) of a formula ϕ we understand the number of subformulas and sub-
terms occurring in ϕ.
Proof of Theorem 2.2. The proof follows from Lemmas A.1 and A.2 below which showtogether that every satisfiable RC-formula can be satisfied in an Aleksandrov model of sizepolynomial (in fact, quadratical) in the length of the input formula (in other words, RC hasthe polynomial finite model property). Thus, we have a nondeterministic polynomial timealgorithm for the satisfiability problem.
K
In fact, Lemma A.1 shows that RC is complete with respect to a subclass of Aleksandrov
spaces, namely, finite disjoint unions of finite brooms. Recall from p. 179 that a broom isa partial order b of the form r ∪ V0, R , where R is the reflexive closure of r × V0(see Fig. 4). We call r the root of b and points in V0 the leaves of b; they are also referredto as points of depth 1 and 0, respectively. A broom b is said to be a κ-broom, κ ≤ ω, if|V0| ≤ κ. In particular, we call a broom finite if it is an n-broom, for some n < ω.
196

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Lemma A.1. Every satisfiable RC-formula is satisfied in an Aleksandrov model based ona finite disjoint union of finite brooms.
Proof. As is well-known, if an RC-formula ϕ is satisfiable then it can be satisfied in a finiteAleksandrov model M = G, V , G = V, R . Define a new relation R on V by taking Rto be the reflexive closure of R ∩ (V1 × V0), where
V0 = x ∈ V | ¬∃y (xRy ∧ ¬ yRx)
and
V1 = V − V0.
(Without loss of generality we may assume that V1 = ∅ and no y ∈ V0 has more than oneproper R-predecessor.) Let G = V, R
and M = G , V . Clearly, G is a partial order as
required. We prove that, for every RC-formula ψ,
M |= ψ
iff
M |= ψ.
(9)
First we show that, for every Boolean region term
and every x ∈ V ,
(M , x) |=
iff
(M, x) |= .
(10)
By definition, (M , x) |= p iff (M, x) |= p, for every spatial variable p. It is readily seen thatfor every y ∈ V0 and every spatial term τ , we have (M , y) |= τ iff (M, y) |= τ . Now, if
is
a Boolean region term then
= CIτ for some spatial term τ , and we clearly have:
(M, x) |= CIτ
iff
∃y ∈ V
xRy and ∀z ∈ V (yRz → (M, z) |= τ )
iff
∃y ∈ V0 xR y and (M, y) |= τ
iff
∃y ∈ V0 xR y and (M , y) |= τ
iff
∃y ∈ V0 xR y and (M , y) |= Iτ
iff
(M , x) |= CIτ.
Next, we extend (10) to spatial terms of the form I where
is a Boolean region term. If
(M, x) |= I
then (M, y) |=
whenever xRy, and so, by R ⊆ R, we have (M , x) |= I .
Conversely, suppose (M , x) |= I . Take any y with xRy and any z ∈ V0 with yRz. Weclaim that (M, z) |=
. Indeed, if x ∈ V1 then this follows by IH from xR z. If x ∈ V0
then zRx. Since (M , x) |= , by IH and
= CIτ , we obtain (M, z) |= . Now (M, y) |=
follows by yRz and
= CIτ . Thus, (M, x) |= I .
Finally, we can easily extend (10) to arbitrary spatial terms and formulas of RC because
both are constructed from spatial terms of the form
and I , with
a Boolean region term,
using operators that do not depend on the structure of the underlying partial order. Thuswe have (9).
K
Lemma A.2. Every satisfiable RC-formula ϕ is satisfied in an Aleksandrov model basedon a disjoint union of at most (ϕ) many 2 (ϕ)-brooms.
Proof. Remember that every RC-formula ϕ is (equivalent to) a Boolean combination ofspatial formulas from some set Σϕ = 3
∃ τ1, . . . , 3
∃ τm.5 For each 3
∃ τ ∈ Σϕ, the spatial term
5. In the following proof we consider 3
∃ as primary and 2
∀ τ as an abbreviation for ¬3
∃ τ .
197

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
τ is also a Boolean (or rather set-theoretic) combination of some
1, . . . ,
k , I
, . . . , I
1
m,
where the i and the
are Boolean region terms.
i
It follows from Lemma A.1 that ϕ is satisfied in an Aleksandrov model M = G, V ,
where G = V, R is a finite disjoint union of finite brooms. For every 3
∃ τ ∈ Σϕ with
M |= 3
∃ τ , fix a point xτ ∈ V such that (M, xτ ) |= τ . We may assume that the xτ are
pairwise distinct and that the roots of all brooms are the points of the form xτ for 3
∃ τ ∈ Σϕ.
Therefore, G is a disjoint union of ≤ (ϕ) many finite brooms bτ , for 3
∃ τ ∈ Σϕ.
Let us construct a new model M as follows. For each broom bτ , 3
∃ τ ∈ Σϕ, and each
∈ Ξτ , we pick
• a leaf yτ, of bτ (if any) such that (M, yτ, ) |= ,
• a leaf yτ, of bτ (if any) such that (M, yτ, ) |=
and remove the other leaves of bτ . Denote by bτ the resulting broom. Clearly, it is a 2 (ϕ)-broom. Let G = V , R
be the disjoint union of all bτ , for 3
∃ τ ∈ Σϕ, and M = G , V .
It is easy to see that G is as required.
Now, to show that ϕ is satisfied in M , it suffices to prove that, for all 3
∃ τ ∈ Σϕ,
M |= 3
∃ τ
iff
M |= 3
∃ τ.
(11)
By definition of M , for all leaves y of G and all spatial terms τ ,
(M , y) |= τ
iff
(M, y) |= τ.
Next, for every root xτ of bτ , every 3
∃ τ ∈ Σϕ and every
∈ Ξτ , we have (M, xτ ) |=
iff
there is a leaf y such that xτ Ry and (M, y) |=
(simply because
= CIδ, for some δ). It
follows from the construction of M that (M, xτ ) |=
iff (M , xτ ) |= , for every
∈ Ξτ .
It also follows that (M, xτ ) |= I implies (M , xτ ) |= I . Conversely, if (M , xτ ) |= I , but(M, xτ ) |= I then there is a leaf y such that xτ Ry and (M, y) |=
which is a contradiction.
Since intersection and complement do not depend on the structure of the underlying frame,we have (M , xτ ) |= τ iff (M, xτ ) |= τ , for every root xτ of bτ , which proves (11).
K
Proof of Theorem 2.4. The PSPACE upper bound follows from Theorem 2.1. The proofof PSPACE-hardness is by reduction of the validity problem for quantified Boolean formulaswhich is known to be PSPACE-complete (Stockmeyer, 1987). We will slightly modify theproof of Ladner (1977) (that shows the PSPACE-hardness of S4), in order to take intoaccount that the variables in RCmax-formulas are always prefixed by CI.
We may assume that quantified Boolean formulas are of the form
ϕ = Q1p1 . . . Qnpn ϕ ,
where Qi ∈ ∀, ∃ and ϕ is a Boolean formula with variables p1, . . . , pn. As is well known,all possible truth assignments to p1, . . . , pn can be arranged as the leaves of a full binarytree of depth n. The left subtree of the root contains all truth assignments with p1 trueand the right subtree those with p1 false; then we branch on p2, then p3, and so on. Wecan determine whether ϕ is valid by pruning this full binary tree: whenever Qi is ∀, thenwe keep both subtrees at the ith level, and whenever Qi is ∃ then only one of them. If this
198

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
ϕ
ϕ
ϕ
ϕ
q3,rp1,p2,p3
q3,rp1,p2
q3,rp2,p3
q3,rp2
λd
s
3
 
λ3
λd
s
3
 
λ3
d
 
d
 
d
2
r  
d
 
q2, p1, p2
q2, p2
λd 
λ2 r
d
E
 
r
E r
T
T
λ
λ
1
r
q1, p1
1 r
q
E r
E r
1
r
‰
¨
B
r
¨
r
¨
r
¨
r
¨
rr r
¨
¨
r
E
¨
rq0
λ0
Figure 6: An Aleksandrov model that may satisfy ϕ∗, for ϕ = ∀p1∃p2∀p3 ϕ .
way we can end up with a tree such that all its leaves evaluate ϕ to true, then ϕ is valid,otherwise not.
We will ‘generate’ the leaves of this binary tree in Aleksandrov models with the help of
an RCmax-formula. More precisely, we will construct an RCmax-formula ϕ∗ such that
• its length is polynomial in the length of ϕ, and
• ϕ∗ is satisfied in an Aleksandrov model iff ϕ is valid.
Take fresh spatial variables q0, . . . , qn, and put, for i = 0, . . . , n,

q0
q1
if
i = 0;



λi =
qi−1
qi
qi+1 ,
if
0 < i < n;



qn−1
qn ,
if
i = n.
Now consider the variables p1 . . . , pn of ϕ as spatial variables, and let ϕ be the result ofreplacing every occurrence of pi with pi in ϕ . Put
ϕ∗ = 3
∃ λ0 ∧
2∀ λi−1
(τ −
τ +)
∧
2∀ λ
τ +)
∧ 2∀ λ
i
i
i−1
(τ −
i
i
n
ϕ
,
Qi=∃
Qi=∀
where, for i = 1, . . . , n,
τ − = C λ
= C λ
i
i
pi
and
τ +
i
i
I pi .
Clearly, ϕ∗ is an RCmax-formula and its length is polynomial in the length of ϕ.
Suppose first that ϕ is valid. Then Fig. 6 shows the structure of a possible Aleksandrov
model satisfying ϕ∗.
The converse direction is similar to that of Ladner’s proof (1977). Suppose that ϕ∗ is
satisfied in an Aleksandrov model M. Then, for each ‘necessary’ sequence of truth values for
p1 , . . . , pn , there is a point in M ‘reflecting’ this sequence (we do not use the ‘structure’
of the spatial terms λi here). Since, by the last conjunct of ϕ∗, ϕ holds in M at all thesepoints, we obtain that the quantified Boolean formula ϕ must be valid.
K
199

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Appendix B. Spatio-Temporal Logics Based on S4u
In this appendix we prove Theorems 3.1, 3.2, 3.6 and 3.7 as well as Proposition 3.4. ThenTheorems 3.3 and 3.5 are immediate corollaries of Theorem 3.6. But first, some generalresults are established to be used later on.
We remind the reader that by an Aleksandrov tt-model we mean a tt-model based on an
Aleksandrov (topological) space. Every such model can be regarded as a triple of the formK = F, G, V , where F = W, < is a flow of time, G = V, R a quasi-order, and V is a mapassociating with every spatial variable p and every time point w ∈ W a set V(p, w) ⊆ V .As in Appendix A, instead of x ∈ V(τ, w) we write (K, w, x ) |= τ to unify notation forspatio-temporal formulas and terms.
Given a spatio-temporal formula ϕ, we denote by sub ϕ the set of all its subformulas
and by term ϕ the set of all spatio-temporal terms occurring in ϕ.
Lemma B.1. (i) If a PT L × S4u-formula ϕ is satisfied in a tt-model with FSA and basedon a flow of time F, then ϕ is satisfied in an Aleksandrov tt-model with FSA and basedon F.
(ii) If a PT L ◦ S4u-formula ϕ is satisfied in a tt-model based on a flow of time F, then
ϕ is satisfied in an Aleksandrov tt-model based on F as well.
Moreover, in both cases we can choose an Aleksandrov tt-model K = F, G, V satisfying
ϕ (with F =
W, < and G =
V, R ) in such a way that for all w ∈ W , x ∈ V and
spatio-temporal terms τ , the set
Aw,x,τ = y ∈ V | xRy and (K, w, y ) |= τ 
contains an R-maximal point 6 (provided of course that Aw,x,τ = ∅).
Proof. The proof uses the Stone–J´
onsson–Tarski representation of topological Boolean
algebras (in particular, topological spaces) in the form of general frames (see, e.g., Goldblatt,1976 or Chagrov & Zakharyaschev, 1997).
(i) Suppose that ϕ is satisfied in a tt-model M = F, T, U with FSA and based on a
topological space T = U, I . Denote by V the set of all ultrafilters over U . For any twoultrafilters x1, x2 ∈ V , put x1Rx2 iff ∀A ⊆ U (IA ∈ x1 → A ∈ x2). It is easy to see that Ris a quasi-order on V . Define an Aleksandrov tt-model K = F, G, V by taking G = V, Rand V(p, w) = x ∈ V | U(p, w) ∈ x. We show by induction on the construction of aspatio-temporal term τ that, for all w ∈ W and x ∈ V ,
(K, w, x ) |= τ
iff
U(τ, w) ∈ x.
(12)
The basis of induction and the case of the Booleans are trivial. The case of τ = Iτ isstandard (consult Goldblatt, 1976 or Chagrov & Zakharyaschev, 1997).
Case τ = τ1 U τ2. Assume that (K, w, x ) |= τ1 U τ2. Then there is v > w such that
(K, v, x ) |= τ2 and (K, u, x ) |= τ1 for all u in the interval (w, v). By IH, U(τ2, v) ∈ x andU(τ1, u) ∈ x for all u ∈ (w, v). Since
U(τ1 U τ2, w) ⊇ U(τ2, v) ∩
U(τ1, u),
u∈(w,v)
6. A point z is said to be R-maximal in A ⊆ V if, for every z ∈ A, we have z Rz whenever zRz .
200

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
we shall have U(τ1 U τ2, w) ∈ x if we show that
U(τ2, v) ∩
U(τ1, u) ∈ x.
(13)
u∈(w,v)
In view of FSA, we can find time points u1, . . . , ul ∈ (w, v) such that
U(τ1, u1) ∩ · · · ∩ U(τ1, ul) =
U(τ1, u),
u∈(w,v)
which yields (13) because ultrafilters are closed under finite intersections.
Conversely, let U(τ1 U τ2, w) ∈ x. By FSA, there are time points v1, . . . vl such that
U(τ1 U τ2, w) =
U(τ2, vi) ∩
U(τ1, u) .
1≤i≤l
u∈(w,vi)
And since x is an ultrafilter,
U(τ2, vi) ∩
U(τ1, u) ∈ x,
u∈(w,vi)
for some i, 1 ≤ i ≤ l. Therefore, by IH, (K, vi, x ) |= τ2 and (K, u, x ) |= τ1 for allu ∈ (w, vi). Hence (K, w, x ) |= τ1 U τ2.
Case τ = τ1 S τ2 is considered analogously.Now, we show that, for all w ∈ W and spatio-temporal terms τ ,
(K, w) |= 2
∀ τ
iff
U(τ, w) = U.
Suppose that (K, w) |= 2
∀ τ . Then (K, w, y ) |= τ for all y ∈ V , and so, by IH, U(τ, w) ∈ y
for all y ∈ V . But then U(τ, w) = U . Conversely, if U(τ, w) = U then U(τ, w) ∈ y for ally ∈ V , from which, by IH, (K, w) |= 2
∀ τ .
It follows immediately that ϕ is satisfied in K. It should be also clear that K satisfies
FSA. This proves (i). The existence of R-maximal points in sets of the form Aw,x,τ (wherew ∈ W , x ∈ V and τ is a spatio-temporal term) follows from a result of Fine (1974); seealso (Chagrov & Zakharyaschev, 1997, Theorem 10.36).
(ii) The construction is the same as in (i). First we show by induction that, for every
spatio-temporal term τ of PT L ◦ S4u, (K, w, x ) |= τ iff U(τ, w) ∈ x. This time, however,instead of U and S we need the inductive step for
.
Case τ =
τ . We have (K, w, x ) |=
τ iff there exists an immediate successor w of
w such that (K, w , x ) |= τ iff, by IH, there is an immediate successor w of w such thatU(τ , w ) ∈ x. It remains to recall that U( τ , w) = U(τ , w ) whenever w is the immediatesuccessor of w and U( τ , w) = ∅ whenever w has no immediate successor.
The remaining part of the proof is the same as in (i).
K
Proof of Proposition 3.4. The implication (⇐) follows immediately from the definition.
(⇒) Suppose that a PT L×S4u-formula ϕ is satisfied in a tt-model with FSA and a flow
of time F = W, < . Then, by Lemma B.1 (i), ϕ is satisfiable in an Aleksandrov tt-modelM = F, G, V with FSA and based on a quasi-order G = V, R . In view of FSA, for
201

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
every τ ∈ term ϕ, there are finitely many sets A1, . . . , Ak ⊆ V such that V(τ, w) | w ∈W  = A1, . . . , Ak. Therefore, there are finitely many time points w1, . . . , wm ∈ W suchthat, for every w ∈ W , there is wi, 1 ≤ i ≤ m, with V(τ, w) = V(τ, wi) for all τ ∈ term ϕ.Now we use the Lemmon filtration (see, e.g., Chagrov & Zakharyaschev, 1997) to constructa tt-model based on a finite Aleksandrov topological space. First, define an equivalencerelation ∼ on V by taking x ∼ y if
(M, wi, x ) |= τ
iff
(M, wi, y ) |= τ,
for all i, 1 ≤ i ≤ m, and τ ∈ term ϕ.
Denote by [x] the equivalence class of x ∈ V . The set V /∼ of pairwise distinct equivalenceclasses is clearly finite. Define a binary relation S on V /∼ by taking [x]S[y] if
(M, wi, y ) |= Iτ
whenever
(M, wi, x ) |= Iτ,
for all i, 1 ≤ i ≤ m, and τ ∈ term ϕ.
Clearly, S is well-defined, reflexive and transitive, and so G = V /∼, S is a finite quasi-order. Let V (p, w) = [x] | x ∈ V(p, w), for every spatial variable p and every w ∈ W .
Consider the tt-model M = F, G , V . First we show that for all τ ∈ term ϕ, x ∈ V
and w ∈ W ,
(M, w, x ) |= τ
iff
(M , w, [x] ) |= τ.
The basis of induction follows from the definition of V , the cases of intersection and com-plement are trivial, and those of temporal operators follow by IH.
Suppose that (M, w, x ) |= Iτ and [x]S[y]. Then there is a moment wi such that
(M, w, z ) |= τ iff (M, wi, z ) |= τ , for all τ ∈ term ϕ and z ∈ V . By the definition of S,we have (M, wi, y ) |= τ , and so (M, w, y ) |= τ . Finally, by IH, (M , w, [y] ) |= τ , andsince y was arbitrary, we obtain (M , w, [x] ) |= Iτ .
Conversely, let (M , w, [x] ) |= Iτ and xRy. Then [x]S[y], and so (M , w, [y] ) |= τ ,
from which, by IH, (M, w, y ) |= τ . Thus, (M, w, x ) |= Iτ .
Finally, by a straightforward induction on the structure of ϕ, one can show that
(M, w) |= ψ
iff
(M , w) |= ψ,
for all ψ ∈ sub ϕ and w ∈ W . It follows that ϕ is satisfied in M .
K
B.1 Temporalisations of S4u
Lemma B.2. Let Γ be a finite set of S4u-formulas. Then there is a finite quasi-order Gsuch that every satisfiable subset Φ ⊆ Γ is satisfied in some Aleksandrov model based on G.
Proof. For every satisfiable Φ ⊆ Γ, fix a model based on a finite quasi-order GΦ = VΦ, RΦand satisfying Φ. Let n = max|VΦ| : Φ ⊆ Γ, Φ is satisfiable and let G be the disjointunion of n full n-ary (transitive) trees of depth n whose nodes are clusters of cardinalityn. It is not difficult to see that every GΦ is a p-morphic image of G. Therefore, everysatisfiable Φ ⊆ Γ is satisfied in an Aleksandrov model based on G.
K
Proof of Theorem 3.1. PSPACE-hardness follows from Theorem 2.1 or 2.5. We showthe matching upper bound.
Let ϕ be a PT L[S4u]-formula. Since ϕ is a PT L ◦ S4u-formula, by Lemma B.1 (ii), it
is satisfiable in a tt-model iff it is satisfiable in an Aleksandrov tt-model based on the same
202

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
flow of time. With every (spatial) subformula 2
∀ τ of ϕ we associate a fresh propositional
variable pτ and denote by ϕ∗ the PT L-formula that results from ϕ by replacing all itssubformulas of the form 2
∀ τ with pτ . We claim that ϕ is satisfiable in an Aleksandrov
tt-model over a flow of time F = W, < iff
• there exists a temporal model N = F, U satisfying ϕ∗ and,
• for every w ∈ W , the set Φw = 2∀τ | (N, w) |= p  ∪ ¬2∀

 
τ
τ | (N, w) |= ¬pτ of spatial
formulas is satisfiable.
The implication (⇒) is obvious. Conversely, suppose that we have a temporal model Nsatisfying the conditions above. Let Γ =
Φ
w∈W
w .
By Lemma B.2, there is a finite
quasi-order G such that, for every w ∈ W , we have G, Vw |= Φw for some valuationVw. It should be clear that ϕ is satisfied in the Aleksandrov tt-model F, G, V , whereV(p, w) = Vw(p), for every spatial variable p and every w ∈ W .
Now, to devise a decision procedure for PT L[S4u] which uses polynomial space in the
length of the input formula, one can take the corresponding nondeterministic PSPACEalgorithm for PT L (Sistla & Clarke, 1985; Reynolds, 2004, 2003) and modify it as follows.The algorithm constructs a ‘pure’ temporal model N = F, U for ϕ∗ and every time itproduces a state for a time instant w ∈ W , it additionally checks whether the set Φw ofspatial formulas is satisfiable. By Theorem 2.1, this extra test can also be performed by aPSPACE algorithm, which does not increase the complexity of the ‘combined’ algorithm.
K
Proof of Theorem 3.2. The proof is essentially the same as that of Theorem 3.1, but nownondeterministic polynomial-time algorithms for the component logics are available.
K
B.2 Undecidability of PT L ◦ S4u and PT L2 × S4u
Note that although our spatio-temporal languages contain no propositional variables, westill can simulate them: for a spatial variable p, formula 2
∀ p can be regarded as a proposition.
Thus, in what follows by a propositional variable p we mean the formula 2
∀ p, for a spatial
variable p (note the different typefaces used to denote propositional and spatial variables).
Proof of Theorem 3.6. The proof is by reduction of the undecidable Post’s (1946) cor-respondence problem or PCP, for short. It is formulated as follows. Given a finite alphabetA and a finite set P of pairs v1, u1 , . . . , vk, uk of nonempty finite words
vi = bi1, . . . , bil ,
ui = ci
(i = 1, . . . , k)
i
1, . . . , ciri
over A, an instance of PCP, decide whether there exist an N ≥ 1 and a sequence i1, . . . , iNof indices such that
vi ∗ · · · ∗ v
= u ∗ · · · ∗ u
,
(14)
1
iN
i1
iN
where ∗ is the concatenation operation. We will construct (using only future-time temporaloperators) a PT L ◦ S4u-formula ϕA,P such that
(i) the length of ϕA,P is a polynomial function in the size of both A and P ;
(ii) if ϕA,P is satisfiable in a tt-model based on N, < then there exist an N ≥ 1 and a
sequence i1, . . . , iN of indices such that (14) holds;
203

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
(iii) if there exist an N ≥ 1 and a sequence i1, . . . , iN of indices such that (14) holds then
ϕA,P is satisfiable in a tt-model with FSA and based on N, < ;
(iv) ϕA,P is satisfiable in a tt-model based on N, < iff ϕA,P is satisfiable in a tt-model
based on a finite flow of time.
The case of Z, < follows immediately. By Lemma B.1 (ii), it suffices to consider onlyAleksandrov tt-models for ϕA,P .
We build ϕA,P using spatial variables lefta and righta (a ∈ A), left, right and stripe, as
well as propositional variables pairi, for every pair vi, ui , 1 ≤ i ≤ k, and range.
The variable range is required to ‘relativise’ temporal operators 2F and 3F in order to
ensure that we can construct a model based on a finite flow of time. The variable stripe isused to introduce a new ‘strict closure’ operator in Aleksandrov spaces by taking, for everyspatio-temporal term τ ,
Sτ = stripe
C(stripe
Cτ )
stripe
C(stripe
Cτ ) .
Denote by Sn a sequence of n operators S. Other abbreviations we need are τ1 ≡ τ2 whichstands for (τ1
τ2)
(τ2
τ1) and 2+ϕ which replaces ϕ ∧ 2
F
F ϕ.
The formula ϕA,P is defined as the conjunction
ϕA,P = ϕrange ∧ ϕstripe ∧ ϕpair ∧ ϕeq ∧ ϕleft ∧ ϕright,
where
ϕrange = range ∧ 3F ¬range ∧ 2F (¬range → 2F ¬range),
ϕpair = 2+ 3
pair ∧
¬(pair ∧ pair
F
F range →
i
i
j ) ,
1≤i≤k
1≤i<j≤k
ϕstripe = 2+ 3
F
F range → 2
∀ (stripe ≡
stripe) ,
ϕeq = 3F range ∧
2∀(lefta ≡ righta) ,
a∈A
ϕleft is the conjunction of (15)–(21), for all i with 1 ≤ i ≤ k,
2+¬3∃ left
2∀ left ≡
left
F
a
leftb
∧ 2+
F
a ,
(15)
a=b
a∈A
a,b∈A
2+ pair → 2∀(left
F
i
a
lefta) ,
(16)
a∈A
2∀left ∧ 2+2∀(left
Sleft),
(17)
F
2+ pair → 2∀(left
Sli left) ,
(18)
F
i
2+ pair →
2∀((Sjleft Sj+1left)
left
) ,
(19)
F
i
bili−j
j<li
pair →
3∃
i
τ left,
(20)
i
2F pair → 2∀
i
((left
Sleft)
Sτ left) ,
(21)
i
204

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
˜
˜
˜
˜
˜
˜ = left
r = left
y
˜
˜
˜
˜
˜rt
n
bi4
4
li
t
.
= left
Sleft
.
.
.
. 
.
4
.
.
.
.
.
.
.
v
.
.
.
.
l
i4
.
i4
y
˜
˜
˜
˜
˜r
n
bi4
3+1
1
y
˜
˜
˜
˜rt
˜r
n
bi3
3
li
.
.
.
. 
.
3
.
.
.
.
.
.
v
.
.
.
l
i3
.
i3
y
˜
˜
˜
˜r
˜r
n
bi3
2+1
1
y
˜
˜
˜rt
˜r
˜r
n
bi2
2
li
.
.
. 
.
2
.
.
.
.
.
v
.
.
l
i2
.
i2
y
˜
˜
˜r
˜r
˜r
n
bi2
1+1
1
y
˜
˜rt
˜r
˜r
˜r
n
bi1
1
li
.
. 
.
1
.
.
.
.
v
.
l
i1
.
i1
y
˜
˜r
˜r
˜r
˜r
1
bi1
1
pairi
pair
pair
pair
1
i2
i3
i4
0
1
2
3
4
. . .
range
Figure 7: Model satisfying ϕleft, for N = 4.
where
τ left = left
S left
S(left
· · ·
Sleft
) . . .
i
bi
bi
bi
bi
1
2
3
li
(remember that li is the length of the word vi). The conjunct ϕright is defined by replacingin ϕleft all occurrences of left with right, lefta with righta (for a ∈ A), li with ri and τ left
i
with τ right, which is defined similarly. (Note that pair
i
i occurs in both ϕleft and ϕright.)
Let us prove that ϕA,P is as required. Suppose that (M, 0) |= ϕA,P , for an Aleksandrov
tt-model M =
N, < , G, V
with G = V, R . Since (M, 0) |= ϕeq, we can find an N ,
1 ≤ N < ω, such that
(M, N ) |= range ∧
2∀(lefta ≡ righta).
(22)
a∈A
In view of ϕrange, we have (M, j) |= range for all j, 0 ≤ j ≤ N . Let i1, . . . , iN be thesequence of indices such that, for 1 ≤ j ≤ N , we have (M, j − 1) |= pairi (ϕpair ensures
j
that there is a unique sequence of this sort). We claim that (14) holds for this sequence.
Since ϕstripe holds in M at 0, we have, for every y ∈ V , (M, 0, y ) |= stripe iff
(M, j, y ) |= stripe for all j, 0 ≤ j ≤ N . Denote by Rs the transitive binary relationon V defined by taking xRsy if there is z ∈ V such that xRzRy and (M, 0, x ) |= stripeholds iff (M, 0, z ) |= stripe. Then we clearly have that, for every j, 0 ≤ j ≤ N , and everyx ∈ V ,
(M, j, x ) |= Sτ
iff
there is y ∈ V such that xRsy and (M, j, y ) |= τ.
Call a sequence y1, . . . , yl of (not necessarily distinct) points from V an Rs-path in
V(left, j) of length l if y1, . . . , yl ∈ V(left, j) and y1Rsy2Rs . . . Rsyl. For every sequence
205

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
z1, . . . , zl of points from V(left, j) we define
leftwordj(z1, . . . , zl) = a1, . . . , al ,
where the ai are the (uniquely determined by (15)) symbols from A with (M, j, zi ) |= lefta .
i
We will show now that, for every j, 1 ≤ j ≤ N , the following holds:
(a) there exists an Rs-path y1, . . . , yn
in V(left, j) of length n
+ · · · + l
such
j
j = li1
ij
that
leftword
∗
j (y1, . . . , yn ) = v
. . .∗ v ;
j
i1
ij
(b) every Rs-path in V(left, j) is of length ≤ nj;
(c) for every Rs-path y1, . . . , yn
in V(left, j), we have
j
leftword
∗
j (y1, . . . , yn ) = v
. . .∗ v .
j
i1
ij
Indeed, for j = 1, we have (a) by (M, 0) |= pairi and (20), (b) by (17) and (18), and
1
(c) by (19).
Now assume inductively that (a)–(c) hold for some j, 1 ≤ j < N .
Let
y1, . . . , yn
be a maximal R
∈ V(left, j + 1).
j
s-path in V(left, j). First, by (16), y1, . . . , ynj
Second, since (M, j, yn ) |= left
Sleft and (M, j) |= pair
, (21) now implies that
j
ij+1
there exist yn
such that y
is an R
j +1, . . . , ynj +li
1, . . . , yn
s-path in V(left, j + 1),
j+1
j +lij+1
as required in (a). For (b) and (c), observe first that for every Rs-path y1, . . . , yl inV(left, j + 1),
y1, . . . , yl−l
is an R
i
s-path in V(left, j), by (18).
So l ≤ nj+1 must
j+1
hold. If l = nj+1 then leftword
∗
j (y1, . . . , yl−l
) = v
. . . ∗ v
by the induction hypo-
i
i
i
j+1
1
j
thesis, and so leftword
∗
j+1(y1, . . . , yl−l
) = v
. . . ∗ v
by (16). On the other hand,
i
i
i
j+1
1
j
leftwordj+1(yl−l
by (19), and so we have leftword
i
+1, . . . , yl) = vi
j+1(y1, . . . , yl) =
j+1
j+1
vi ∗ . . .∗ v ∗ v
, as required.
1
ij
ij+1
We can repeat the argument above for the ‘right side’ as well. For every sequence
z1, . . . , zl of points from V(right, j), define
rightwordj(z1, . . . , zl) = a1, . . . , al ,
where the ai are the uniquely determined elements of A such that (M, j, zi ) |= righta .
i
We then have, for every 1 ≤ j ≤ N :
(a ) there is an Rs-path y1, . . . , ym
in V(right, j) of length m
+ · · · + r
such that
j
j = ri1
ij
rightword
∗
j (y1, . . . , ym ) = u
. . .∗ u ;
j
i1
ij
(b ) every Rs-path in V(right, j) is of length ≤ mj;
(c ) for every Rs-path y1, . . . , ym
in V(right, j), we have
j
rightword
∗
j (y1, . . . , ym ) = u
. . .∗ u .
j
i1
ij
206

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Now, by (15) and (22), we have V(left, N ) = V(right, N ). By (a), there exists an Rs-
path y1, . . . , yl in V(left, N ) such that l = nN and leftword
∗
N (y1, . . . , yl) = vi
. . .∗ v
.
1
iN
By (b ), we have nN ≤ mN . Similarly, using (a ) and (b), we obtain mN ≤ nN , from whichnN = mN . Hence, by (c ), rightword
∗
N (y1, . . . , yl) = ui
. . .∗ u
. Since, by (22),
1
iN
leftwordN (y1, . . . , yl) = rightwordN (y1, . . . , yl),
we finally obtain vi ∗ . . .∗ v
= u ∗ . . .∗ u
, as required.
1
iN
i1
iN
Conversely, suppose there is an N ≥ 1 and a sequence i1, . . . , iN for which (14) holds.
We will show that ϕA,P is satisfiable in an Aleksandrov tt-model M =
N, < , N, ≤ , V
with FSA. Let nj = li + · · · + l
and m
+ · · · + r
for every j, 1 ≤ j ≤ N . By our
1
ij
j = ri1
ij
assumption, nN = mN and we have
vi ∗ . . .∗ v
= a
= u ∗ . . .∗ u
.
1
iN
1, . . . , anN
i1
iN
Define a valuation V by taking
• V(range, j) is true iff 0 ≤ j ≤ N ,
• V(stripe, j) = 2m | m < ω, 0 ≤ j ≤ N ,
• V(pairi, j − 1) is true iff i = ij and 1 ≤ j ≤ N,
• V(lefta, j) = k | 1 ≤ k ≤ nj, ak = a for a ∈ A and 1 ≤ j ≤ N ,
• V(righta, j) = k | 1 ≤ k ≤ mj, ak = a for a ∈ A and 1 ≤ j ≤ N,
• V(left, j) =
V(lefta, j)
and
V(right, j) =
V(righta, j).
a∈A
a∈A
One can easily check that under this valuation we have (M, 0) |= ϕA,P and M satisfiesFSA. It is also readily seen that ϕA,P is satisfiable in a tt-model based on N, < iff it issatisfiable in a tt-model based on a finite flow of time.
K
Proof of Theorem 3.7. We show this by modifying formulas from the proof of The-orem 3.6. First, we replace ϕstripe with
2+2∀(stripe
2
2∀(stripe
2
F
F stripe) ∧ 2+
F
F stripe).
Then, ϕleft is the conjunction of (15 )–(21 ), for all i with 1 ≤ i ≤ k,
2+¬3∃ left
2∀ left ≡
left
F
a
leftb
∧ 2+
F
a ,
(15 )
a=b
a∈A
a,b∈A
2+ pair → 2∀(left
F
i
a
2F lefta) ,
(16 )
a∈A
2∀left ∧ 2+2∀(left
Sleft),
(17 )
F
2+ pair → 2∀(left
3
F
i
F Sli left) ,
(18 )
2+ pair →
2∀ (left 2
)
,
(19 )
F
i
F left)
2F ((Sjleft Sj+1left)
leftbili−j
j<li
pair → 2
i
F 3
∃ τ left,
(20 )
i
2F pair → 2∀
i
((left
Sleft)
2F Sτleft) ,
(21 )
i
207

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
where the τ left are defined exactly as in the proof of Theorem 3.6. Formula ϕ
i
right is modified
in a similar way.
K
Remark B.3. In fact, the set of PCP instances without solutions is not recursively enumer-able and therefore, the proofs above show that the sets of PT L ◦ S4u and PT L2 × S4u-formulas which are true in all models based on N, < , Z, < or finite flows of time are notrecursively enumerable either. Therefore, these logics are not recursively axiomatisable.
Appendix C. Spatio-Temporal Logics Based on RC
In this appendix we establish lower and upper complexity bounds for a wide range ofdecidable spatio-temporal combinations and, in particular, prove Theorems 3.8–3.15. Webegin with a straightforward generalisation of Lemma A.1 to the spatio-temporal case:
Lemma C.1. (i) If a PT L × RC-formula ϕ is satisfiable in a tt-model with FSA and basedon a flow of time F then ϕ is satisfiable in an Aleksandrov tt-model based on F and a finitedisjoint union of finite brooms.
(ii) If a PT L ◦ RC-formula ϕ is satisfiable in a tt-model based on a flow of time F then ϕ
is satisfiable in an Aleksandrov tt-model based on F and a (possibly infinite) disjoint unionof ω-brooms.
Proof. (i) By Lemma B.1 (i), ϕ is satisfiable in an Aleksandrov tt-model based on F and afinite quasi-order G. The rest of the proof is similar to that of Lemma A.1. Further detailsare left to the reader.
(ii) By Lemma B.1 (ii), ϕ is satisfiable in an Aleksandrov tt-model based on F and a
quasi-order G = V, R . The rest of the proof again is similar to that of Lemma A.1. Weonly note that although G can be infinite, still for every x ∈ V there is a y ∈ V0 such thatxRy. This is guaranteed by the condition that the set Aw,x, has a maximal point.
K
Observe that Aleksandrov spaces are essentially infinite in case (ii) of Lemma C.1 and a
generalisation of Lemma A.2 does not go through. First, we can easily enforce a topologicalspace to be infinite using the PT L ◦ RCC-8 formula
2+NTTP(p, p).
F
Moreover, the formula
3∃( p
I p )
∧
2+2∀( p
p )
∧
2+2∀
p
I p
I
p
p
p
F
F
is satisfied in an Aleksandrov tt-model based on a single ω-broom, but cannot be satisfiedin an Aleksandrov tt-model based on a union of n-brooms for any finite n.
On the other hand, Aleksandrov tt-models based on disjoint unions of n-brooms, where
n is bounded by the width of the formula, are enough for spatio-temporal logics based onRC−. Recall that spatial terms τ of PT L × RC− (and PT L ◦ RC−) are defined as follows
δ
::=
|
σ,
σ
::=
I
|
δ
|
σ1
σ2,
τ
::=
δ1
· · ·
δm
|
δ
σ
|
σ,
208

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
where the
are spatio-temporal Boolean region terms of PT L × BRCC-8 (and PT L ◦
BRCC-8, respectively). It is not hard to see that, for every tt-model M = F, T, V withF = W, < , T = U, I and every w ∈ W , we have
V(δ, w) = CIV(δ, w)
and
V(σ, w) = ICV(σ, w),
(23)
i.e., the δ are always interpreted by regular closed sets, whereas the σ by regular open ones.
We define the width w(ϕ) of a PT L × RC−-formula ϕ as the maximal number m of
conjuncts in its subformulas of the form 2
∀ (δ1
· · ·
δm), if such subformulas exist, and put
w(ϕ) = 1 otherwise.
Lemma C.2. (i) If a PT L × RC−-formula ϕ is satisfiable in a tt-model with FSA andbased on a flow of time F then ϕ is satisfiable in an Aleksandrov tt-model based on F and afinite disjoint union of w(ϕ)-brooms.
(ii) If a PT L ◦ RC−-formula ϕ is satisfiable in a tt-model based on a flow of time F
then ϕ is satisfiable in an Aleksandrov tt-model based on F and a (possibly infinite) disjointunion of w(ϕ)-brooms.
Proof. By Lemma C.1, we may assume that ϕ is satisfied in an Aleksandrov tt-model M =
F, G, V , where F = W, < and G = V, R is a disjoint union of brooms (in (i), the union
and the brooms are finite). Without loss of generality we may assume that ϕ is composed(using temporal operators and the Booleans) from formulas of the set Σϕ = 3
∃ τ1, . . . , 3
∃ τn,7
where every τi has one of the following forms
δ1
· · ·
δm,
δ
σ
or
σ,
(24)
and the δi, δ and σ are as defined above.
For every 3
∃ τ ∈ Σϕ and every w ∈ W with (M, w) |= 3
∃ τ , we fix a point xτ,w ∈ V such
that (M, w, xτ,w ) |= τ . We may assume that the xτ,w are pairwise distinct and that theroots of all the brooms are the points of the form xτ,w for some w ∈ W and 3
∃ τ ∈ Σϕ.
Therefore, G is a disjoint union of brooms bτ,w, for 3
∃ τ ∈ Σϕ and w ∈ W .
Let us construct a model M = F, G , V
as follows. Given a broom bτ,w, we delete
some of its leaves depending on the form of τ . Three cases are possible:
Case τ = δ1
· · ·
δm: take m leaves y1, . . . , ym of bτ,w such that (M, w, yi ) |= δi and
xτ,wRyi for i = 1, . . . , m and remove all leaves different from y1, . . . , ym.
Case τ = δ
σ: take a leaf y of bτ,w such that (M, w, y ) |= δ and xτ,wRy and remove
all other leaves. Note that, by (23), we have (M, w, y ) |= σ, and therefore (M, w, y ) |= τ .
Case τ = σ: take a leaf y of bτ,w such that xτ,wRy and remove all other leaves. By (23),
we have (M, w, y ) |= τ .
Denote by bτ,w the resulting broom. Clearly, it is a w(ϕ)-broom. Let G = V , R be
the disjoint union of all bτ,w, for 3
∃ τ ∈ Σϕ and w ∈ W . It should be clear that G is as
required. Finally, we define V by taking for every spatial variable p, every w ∈ W andevery x ∈ V ,
x ∈ V (p, w)
iff
there is y ∈ V of depth 0 such that xR y and y ∈ V(p, w).
7. We treat 3
∃ as primitive and 2
∀
as an abbreviation.
209

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
To show that ϕ is satisfied in M , we first prove that, for all w ∈ W and all 3
∃ τ ∈ Σϕ,
(M , w) |= 3
∃ τ
iff
(M, w) |= 3
∃ τ.
It is readily proved by induction that we have (M , w, x ) |= τ iff (M, w, x ) |= τ , for allpoints x ∈ V of depth 0, all w ∈ W and all spatio-temporal terms τ .
Then, by the construction, we also have that, for all formulas 3
∃ τ ∈ Σϕ and all w ∈ W ,
(M, w) |= 3
∃ τ implies (M , w) |= 3
∃ τ . So it remains to show that (M, w) |= ¬3
∃ τ implies
(M , w) |= ¬3
∃ τ for all 3
∃ τ ∈ Σϕ and all w ∈ W . Suppose that we have (M , w, x ) |= τ and
(M, w) |= ¬3
∃ τ . Consider three possible cases for τ :
Case τ = δ1
· · ·
δm. Then, for every i, 1 ≤ i ≤ m, there is yi ∈ V of depth 0 such
that xR yi and (M , w, yi ) |= δi. But then (M, w, yi ) |= δi and, by (23), (M, w, x ) |= δi.Therefore, (M, w, x ) |= τ , contrary to (M, w) |= ¬3
∃ τ .
Case τ = δ
σ. Then there is y ∈ V of depth 0 such that xR y, (M , w, y ) |= δ and,
by (23), (M , w, y ) |= σ. Thus (M , w, y ) |= τ . But then (M, w, y ) |= τ , contrary to(M, w) |= ¬3
∃ τ .
Case τ = σ. Then there is y ∈ V of depth 0 with xR y and, by (23), (M , w, y ) |= τ .
But then (M, w, y ) |= τ , contrary to (M, w) |= ¬3
∃ τ .
Now, by a straightforward induction we can easily show that, for all w ∈ W and all
formulas ψ built from Σϕ using the temporal operators and the Booleans,
(M , w) |= ψ
iff
(M, w) |= ψ.
It follows that ϕ is satisfied in M .
K
C.1 Lower Complexity Bounds (I)
Proof of Theorem 3.10, lower bound. The proof is by reduction of an arbitrary prob-lem in 2EXPSPACE to the satisfiability problem of PT L ◦ RC. Let A be a (single-tape,deterministic) Turing machine such that A halts on every input (accepting or rejecting it),
and A uses ≤ 22f(n) cells of the tape on any input of length n, for some polynomial f . Givenany such Turing machine A and an input x for it, we will construct a PT L ◦ RC-formulaϕA,x (using only future-time temporal operators) such that
(i) the length of ϕA,x is polynomial in the size of A and x;
(ii) if ϕA,x is satisfiable in a tt-model based on N, < then A accepts x; and
(iii) if A accepts x then ϕA,x is satisfiable in a tt-model with FSA and based on N, < .
The case of Z, < as a flow of time (with or without FSA) follows immediately. The caseof finite flows of time can be proved by relativising the temporal operators of ϕA,x (say,by a propositional variable range as in the proof of Theorem 3.6 in Appendix B.2 and inthe proof of the lower bound of Theorem 3.9 below): we can obtain a formula ϕ
such
A,x
that ϕ
is satisfiable in an Aleksandrov tt-model based on
A,x
N, < iff it is satisfiable in an
Aleksandrov tt-model based on the same quasi-order but on a finite flow of time. So thisway all the lower bound results of this theorem follow.
210

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Given a Turing machine A, polynomial f , and input x = x1, . . . , xn as above, let
d = f (n),
exp(1, d) = d · 2d
and
exp(2, d) = exp(1, d) · 2exp(1,d).
Then we have
22f(n) ≤ exp(2, d).
(25)
Our plan is as follows. First, we will show that ‘yardsticks’ of length exp(2, d) (similar tothose used by Stockmeyer, 1974 or Halpern and Vardi, 1989) can be encoded by PT L ◦ RC-formulas of length polynomial in d. These yardsticks will be used to define a temporaloperator
exp(2,d). Then, using this operator, we will encode the computation of A on
input x.
By Lemma C.1 (ii), if a PT L ◦ RC-formula ϕA,x is satisfied in a tt-model based on a flow
of time N, < , then it is satisfied in an Aleksandrov tt-model M =
N, < , G, U , where
G = V, R is a disjoint union of ω-brooms. Take such a model M and suppose that thePT L ◦ RC-formula8
2+2∀ aux ≡
aux
(26)
F
is true in M at moment 0. Since region aux does not change over time, we can divide allpoints in V into three disjoint sets: external, boundary and internal points with respect to
aux —i.e., those satisfying
ep(aux) = aux ,
bp(aux) = aux
I aux
and
I aux ,
respectively. Note that every boundary point has a non-boundary R-successor, so boundarypoints can only be of depth 1. In what follows we simply speak about external and boundarypoints not mentioning ‘with respect to aux .’
We define the ‘ exp(2,d) operator’ by a PT L ◦ RC-formula of length polynomial in d as
follows:
(a) First, we ‘encode’ yardsticks of length d. We will use different formulas for yardsticks
on external points and for yardsticks on boundary points.
(b) Then, with the help of d-yardsticks, we ‘encode’ yardsticks of length exp(1, d). We
will again use different formulas for external and boundary points.
(c) Next, with the help of exp(1, d)-yardsticks on both boundary and external points, we
‘encode’ yardsticks of length exp(2, d) on boundary points.
(d) Finally, with the help of exp(2, d)-yardsticks on boundary points, we define a polyno-
mial-length ‘ exp(2,d) operator’ applicable to propositional variables.
Step (a). Suppose that (26) and the following formula hold in M at 0:
2+2∀ bp(aux)
δ
2∀ ep(aux)
δext
F
0,d
∧ 2+
F
0,d
(27)
where
d−1
δ
j
0,d =
delim0 ≡
ddelim0
delim0
delim0
,
j=1
8. Recall that τ1 ≡ τ2 stands for (τ1
τ2)
(τ2
τ1). We assume that
and
bind stronger than ≡.
211

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
and δext results from δ
0,d
0,d by replacing each occurrence of delim0 with ext delim0.
Take a boundary point z. Suppose that v ∈ N is such that (M, v, x ) |= delim0 . By
δ0,d, for every time moment w ≥ v,
(M, w, z ) |= delim0
iff
w ≡ v
(mod d),
that is, on z, delim0 holds once in every d time instants, starting from v. By the secondconjunct of (27), external points of aux behave similarly with respect to ext delim0 .
Step (b). To encode yardsticks of length exp(1, d), recall first that every number a < 2d
can be represented in binary by a sequence a0 . . . ad−1 of bits. We will ‘mark’ the bits ofbinary numbers by a region term bit1 as follows. Given a boundary point z and a timemoment v such that (M, v, z ) |= delim0 , we say that an interval [w, w + d − 1], for somew = v + j · d, j ∈ N, encodes a number a < 2d on z, if for every i < d,
(M, w + i, z ) |= bit1
iff
ai = 1.
Recall that the binary representation b0 . . . bd−1 is the successor of a0 . . . ad−1 modulo 2d ifthe following holds: for all i, 0 ≤ i < d, we have ai = bi iff aj = 0, for some j, i < j < d.We will use the d-intervals starting from v to encode < 2d numbers in such a way thatconsecutive intervals encode consecutive (modulo 2d) numbers, starting from 0.
So, suppose that (26), (27) and the following formula hold in M at 0:
2+2∀ bp(aux)
γ
2∀ ep(aux)
γext
F
1,d
δ1,d
∧ 2+
F
1,d
δext
1,d
,
(28)
where
γ1,d
=
lwr1
≡
delim0
bit1
lwr1
zr1
≡
bit1
delim0
zr1
delim1
≡
delim0
zr1 ,
δ1,d
=
lwr1
≡
bit1 ≡
dbit1
,
and both γext and δext result from γ
1,d
1,d
1,d and δ1,d, respectively, by attaching prefix ext
to all
of their spatial variables (save aux).
Take a boundary point z. Suppose that v ∈ N is such that (M, v, z ) |= delim1 .
Then, by the last conjunct of γ1,d, we have (M, v, z ) |= delim0 . Since, by (a), delim0holds once in every d time instants on z,
delim0 ‘marks’ the starting moment of each
d-interval. Then, by the first conjunct of γ1,d, for every i, 0 ≤ i < d, we have9
(M, v + i, z ) |= lwr1
iff
(M, v + j, z ) |= bit1 , for all j, i < j < d.
Therefore, δ1,d says that consecutive < 2d numbers (starting with 0) are encoded by consec-utive d-intervals (starting from v). Similarly to the first conjunct of γ1,d, its second conjunctensures that, for every i, 0 ≤ i < d,
(M, v + i, z ) |= zr1
iff
(M, v + j, z ) |= bit1 , for all j, i ≤ j < d.
9. Since we cannot apply the U operator to form spatio-temporal terms, auxiliary regions are used instead:
¦
§
¦
§  ¦
§ ¦
§¡
¦
§
¦
§
¦
§
lwr1
≡
delim0
bit1
lwr1
ensures that
lwr1
behaves as
bit1 U delim0 . This
equality term can indeed be regarded as a fixed point characterisation of the U operator. Note also that
¦
§
¦
§
we do not need to require (as we should do for the fixed point characterisation) lwr1
3F delim0 to
be true because the eventuality is already enforced by δ0,d.
212

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
So, by the last conjunct of γ1,d, delim1 holds on z once in every exp(1, d) = d · 2d timeinstants, starting from v. By the second conjunct of (28), external points behave similarlywith respect to ext delim1 .
Step (c). Now we construct yardsticks of length exp(2, d), using the exp(1, d)-yardsticks
constructed in (b). Suppose that (26)–(28) and the following formulas hold in M at 0:
2+2∀ bp(aux)
ext delim
2∀ ext delim
F
1
∧ 2+
F
1
(ep(aux)
bp(aux)) ,
(29)
2+2∀ ep(aux)
η
F
1,d(bit2) ,
(30)
2+2∀ bp(aux)
γ
F
2,d
δ2,d ,
(31)
where γ2,d is defined similarly to γ1,d and
η1,d(bit2)
=
jm1 bit2
≡
ext delim1
bit2
ext delim1
jm1 bit2
,
δ2,d
=
bit2 ≡ I bit2
lwr2
≡
bit2 ≡ J1,d bit2 ,
J1,d bit2
=
I (aux
ext delim1)
jm1 bit2 .
Take a boundary point z. Suppose v is a time moment such that (M, v, z ) |= delim2 .Then, by the last conjunct of γ2,d, (M, v, z ) |= delim1 . We know from (b) that delim1holds on z once in every exp(1, d) time instants starting from v. So, by δ2,d and the firstconjunct of γ2,d we intend to express that consecutive < 2exp(1,d) numbers (starting with0) are encoded by consecutive exp(1, d)-intervals starting from v. If we could do this then,by the last conjunct of γ2,d, delim2 would hold on z once in every exp(2, d) time instantsstarting from v. The only problem (and the only difference from step (b)) is that to ‘mark’the bits of < 2exp(1,d) binary numbers by a term bit2 , we need to show that the (polynomiallength) term J1,d bit2 actually defines ‘ exp(1,d) bit2 ’ in the sense that, for every w ≥ v,
(M, w, z ) |= J1,d bit2
iff
(M, w + exp(1, d), z ) |= bit2 .
(32)
Suppose first that (M, w, z ) |= J1,d bit2. Then, by (29), there is an external R-successor ywof z (of depth 0) such that (M, w, yw ) |= ext delim1 , and so (M, w, yw ) |= jm1 bit2 .On the other hand, it is not hard to see that if (M, w, z ) |= J1,d bit2, then there isan external R-successor yw of z (of depth 0) such that (M, w, yw ) |= ext delim1 but(M, w, yw ) |= jm1 bit2 .
In both cases, it is readily checked that if (M, w, y ) |= ext delim1 , for some external
point y, then, by (30),
(M, w, y ) |= jm1 bit2
iff
(M, w + exp(1, d), y ) |= bit2 .
Now (32) follows by the first conjunct of δ2,d.
Step (d). We are now in a position to define a polynomial-length ‘ exp(2,d) operator’ J2,d
applicable to propositional variables. Recall that a propositional variable p stands for spatialformula 2
∀ p, where p is a spatial variable associated with p. Now, for every propositional
213

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
variable p we intend to apply the new operator to, we introduce a fresh spatial variablejm2 p. Suppose that (26)–(31) and the following formulas hold in M at 0:
2+3∃ bp(aux)
delim
F
2
,
(33)
2+ 2∀ p ↔ ¬2∀ p
∧ 2+2∀ η
F
F
2,d(p),
(34)
where η2,d(p) is obtained by replacing bit2, jm1 bit2 and ext delim1 in η1,d(bit2) with p,jm2 p and delim2, respectively. Let
J2,d p = 2
∀
(bp(aux)
delim2 )
jm2 p .
We claim that, for every time moment w and every propositional variable p,
(M, w) |= J2,d p
iff
(M, w + exp(2, d)) |= p.
(35)
Suppose first that (M, w) |= J2,d p. Then, by (33), there is a boundary point z suchthat (M, w, z ) |=
delim2 , and therefore (M, w, z ) |= jm2 p . On the other hand,
if (M, w) |= J2,d p, then there is a boundary point z with (M, w, z ) |= delim2 but(M, w, z ) |= jm2 p . In both cases, it is readily checked that if (M, w, z ) |= delim2 ,for some boundary point z, then, by the second conjunct of (34),
(M, w, z ) |= jm2 p
iff
(M, w + exp(2, d), z ) |= p .
Now (35) follows by the first conjunct of (34).
Finally, we are in a position to define the PT L ◦ RC-formula ϕA,x that encodes the
computation of Turing machine A on input x. Let A be the tape alphabet (with the blanksymbol b ∈ A) and S the set of states (with two halt states syes and sno in S) of A. We usethe symbol £ /
∈ A to mark the left end of the tape. We know that the space used by A on
input x = x1, . . . , xn is ≤ 22f(n), which is ≤ exp(2, d) by (25). So we can represent eachconfiguration of the computation of A on x as a finite word
£, a1, . . . , ai−1, s, ai , ai+1, . . . , am, b, . . . , b
of length exp(2, d), where a1, . . . , am ∈ A and s, ai ∈ S × A represents the current stateand the active cell. The transition function δ of A takes triples of the form ai, s, aj , ak(for ai ∈ A ∪ £, aj, ak ∈ A, s ∈ S − syes, sno) to similar triples. For instance,
δ(ai, s, aj , ak) = ai, aj, s , ak
means that, when being in state s and reading symbol aj, the new state should be s andthe head should move one cell to the right. We also assume that, for all ai ∈ A ∪ £ andaj, ak ∈ A, we have δ(ai, syes, aj , ak) = ai, aj, ak and δ(ai, sno, aj , ak) = ai, aj, akmeaning that the head is removed after A is being halted.
Now, for every α ∈ A ∪ £ ∪ (S × A), we introduce a fresh propositional variable pα.
Let ϕA,x be the conjunction of (26)–(31), (33) and an instance of (34), for each pα, as well
214

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
9
6 9
6
exp(1, d) many lj
exp(1,d)
exp(1, d) many lj
exp(1,d)
§
0
l
exp(2,d)−1
l
™
™
™
™
™ ¤ 0 r
§
¤exp(2,d)−1
¦
Â¥
™
™
™
™
™
r
. . .

I
¦
Â¥
r
‰
¨
B

I
 ¦
§
r
‰
¨
B
 ¦
§
r
¨

d
s
T
 

r
¨


ep(aux)
d
s
T
 

r d
 


¨
I aux
ep(aux) rd
 

¨
I aux
r
¨
r

¨
d
r rd


d
r rd


 
¨
 
¨
r
E

r
E
0
exp(2,d)−1
8
bp(aux)
7 8
bp(aux)
7
exp(2, d) many (exp(1, d) + 1)-brooms
Figure 8: Structure of yardsticks.
as the following formulas:
2+ ¬p ∨ ¬p
F
α
β ,
(36)
α,β∈A∪£∪S×A
α=β
p ∧
∧
∧
∧
U
£
(p s
(p
(· · · ∧
(p
p
p
0,x1
x2
xn
b
£) · · · ))),
(37)
2+
af head ↔
p
F
s,a
,
(38)
s,a ∈S×A
2+
af head → p → J
∧
p → J
∧
p → J
F
α
2,d pα
β
2,d pβ
γ
2,d pγ
, (39)
δ(α,β,γ)=
α ,β ,γ
2+ ¬
af head ∨
af head ∨ af head → p → J
F
a
2,d pa
,
(40)
a∈A∪£
3F
p
∧ ¬3
s
p
yes,a
F
sno,a .
(41)
a∈A
a∈A
Suppose first that ϕA,x holds in M at time moment 0. By (36)–(40) and (35), the consecutiveconfigurations of the computation of A on input x are properly ‘encoded’ along the timeaxis. (For instance, p£ holds once in every exp(2, d) time moments.) Finally, (41) says thatA accepts input x.
Conversely, suppose that A accepts input x. We will define an Aleksandrov tt-model
M =
N, < , G, U with FSA that satisfies ϕA,x. Let the partial order G = V, R be a
disjoint union of exp(2, d) many (exp(1, d) + 1)-brooms (see Fig. 8):
V = ri | i < exp(2, d) ∪ lj | i < exp(2, d), j ≤ exp(1, d),
i
zRy
iff
z = y
or
z = ri, y = lj, for some i, j.
i
Suppose that the number of steps in the computation of A on x is m. Then M will havea prefix of length N = m · exp(2, d) after which the final configuration (without a haltingstate) repeats to infinity. For w ∈ N, let
exp(1,d)
U(w, aux) = l
| i < exp(2, d).
i
215

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Then it is easy to see that the boundary points are the ri, and the external points are thelj, for i < exp(1, d). Now put, for every w ∈
i
N,
exp(1,d)
U(w, delim2) = l
| i ≡ w
(mod exp(2, d)),
i
exp(1,d)
U(w, delim1) = l
| i ≡ w
(mod exp(1, d)),
i
exp(1,d)
U(w, delim0) = l
| i ≡ w
(mod d),
i
U(w, ext delim1) = lv |
i
v ≡ w
(mod exp(1, d)), i < exp(2, d),
U(w, ext delim0) = lv |
i
v ≡ w
(mod d), i < exp(2, d).
The valuations for the other variables should be clear. We then have
exp(1,d)
(M, w, z ) |= delim2
iff
z = ri or z = l
for some i ≡ w
(mod exp(2, d)),
i
exp(1,d)
(M, w, z ) |= delim1
iff
z = ri or z = l
for some i ≡ w
(mod exp(1, d)),
i
(M, w, z ) |= ext delim1
iff
z = ri or z = lvi for some v ≡ w (mod exp(2, d))
and i < exp(2, d),
and so on, as required. It is not hard to see that M satisfies FSA and (M, 0) |= ϕA,x.
K
Proof of Theorem 3.9, lower bound. The proof is by reduction of the 2n-corridor tilingproblem which is known to be EXPSPACE-complete (Chlebus, 1986; van Emde Boas, 1997).The problem can be formulated as follows: given an instance T = T, t0, t1, n , where T isa finite set of tile types, t0, t1 ∈ T and n > 0, decide whether there is an m ∈ N such thatT tiles the m × 2n-grid (or corridor) in such a way that t0 is placed onto 0, 0 , t1 onto
m − 1, 0 , and the top and bottom sides of the corridor are of some fixed colour, say, white.
Suppose T = T, t0, t1, n is given. Our aim is to construct (using only future-time
temporal operators) a PT L ◦ BRCC-8 formula ϕT such that
(i) the length of ϕT is a polynomial function of |T | and n;
(ii) if ϕT is satisfiable in a tt-model based on N, < then there is m ∈ N such that T tiles
the m × 2n-corridor;
(iii) if there is m ∈ N such that T tiles the m × 2n-corridor, then ϕT is satisfiable in a
tt-model with FSA and based on N, < ;
(iv) ϕT is satisfiable in a tt-model based on N, < iff it is satisfiable in a tt-model based
on a finite flow of time.
The case of Z, < follows immediately.
Recall that, by Lemma C.2 (ii), if ϕT is satisfied in a tt-model then it is satisfied in
an Aleksandrov tt-model M =
N, < , G, V , where G = V, R is a disjoint union of ω-
brooms. To explain the meaning of ϕT ’s subformulas, we assume that such a model M isgiven. Throughout the proof we use only a restricted subset of RCC-8 predicates: for spatio-temporal terms τ1 and τ2 constructed from spatial variables using only the complement, theintersection and the next-time operator
, we need EQ(τ1, τ2) as well as two abbreviations
P(τ1, τ2) = EQ(τ1, τ2) ∨ TPP(τ1, τ2) ∨ NTPP(τ1, τ2) and E τ1 = ¬DC(τ1, τ1) standing for ‘τ1
216

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
0
m · 2n
(m + 1) · 2n
count
range
E
0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
...
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
σ0
σ1
σ2
σ3
σ0
σ1
σ2
σ3
σ0
σ1
σ2
σ3
σ0
σ1
σ2
σ3
σ0
Figure 9: Counting formulas for m = 3 and n = 2.
is a part of τ2’ and ‘τ1 is nonempty,’ respectively. Clearly, this language forms a subset ofPT L ◦ BRCC-8 (in fact, as we show in Remark C.3 below, the proof goes through for aneven more restricted subset of the langauge).
Our first step in the construction of ϕT (which will contain, among many others, spatial
variables t for all t ∈ T ) is to write down formulas forcing a sequence y0, y1, . . . , ym·2n−1of distinct points (of depth 0) from V , for some m ∈ N, such that, for each i < m · 2n,(M, i, yi ) |= t for a unique tile type t ∈ T . If i = k · 2n + j, for some k < m, j < 2n,then we will use yi (at time i) to encode the pair k, j of the m × 2n-grid. Thus, the upneighbour k, j + 1 of k, j will be coded by the point yi+1 at time i + 1, while its rightneighbour k + 1, j by yi+2n at moment i + 2n (see Fig. 10).
Let q0, . . . , qn−1 be pairwise distinct propositional variables and
d
σ
n−1
j = qd0 ∧ · · · ∧ q
,
0
n−1
where dn−1 . . . d0 is the binary representation of j < 2n, q0 = ¬q
= q
i
i and q1
i
i, for each i.
Suppose that the formula
count ∧ σ0
∧
count U (σ0 ∧ 2+¬count) ∧ 2+ count → χ
(42)
F
F
is true in M at 0, where count is a fresh propositional variable and χ is the following‘counting’ formula (the length of which is polynomial in n)
χ =
q ∧ ¬
→
¬
∧
∧
↔
i
qk
qi
qk
(qi
qi)
∧
σ2n−1 →
σ0 .
k<n
i<k
i<k
k<i<n
Then there is an m ∈ N such that count is true before moment (m + 1) · 2n and false startingfrom (m + 1) · 2n. The sequence σ0, σ1, . . . , σ2n−1 is repeated m+1 times along the time-line,i.e., while count is true. Let
range = 3F (count ∧ σ0).
Clearly, range is true before moment m · 2n and then always false (see Fig. 9).
Let equ, p0, . . . , pn−1 and e0, . . . , en−1 be fresh distinct spatial variables, and
d
π
n−1
j = pd0
· · ·
p
,
0
n−1
where dn−1 . . . d0 is the binary representation of j < 2n, p0 = p
= p
i
i and p1
i
i, for each i.
Suppose that (42) and
2+EQ equ,
e
2+ q ↔ EQ(e
2+EQ p
F
i
∧
F
i
i, pi)
∧
F
i,
pi
(43)
i<n
i<n
i<n
217

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
are true in M at 0. Then, by the first two conjuncts of (43), for all i ∈ N and y ∈ V ofdepth 0, there is j < 2n such that (M, i, y ) |= equ iff (M, i) |= σj and (M, i, y ) |= πj. Bythe last conjunct of (43), we then have
(M, i, y ) |= equ
iff
∃j < 2n (M, i) |= σj
and
(M, k, y ) |= πj, for all k ∈ N . (∗)
We can generate the required sequence of points yi using the formulas:
range ∧ 2+(range → E tile),
(44)
F
2+EQ tile, equ
t
no t in future ,
(45)
F
t∈T
t∈T
2+P no t in future, t
no t in future ,
(46)
F
t∈T
where tile and the no t in future (for all t ∈ T ) are fresh spatial variables. Indeed, supposethe conjunction of (42)–(46) holds at time 0 in M. Then, by the first conjunct of (44) and(42), (M, 0) |= range ∧ σ0 and, by the second conjunct of (44), (M, 0, y0 ) |= tile for somey0 ∈ V . We may assume that y0 is of depth 0. Then, by (45), we have
(a0) (M, 0, y0 ) |= equ, and, by (∗), (M, k, y0 ) |= π0 for all k ∈ N;
(b0) for all t ∈ T , (M, 0, y0 ) |= no t in future and, by (46), (M, k, y0 ) |= t for all k > 0.
Next, by (42), we have (M, 1) |= range ∧ σ1 and, by (44), there is y1 ∈ V (again, of depth0) such that (M, 1, y1 ) |= tile. In particular, we have:
(a1) (M, 1, y1 ) |= equ, and, by (∗), (M, k, y1 ) |= π1 for all k ∈ N;
(b1) for all t ∈ T , (M, 1, y1 ) |= no t in future and, by (46), (M, k, y1 ) |= t for all k > 1.
By (b0), (M, 1, y0 ) |= t, for all t ∈ T , and thus y1 = y0. Now we consider y1 at moment 1and use the same argument to find a point y2 ∈ V (which is different from y1 by (b1)), andso forth; see Fig. 10. This gives us points y0, y1, . . . , ym·2n−1 (of depth 0) from V we need.
Our next aim is to write down formulas that could serve as pointers to the up and right
neighbours of a given pair in the corridor (at this moment we do not bother about its topborder). Consider the formulas
2+EQ up, tile ,
(47)
F
2+EQ right, equ no equ U tile ,
(48)
F
2+EQ no equ U tile, tile
equ
no equ U tile
,
(49)
F
where up, right and no equ U tile are fresh spatial variables.
We claim that, for all
i, j < m · 2n,
• (M, i, yj ) |= up
iff
j = i + 1;
• (M, i, yj ) |= right
iff
j = i + 2n.
218

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
˜ = t for all t∈T
q£¢ q ¡= no equ U tile
range
V
equ
equ
up
π
q
q
q
q
q
q
q
q£
equ
3 →
y11
¢
q
q
q ¡ r
˜
right
tile
equ
equ
up
π
q
q
q
q
q
q
q£
equ
2 →
y10
¢
q
q
q ¡ r
˜
˜
right
tile
T
equ
equ
up
π
q
q
q
q
q
q£
equ
1 →
y9
¢
q
q
q ¡ r
˜
˜
˜
right
right
tile
equ
equ
up
equ
T
π
q
q
q
q
q£
equ
0 →
y8
¢
q
q
q ¡ r
˜
˜
˜
˜
right
tile
equ
up
equ
π
q
q
q
q£
equ
3 →
y7
¢
q
q
q ¡ r
˜
˜
˜
˜
˜
right
tile
equ
up
equ
π
q
q
q£
equ
2 →
y6
¢
q
q
q ¡ r
˜
˜
˜
˜
˜
˜
up
right
tile
T
equ
up
equ
π
q
q£
equ
sT
)
1 →
y5
¢
q
q
q ¡ r
˜
˜
˜
˜
˜
˜
˜
right
tile
equ
up
equ
equ
π
q£
equ
0 →
y4
¢
q
q
q ¡ r
˜
˜
˜
˜
˜
˜
˜
˜
right
tile
up
equ
equ
π
q£
equ
3 →
y3
¢
q
q ¡ r
˜
˜
˜
˜
˜
˜
˜
˜
˜
tile
up
equ
equ
π
q£
equ
2 →
y2
¢
q ¡ r
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
up
tile
up
equ
equ
T
π
q£ equ
™
1 →
y1
¢ ¡
r
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
E right
tile
equ
equ
equ
π
r
equ
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
˜
0 →
y0 tile
0
1
2
3
4
5
6
7
8
9
10
11
12
...
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
↑
3 × 22 corridor
σ0
σ1
σ2
σ3
σ0
σ1
σ2
σ3
σ0
σ1
σ2
σ3
σ0
Figure 10: Satisfying ϕT , n = 2, in a tt-model based on space with 3 · 22 points.
The former is obvious. Let us prove the latter. To show that (M, i, yj ) |= right, forj = i + 2n, we first observe that (M, j, yj ) |= equ and (M, i, yj ) |= equ by (∗). It followsfrom (M, j, yj ) |= tile by (49) that (M, j − 1, yj ) |= no equ U tile. Then, applying(49) (from right to left) sufficiently many times, we obtain (M, i, yj ) |= no equ U tile,(M, i − 1, yj ) |= no equ U tile, and so (M, i, yj ) |= right.
Conversely, suppose that (M, i, yj ) |= right for some yj. Then (M, i, yj ) |= equ and,
by (∗) (note that i + 2n < (m + 1) · 2n, and so count is still true at i + 2n),
(M, i + 2n, yj ) |= equ.
(∗∗)
We have (M, i, yj ) |= no equ U tile. Then applying (49) (from left to right) sufficientlymany times we arrive at (M, i + 2n − 1, yj ) |= no equ U tile which together with (∗∗)gives (M, i + 2n, yj ) |= tile. But then j = i + 2n.
It should be noted that at every time point the extension of no equ U tile coincides with
the extension of the term equ U tile on elements of the sequence y0, . . . , ym·2n, and that (49)is indeed the fixed point characterisation of this U operator.
Finally, the formulas below ensure that every point of the m × 2n-corridor is covered by
at most one tile, 0, 0 is covered by t0, m − 1, 0 by t1, the top and bottom sides are white
219

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
and that the colours on adjacent edges of adjacent tiles match:
2+¬E (t t ),
(50)
F
t,t ∈T
t=t
P(tile, t0) ∧ 2+
σ
F
0 ∧ range
∧ ¬3F σ0 ∧ range → P tile, t1
,
(51)
2+ σ
P tile, t
,
(52)
F
2n−1 →
t∈T
up(t)=white
2+ σ
P tile, t
,
(53)
F
0 →
t∈T
down(t)=white
2+ ¬σ
F
2n−1 ∧ E t → P up, no t in future
,
(54)
t,t ∈T
up(t)=down(t )
2+ E t → P right, no t in future .
(55)
F
t,t ∈T
right(t)=left(t )
Let ϕT be the conjunction of (42)–(55). Suppose that ϕT holds at 0 in M. Then there
is m ∈ N such that (M, m · 2n − 1) |= range and, for every i ≥ m · 2n, (M, i) |= ¬range.Then we define a map τ : m × 2n → T by taking
τ (k, j) = t
iff
(M, i, yi ) |= t and i = k · 2n + j.
We leave it to the reader to check that τ is a tiling of m × 2n, as required.
For the other direction, suppose that there is a tiling τ of the m × 2n-corridor by T , for
some m > 0. Then ϕT is satisfied in the Aleksandrov tt-model M =
N, < , V, R , V ,
where V = y0, . . . , ym·2n−1, R is the minimal reflexive relation on V ,
V(t, i) = yi ∈ V | τ (k, j) = t and i = k · 2n + j,
and the other variables of ϕT are interpreted as shown in Fig. 10. Clearly, M satisfiesFSA. Moreover, ϕT is satisfiable in tt-models over finite flows of time iff it is satisfiable intt-models over N, < . Details are left to the reader.
K
Remark C.3. It may be of interest to note that the language used in the proof above israther limited. In fact, it is enough to extend the PSPACE-complete logic PT L ◦ RCC-8with predicates of the form EQ( 1, 2
3) (where the
i are atomic spatio-temporal region
terms) to make it EXPSPACE-hard. To show this, we transform the PT L◦BRCC-8 formulaϕT constructed above in the following way. First, we take a fresh spatial variable u (denoting‘the universe’) and add to ϕT the conjunct 2+EQ(u, u). Next, for every spatio-temporal
F
Boolean region term
of ϕT , we introduce a spatial variable neg
(‘the complement of
with respect to u’), add to ϕT conjuncts 2+EQ(u,
neg ) ∧ 2+DC( , neg ), and replace
F
F
every occurrence of
in the resulting formula with neg . Finally, for every spatio-temporal
term of the form 1
2, we introduce a fresh spatial variable
1 and
2, add the conjuncts
2+P(
P(
P(
F
1 and
2,
1) ∧ 2+
F
1 and
2,
2) ∧ 2+
F
1, neg
2
1 and
2)
220

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
and replace occurrences of 1
2 with
1 and
2. One can readily see that (i) the length of
the resulting formula ϕT is linear in the length of ϕT and (ii) ϕT is satisfiable in a tt-modelbased on N, < (with FSA) iff ϕT is satisfiable in a tt-model based on N, < (with FSA).
C.2 Upper Complexity Bounds (I): Quasimodels for PT L × RC
In this appendix we define quasimodels for PT L × RC in the spirit of the paper (Hodkinsonet al., 2000) in order to establish the upper complexity bounds of Theorems 3.10 and 3.13.We remind the reader that spatio-temporal terms of PT L × RC are of the form:
τ
::=
|
I
|
τ
|
τ1
τ2,
::=
CIp
|
CI
|
CI( 1
2)
|
CI( 1 U 2)
|
CI( 1 S 2),
and that PT L ◦ RC forms a sublanguage of PT L × RC—it differs from the latter only inthe definition of spatio-temporal region terms:
::=
CIp
|
CI
|
CI( 1
2)
|
CI
.
Let ϕ be a PT L × RC-formula. Recall from p. 200 that by sub ϕ we denote the set of
all subformulas of ϕ and by term ϕ the set of all its spatio-temporal terms including thoseof the form τ and . A type t for ϕ is a subset of term ϕ such that
• for every τ1
τ2 ∈ term ϕ,
τ1
τ2 ∈ t
iff
τ1 ∈ t and τ2 ∈ t;
• for every τ ∈ term ϕ,
τ ∈ t
iff
τ /
∈ t.
Clearly, the number (ϕ) of different types for ϕ is bounded by 2|term ϕ|.
A broom type b for ϕ is a pair
T, ≤ , t , where T, ≤ is a broom (with T 0 being its
leaves) and t a labelling function associating with each x ∈ T a type t(x) for ϕ such thatthe following conditions hold:
(bt0) t(x) = t(y), for each pair of distinct points x, y ∈ T 0;
(bt1) for every x ∈ T 0,
• for every CI( 1
2) ∈ term ϕ,
CI( 1
2) ∈ t(x)
iff
1 ∈ t(x) and
2 ∈ t(x),
• and for every CI ∈ term ϕ,
CI ∈ t(x)
iff
/
∈ t(x);
(bt2) for every I ∈ term ϕ,
I ∈ t(x)
iff
∈ t(y) for every y ∈ T , x ≤ y;
(bt3) for every
∈ term ϕ,
∈ t(x)
iff
∃y ∈ T 0 with x ≤ y and
∈ t(y).
Broom types b1 =
T1, ≤1 , t1 and b2 =
T2, ≤2 , t2 for ϕ are said to be isomorphic if
• for every x1 ∈ T 0, there is x
such that t
1
2 ∈ T 0
2
1(x1) = t2(x2) and
• for every x2 ∈ T 0, there is x
such that t
2
1 ∈ T 0
1
1(x1) = t2(x2).
Clearly, given two isomorphic broom types b1 and b2, we also have t1(r1) = t2(r2), wherer1 and r2 are the roots of b1 and b2, respectively.
A quasistate for ϕ is a pair s, m , where s is a Boolean-saturated subset of sub ϕ and m a
disjoint union
T, ≤ , t of broom types b1, . . . , bn for ϕ such that the following conditions
hold:
221

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
(qs0) bi and bj are not isomorphic, for i = j;
(qs1) for every 2
∀ τ ∈ sub ϕ,
2∀τ ∈ s iff τ ∈ t(x) for every x ∈ T .
Clearly, the number (ϕ) of quasistates for ϕ is bounded by 22 (ϕ) · 2|sub ϕ|.
Fix a flow of time F = W, < . A basic structure for ϕ is a pair F, q , where q is a
function associating with each w ∈ W a quasistate q(w) = sw, mw for ϕ such that, foreach w ∈ W ,
• for every ψ1 U ψ2 ∈ sub ϕ, ψ1 U ψ2 ∈ sw iff there is v > w such that ψ2 ∈ sv and
ψ1 ∈ su for all u ∈ (w, v);
• for every ψ1 S ψ2 ∈ sub ϕ, ψ1 S ψ2 ∈ sw iff there is v < w such that ψ2 ∈ sv and
ψ1 ∈ su for all u ∈ (v, w).
Let F, q be a basic structure for ϕ, where q(w) = sw, mw and mw =
Tw, ≤w , tw
for w ∈ W . Denote by T 0
w the set of all leaves in
Tw, ≤w and by T 1
w the set of all roots
of brooms in it. A 1-run through
F, q is a function r giving for each w ∈ W a point
r(w) ∈ T 1
w ; a coherent and saturated 0-run through
F, q is a function r giving for each
w ∈ W a point r(w) ∈ T 0
w such that the following conditions hold:
• for every CI( 1 U 2) ∈ term ϕ, CI( 1 U 2) ∈ tw(r(w)) iff there is v > w such that
2 ∈ tv (r(v)) and
1 ∈ tu(r(u)) for all u ∈ (w, v);
• for every CI( 1 S 2) ∈ term ϕ, CI( 1 S 2) ∈ tw(r(w)) iff there is v < w such that
2 ∈ tv (r(v)) and
1 ∈ tu(r(u)) for all u ∈ (v, w).
Say that a quadruple Q = F, q, R,
is a quasimodel for ϕ based on F if F, q is a basic
structure for ϕ, R = R0 ∪ R1, with R1 being a set of 1-runs and R0 a set of coherent andsaturated 0-runs through F, q , and
the reflexive closure of a subset of R1 × R0 such
that
(qm2) ∃w0 ∈ W ϕ ∈ sw ;
0
(qm3) for every w ∈ W and every x ∈ Tw, there is r ∈ R with r(w) = x;
(qm4) for all r, r ∈ R, if r
r then r(w) ≤w r (w) for all w ∈ W ;
(qm5) for all r ∈ R, w ∈ W and x ∈ T 0
w , if r(w) ≤w x then there is r
∈ R0 such that
r (w) = x and r
r .
A quasimodel Q is said to be finitary if the set R of runs is finite.
Lemma C.4. A PT L × RC-formula ϕ is satisfiable in an Aleksandrov tt-model based ona flow of time F and a (finite) disjoint union of (finite) brooms iff there is a (finitary)quasimodel for ϕ based on F.
Proof. (⇐) Let ϕ be a PT L × RC-formula and Q = F, q, R,
a quasimodel for ϕ, where
F = W, < and q(w) = sw, Tw, ≤w , tw
for w ∈ W . We construct an Aleksandrov
tt-model M = F, G, V by taking G = R,
and, for each spatial variable p and w ∈ W ,
V(p, w) = r | CIp ∈ tw(r(w)).
222

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Clearly, if Q is finitary then G is finite. Thus, it remains to prove that ϕ is satisfied in M.
First, we show by induction on the construction of a region term
∈ term ϕ that, for
every w ∈ W and every r ∈ R,
(M, w, r ) |=
iff
∈ tw(r(w)).
(56)
The basis of induction:
= CIp. Let (M, w, r ) |=
. Then there is r ∈ R such that
r
r and (M, w, r ) |= Ip. By (qm4), r(w) ≤w r (w). Take any y ∈ T 0
w , r (w) ≤w y. By
(qm5), there is a run r ∈ R0 such that r
r and r (w) = y. Then (M, w, r ) |= p
and, by the definition of V, CIp ∈ tw(r (w)) and, by (bt3),
∈ tw(r(w)).
Conversely, if
∈ tw(r(w)) then, by (bt3), there is y ∈ T 0
w with r(w) ≤w y and
∈ tw(y). By (qm5), there is r ∈ R0, r
r , such that r (w) = y. Then CIp ∈ tw(r (w))
and, by the definition of V, (M, w, r ) |= p. Therefore, (M, w, r ) |= .
The induction steps for
= CI 1, CI( 1
2), CI( 1 U
2) and CI( 1 S
2) are similar,
but instead of the definition of V, we use (bt1) for the cases of the Booleans and coherenceand saturatedness of r for the cases of temporal operators.
Next, we extend (56) to arbitrary spatio-temporal terms τ ∈ term ϕ.Case τ = I . Suppose that (M, w, r ) |= I . Take any y ∈ Tw, r(w) ≤w y. If y ∈ T 0
w
then, by (qm5), there is r ∈ R0 such that r
r and r (w) = y. If y /
∈ T 0
w then clearly
y = r(w) and take r = r. We have (M, w, r ) |= , which, by IH, implies
∈ tw(r (w)).
Therefore,
∈ tw(y) for every y ≥w r(w) and, by (bt2), I ∈ tw(r(w)).
Conversely, if I ∈ tw(r(w)) then, by (bt2),
∈ tw(y), for every y ≥w r(w). Take any
run r ∈ R such that r
r . By (qm4), r(w) ≤w r (w), and so
∈ tw(r (w)), from which,
by IH, (M, w, r ) |= . Hence, (M, w, r ) |= I .
Cases τ = τ1
τ2 and τ1 follow from IH by the definition of type.
Finally, we show by induction on the construction of ψ ∈ sub ϕ that, for every w ∈ W ,
(M, w) |= ψ
iff
ψ ∈ sw.
(57)
Case ψ = 2
∀ τ . Suppose (M, w) |= 2
∀ τ . Take any x ∈ Tw. By (qm3), there is r ∈ R
such that r(w) = x. Then (M, w, r ) |= τ and, by IH, τ ∈ tw(r(w)). Therefore, by (qs1),2∀τ ∈ sw. Conversely, let 2∀τ ∈ sw. Take any run r ∈ R. By (qs1), we have τ ∈ tw(r(w)),from which, by IH, (M, w, r ) |= τ . Hence, (M, w) |= 2
∀ τ .
Cases ψ = ψ1 ∧ ψ2 and ¬ψ1 follow from IH by the Boolean-saturatedness of the sw.It follows from (57) and (qm2) that ϕ is satisfiable in M.
(⇒) Let ϕ be a PT L × RC-formula and suppose that ϕ is satisfied in an Aleksandrov
tt-model M = F, G, V , where F = W, < and G = ∆, ≤ is a disjoint union of brooms.
Denote by ∆0 and ∆1 the leaves and the roots of brooms in G, respectively. With every
pair w, x ∈ W × ∆ we associate the type
t(w, x) = τ ∈ term ϕ | (M, w, x ) |= τ .
Fix a w ∈ W and define a binary relation on ∆ as follows. For x, x ∈ ∆0, let x ∼w x ifft(w, x) = t(w, x ) and, for z, z ∈ ∆1, let z ∼w z iff the brooms generated by z and z areisomorphic, i.e.,
∀x ∈ ∆0 (z ≤ x → ∃x ∈ ∆0 (z ≤ x ∧ x ∼w x )) ∧
∀x ∈ ∆0 (z ≤ x → ∃x ∈ ∆0 (z ≤ x ∧ x ∼w x )).
223

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Clearly, ∼w is an equivalence relation on ∆. Denote by [x]w the ∼w-equivalence class of xand define a map fw by taking, for each x ∈ ∆,
[x]w,
x ∈ ∆1,
fw(x) =
[z]w, [x]w ,
x ∈ ∆0
and
z ∈ ∆1
such that z ≤ x.
Since G is a disjoint union of brooms, fw is well-defined. Now put
Tw = fw(x) | x ∈ ∆,
u ≤w v
iff
∃x, y ∈ ∆
such that x ≤ y, u = fw(x) and v = fw(y),
tw(fw(x)) = t(w, x),
for x ∈ ∆.
By definition of fw, Tw, ≤w is a union of brooms and tw is well-defined. Consider thestructure sw, mw , where
mw =
Tw, ≤w , tw
and
sw = ψ ∈ sub ϕ | (M, w) |= ψ.
It is readily seen that for each of the brooms of mw we have (bt0) and that mw satisfies(qs0). Moreover, as fw is a p-morphism from ∆, ≤ onto Tw, ≤w , we also have (bt1)–(bt3) and (qs1). So, by taking q(w) = sw, mw for each w ∈ W we obtain a basic structure
F, q for ϕ satisfying (qm2).
It remains to define appropriate runs through F, q . For k = 0, 1, let Rk be the set of
all maps r : w → fw(x) for x ∈ ∆k. Clearly, R1 and R0 are sets of 1- and coherent andsaturated 0-runs, respectively. Put R = R0 ∪ R1 and for r, r ∈ R, r
r iff r(w) ≤w r (w)
for all w ∈ W . Then (qm4) holds by definition. Let v ∈ W and y ∈ Tv. Then thereis x ∈ ∆ such that fv(x) = y. Clearly, R contains the run r : w → fw(x), which proves(qm3). Finally, let r ∈ R, v ∈ W and y ∈ T 0
v be such that r(v) ≤v y. There are some
z, x ∈ ∆ such that fw(z) = r(w), for every w ∈ W , and fv(x) = y. We clearly have z ≤ xand x ∈ ∆0. Then take the run r : w → fw(x). By definition, r
r , which proves (qm5).
Thus, Q = F, q, R,
is a quasimodel for ϕ. Note that if G is finite then R is finite as
well and therefore, Q is finitary.
K
We are now in a position to establish the upper complexity bounds of the satisfiability
problem for PT L × RC- and PT L ◦ RC-formulas in tt-models based on N, < , Z, < orarbitrary finite flows of time.
Proof of Theorem 3.10, upper bound. We consider the cases of
N, <
and
Z, < .
The case of arbitrary finite flows of time and that of tt-models with FSA and based on
N, < and Z, < will follow from Theorem 3.13.
One can readily check that as for the propositional temporal logic PT L, we have the
following polynomial reductions for PT L ◦ RC:
• satisfiability in tt-models based on Z, < can be polynomially reduced to satisfiability
in tt-models based on N, < ;
• satisfiability in tt-models based on N, < can be polynomially reduced to satisfiability
of formulas without past-time temporal operators.
224

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
So, in what follows we consider the simplest case of the satisfiability problem, that is forPT L ◦ RC-formulas without past-time temporal operators in tt-models based on N, < .
We present a nondeterministic 2EXPSPACE satisfiability checking algorithm which is
similar to that of Sistla and Clarke (1985). First, one can prove (with the help of Lem-mas C.1 (ii) and C.4) an analogue of (Hodkinson et al., 2000, Theorem 24) which statesthat a PT L ◦ RC-formula ϕ is satisfiable in tt-model based on N, < iff there are l1, l2 ∈ Nsuch that
2
l1 ≤ (ϕ),
0 < l2 ≤ |term ϕ| · 2 (ϕ)
· (ϕ) + (ϕ)
and a ‘balloon’-like quasimodel Q =
N, < , q, R,
for ϕ with q(l1 + n) = q(l1 + l2 + n)
for every n ∈ N. Although Theorem 24 of (Hodkinson et al., 2000) was proved for themonodic fragment of first-order temporal logic, the basic idea of extracting a ‘balloon’-likequasimodel from an arbitrary one works for PT L ◦ RC as well. The only difference is thatquasistates now are more complex: they can be regarded as sets of sets of types for ϕ (notjust sets of types) and thus, both l1 and l2 are triple exponential in the length (ϕ) of ϕ.Then a quasimodel Q can be guessed in 2EXPSPACE by an algorithm which is very similarto that in the proof of (Hodkinson et al., 2003, Theorem 4.1).
K
Proof of Theorem 3.13, upper bound. The proof is similar to that of Theorem 3.10.Again, one can show that all the cases are polynomially reducible to the case of satisfiabilityof PT L × RC-formulas without past-time temporal operators in tt-models with FSA andbased on N, < . To take the FSA into account, we can prove (using Lemmas C.1 (i)and C.4) analogues of Theorems 29 and 35 of (Hodkinson et al., 2000) which state that aPT L × RC-formula ϕ is satisfiable in a tt-model with FSA and based on N, < iff thereis a finitary ‘balloon’-like quasimodel for ϕ based on N, < . The condition of finiteness forthe set of runs can also be ensured by an algorithm similar to that of Theorem 3.10.
K
C.3 Upper Complexity Bounds (II):
Embedding into First-Order Temporal Logic
In this appendix we introduce the first-order temporal language QT L and use some knowncomplexity results for fragments of QT L to obtain upper complexity bounds for spatio-temporal logics based on RC− (and therefore, on BRCC-8).
The alphabet of QT L consists of individual variables x1, x2, . . . , predicate symbols
P1, P2, . . . , each of which is of some fixed arity, the Booleans, the universal ∀x and ex-istential ∃x quantifiers for each variable x, and the temporal operators U , S (with theirderivatives
, 3F , 2F , etc.). Note that our language contains neither constant symbols
nor equality (we simply do not need them to obtain our complexity results).
QT L is interpreted in first-order temporal models of the form M = F, D, I , where
F =
W, < is a flow of time, D a nonempty set, the domain of M, and I a function
associating with every moment of time w ∈ W a first-order structure
I(w)
I(w)
I(w) =
D, P
, P
, . . . ,
0
1
I(w)
the state of M at moment w, where each P
is a relation on D of the same arity as P
i
i.
An assignment in D is a function a from the set of individual variables to D. Given suchan assignment and a QT L-formula ϕ, we define the truth-relation (M, w) |=a ϕ by taking
225

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
u = CIp
e = CIp
9
6
x1
x2
xn−1
xn
u
b
e
b
e
b
ub
depth 0
. . .
Pj1[db]¬Pj2[db] . . .¬Pjn−1[db]Pjn[db]
r
‰
¨
B
=⇒
r
d
s
 

¨
r
¨
d
 
r
¨
r
¨
8
7
depth 1
b
d
r u
 
¨
x0b
db
Figure 11: Representing n-broom b with region CIpj by a point in a first-order model.
•
I(w)
(M, w) |=a Pi(x1, . . . , xm) iff a(x1), . . . , a(xm) ∈ P
,
i
• (M, w) |=a ∀x ψ iff (M, w) |=a ψ, for every assignment a in D which differ from a
only on x,
plus the standard clauses for the Booleans and temporal operators. We say that a QT L-formula ϕ is satisfied in M if (M, w) |=a ϕ for some w ∈ W and some assignment a in D.If all free variables of ϕ are among x1, . . . , xm, then instead of (M, w) |=a ϕ we often write(M, w) |= ϕ[d1, . . . , dm], where di = a(xi) for all i, 1 ≤ i ≤ m.
Denote by QT L1 the one-variable fragment of QT L, i.e., the set of all QT L-formulas
which contain at most one individual variable, say, x. Without loss of generality we mayassume that all predicate symbols of QT L1 are at most unary.
Now we define an embedding of spatio-temporal languages based on RC− into QT L1.
Recall that, by Lemma C.2 (i), if a PT L × RC−-formula ϕ of width n is satisfied in att-model with FSA then ϕ is also satisfiable in an Aleksandrov tt-model based on the sameflow of time and a finite disjoint union of n-brooms. Similarly, if a PT L ◦ RC−-formula ϕof width n is satisfiable then ϕ is also satisfiable in an Aleksandrov tt-model based on thesame flow of time and possibly infinite disjoint union of n-brooms.
To cover both cases, let ϕ be a PT L × RC−-formula of width n. We show how to
construct a QT L1-formula ϕ†n of length linear in (ϕ) such that every Aleksandrov tt-modelbased on a (finite) union of n-brooms satisfying ϕ gives rise to a first-order temporal model(with finite domain, respectively) satisfying ϕ†n and vice versa. Thus, we polynomiallyreduce the satisfiability problem for spatio-temporal languages to that for QT L1.
Suppose that ϕ is satisfied in an Aleksandrov tt-model M = F, G, V , where F = W, <
and G is a (finite or infinite) disjoint union of n-brooms. With every n-broom b of G weassociate an element db of the first-order domain D. Then, for every spatial variable pj in ϕ,we fix n different unary predicate symbols Pj1(x), . . . , Pjn(x) with the following meaning:Pji(x) is true on db ∈ D at moment w ∈ W iff the i-th leaf of b (xi in Fig. 11) belongs to
b
region CIp at w. Define n distinct translations ·†in , 1 ≤ i ≤ n, encoding the truth valuesof spatio-temporal region terms of ϕ on leaves of G by taking, for a spatial variable pj andterms 1 and 2,
(CIpj)†in = Pji(x),
(CI 1)†in = ¬( 1)†in,
(CI( 1
2))†in = ( 1)†in ∧ ( 2)†in ,
(CI( 1 U 2))†in = ( 1)†in U ( 2)†in,
(CI( 1 S 2))†in = ( 1)†in S ( 2)†in.
226

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Next we extend these n translations to arbitrary spatio-temporal terms of ϕ. First weintroduce a translation ·†0n to encode the truth value of arbitrary spatio-temporal terms inthe roots of the n-brooms of G: for a region term , let
n
( )†0n =
( )†kn .
k=1
The formula above shows, in particular, that ·†0n is redundant for region terms since theirtruth values in the roots can be ‘computed’ as defined by ·†0n . For a spatio-temporal termof the form I , where
is a region term, we take
n
(I )†0n =
( )†kn
and
(I )†in = ( )†in
for all i, 1 ≤ i ≤ n,
k=1
and then, for spatio-temporal terms τ1 and τ2,10
(τ1)†in = ¬(τ1)†in
and
(τ1
τ2)†in = (τ1)†in ∧ (τ2)†in
for all i, 0 ≤ i ≤ n.
Finally, we define the translation ·†n of subformulas of ϕ: for a spatio-temporal term τ ,
n
(2
∀ τ )†n = ∀x (τ )†0n
∧
∀x (τ )†kn
k=1
and, for spatio-temporal formulas ψ1 and ψ2,
(¬ψ1)†n = ¬ψ†n,
(ψ
∧ ψ†n,
1
1 ∧ ψ2)†n = ψ†n
1
2
(ψ1 U ψ2)†n = ψ†n U ψ†n,
(ψ
S ψ†n,
1
2
1 S ψ2)†n = ψ†n
1
2
Clearly, the length of ϕ†n is linear in both n and (ϕ).
Lemma C.5. A PT L × RC−-formula ϕ of width n is satisfiable in an Aleksandrov tt-modelbased on a (finite) disjoint union of n-brooms iff ϕ†n is satisfiable in a first-order temporalmodel (with a finite domain) based on the same flow of time.
Proof. (⇒) Suppose that ϕ is satisfied in an Aleksandrov tt-model M = F, G, V , whereF = W, < , G = V, R is a disjoint union of n-brooms b = Wb, Rb , Wb = x0, x1, . . . , xn
b
b
b
and Rb is the reflexive closure of  x0, x1 , . . . , x0, xn  (see Fig. 11).
b
b
b
b
Construct a first-order temporal model N = F, D, I by taking D to be the set of all
db for n-brooms b in G and, for every w ∈ W ,
I(w)
I(w)
I(w)
I(w)
I(w) =
D, P
, . . . , P
, P
, . . . , P
, . . . ,
11
1n
21
2n
where for each spatial variable pj in ϕ and each i, 1 ≤ i ≤ n,
I(w)
P
= d
ji
b ∈ D | (M, w, xib ) |= pj .
10. For brevity, in this definition we follow the syntax of PT L × RC rather than PT L × RC−.
227

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Note that D is finite whenever G is finite.
Now, by induction on the construction of a spatio-temporal region term
of ϕ, it can
easily be shown that for every w ∈ W , every n-broom b in G and every i, 1 ≤ i ≤ n,
(N, w) |= ( )†in [db]
iff
(M, w, xib ) |= .
(58)
Next, (58) can be extended to arbitrary spatio-temporal terms τ of ϕ and i, 0 ≤ i ≤ n:
(N, w) |= (τ )†in [db]
iff
(M, w, xib ) |= τ.
(59)
The cases for i, 1 ≤ i ≤ n, trivially follow from (58) and the fact that leaves have nosuccessors but themselves. Consider now i = 0. The case τ =
holds simply because region
terms are interpreted by regular closed sets:
(M, w, x0b ) |=
iff
(M, w, xkb ) |= ,
for some k, 1 ≤ k ≤ n,
(60)
If τ = I then, on one hand,
(M, w, x0b ) |= I
iff
(M, w, xkb ) |= ,
for all k, 0 ≤ k ≤ n,
and on the other, by the definition of ·†0n ,
(N, w) |= (I )†0n [db]
iff
(N, w) |= ( )†kn [db],
for all k, 1 ≤ k ≤ n,
which together with (60) and IH yields (59). The cases of the Booleans are trivial.
Finally, we show that for every ψ ∈ sub ϕ, we have
(N, w) |= ψ†n
iff
(M, w) |= ψ.
Case ψ = 2
∀ τ :
(N, w) |= (2
∀ τ )†n
iff
∀db ∈ D ∀k ∈ 0, 1, . . . , n (N, w) |= (τ )†kn[db]
iff
∀b in G ∀k ∈ 0, 1, . . . , n (M, w, xkb ) |= τ
iff
(M, w) |= 2
∀ τ.
The remaining cases are trivial. It follows that ϕ†n is satisfied in N.
(⇐) Assume that ϕ† is satisfied in a first-order temporal model N = F, D, I , where
F = W, < and, for every w ∈ W ,
I(w)
I(w)
I(w)
I(w)
I(w) =
D, P
, . . . , P
, P
, . . . , P
, . . . .
11
1n
21
2n
With every point d ∈ D we associate an n-broom bd = Wb , R
so that the sets W ,
d
bd
bd
for d ∈ D, are pairwise disjoint and each contains n + 1 distinct elements x0 , . . . , xn .
bd
bd
Construct an Aleksandrov tt-model M = F, G, V by taking
• G to be the disjoint union of n-brooms bd | d ∈ D,
• V(pj, w) = xi
| (N, w) |= (CIp
b
j )†in [d],
0 ≤ i ≤ n and d ∈ D .
d
228

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Clearly, if D is finite then G is finite as well.
By a straightforward induction one can show that for all w ∈ W , d ∈ D, spatio-temporal
region terms , spatio-temporal terms τ , subformulas ψ of ϕ, and all i, 0 ≤ i ≤ n,
(N, w) |= ( )†in [d]
iff
(M, w, xib ) |=
(i > 0),
d
(N, w) |= (τ )†in [d]
iff
(M, w, xib ) |= τ,
d
(N, w) |= ψ†n
iff
(M, w) |= ψ.
For example,
(N, w) |= (I )†0n [d]
iff
(N, w) |= ( )†kn [d], for all k, 0 ≤ k ≤ n
iff
(M, w, xkb ) |= , for all k, 0 ≤ k ≤ n
d
iff
(M, w, x0b ) |= I .
d
It follows that ϕ is satisfied in M.
K
Now we obtain the upper complexity bounds for combinations of PT L and RC−:
Proof of Theorem 3.11, upper bound. Follows from Lemmas C.2 (ii) and C.5 togetherwith the results on the complexity of the one-variable fragment of QT L (Halpern & Vardi,1989; Sistla & German, 1987; Hodkinson et al., 2000, 2003).
K
Proof of Theorem 3.12, upper bound. Similar to the proof above.
K
Proof of Theorem 3.15, upper bound. The proof follows from Lemmas C.2 (i) and C.5together with the upper complexity bound of the guarded monodic (and so the one-variable)fragment of QT L (Hodkinson, 2004).
K
C.4 Lower Complexity Bounds (II): Embedding First-Order Temporal Logic
We are now in a position to prove Theorem 3.14 and establish the lower complexity boundsfor spatio-temporal logics based on BRCC-8 (and so for those based on RC− as well). Denoteby QT L12 the one-variable fragment of QT L with sole temporal operator 2F . We define apolynomial embedding of QT L12 into PT L2 × BRCC-8. Note that a similar embedding ofthe full one-variable fragment QT L1 into PT L × BRCC-8 can be regarded as an alternativeway to prove the lower complexity bound of Theorem 3.12.
A QT L12-formula is said to be a basic Q-formula if it is of the form ∀x ϑ(x), where
ϑ(x) is quantifier-free and contains no propositional variables. A QT L12-sentence ϕ is in Q-normal form if it is built from basic Q-formulas using the Booleans and temporal operator2F . In other words, sentences in Q-normal form do not contain nested quantifiers and useonly unary predicate symbols. The following observation should not come as a surprise (see,e.g., Hughes & Cresswell, 1996):
Lemma C.6. For every QT L12-sentence ϕ one can effectively construct a QT L12-sentenceϕ in Q-normal form such that ϕ is satisfiable in a first-order temporal model with a flow oftime F (and having finite domain) iff ϕ is satisfiable in a first-order temporal model basedon F (and having finite domain). Moreover, the length of ϕ is linear in the length of ϕ.
229

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Proof. Without loss of generality we may assume that ϕ contains no occurrences of ∃. Totransform ϕ into its Q-normal form, we first introduce a fresh unary predicate symbol Pi(x)for every propositional variable pi in ϕ and replace each occurrence of pi with ∀x Pi(x).Denote the resulting formula by ϕ0. For every subformula ψ of ϕ0 define a formula ψ bytaking inductively
(P (x)) = P (x),
(∀x ψ) = P∀xψ(x),
(¬ψ) = ¬ψ ,
(ψ1 ∧ ψ2) = ψ ∧ ψ ,
(2
1
2
F ψ) = 2F ψ ,
where P∀xψ(x) is a fresh unary predicate symbol. Let
ϕ = ¬∀x ¬ϕ
∧
2+ ∀x P
0
F
∀xψ (x) ∨ ∀x ¬P∀xψ (x)
∧
∀x P∀xψ(x) ↔ ∀x ψ
.
∀xψ∈subϕ0
One can readily show by induction that ϕ is satisfiable in a first-order temporal model basedon F (and having finite domain) iff ϕ is satisfiable in a first-order temporal model based onF (and having finite domain). Moreover, ϕ is in Q-normal form.
K
Now, given a QT L12-formula ϕ in Q-normal form, denote by ϕ∗ the result of replacing
all occurrences of basic Q-formulas ∀x ϑ(x) in ϕ with EQ(ϑ∗,
), where
is a region term
representing the whole space (for instance, CIu
CIu for a fresh spatial variable u), and
the translation ϑ∗ of quantifier-free formulas ϑ(x) is defined by taking:
(P (x))∗ = CIp,
(¬ψ)∗ = CI ψ∗ ,
(ψ1 ∧ ψ2)∗ = CI(ψ∗1
ψ∗2),
(2F ψ)∗ = CI2F ψ∗,
where P (x) is a unary predicate symbol and p a spatial variable standing for P (x). Clearly,ϕ∗ belongs to PT L2 × BRCC-8.
Lemma C.7. A QT L12-sentence ϕ in Q-normal form is satisfiable in a first-order temporalmodel based on a flow of time F and having finite domain iff ϕ∗ is satisfiable in a tt-modelbased on F and satisfying FSA.
Proof. (⇒) Suppose that ϕ is in Q-normal form and M = F, D, I is a first-order temporal
I(w)
model, where F = W, < and, for all w ∈ W , I(w) = D, P
, . . . , . Let (M, w
0
0) |= ϕ for
some w0 ∈ W . Construct an Aleksandrov tt-model M = F, G, V by taking G = D, R ,
I(w)
where R =  d, d | d ∈ D and V(pi, w) =
w, d | d ∈ P
. Note that the topological
i
space TG = D, IG induced by G is discrete, i.e., for all X ⊆ D,
IGX = CGX = X.
It follows by induction that for every quantifier-free QT L12-formula ϑ, every w ∈ W andevery d ∈ D we have
(M, w) |= ϑ[d]
iff
(M , w, d ) |= ϑ∗.
Therefore, for every basic Q-formula ∀x ϑ(x) and every w ∈ W , (M, w) |= ∀x ϑ(x) iff(M , w) |= EQ(ϑ∗,
). It follows by induction that (M , w0) |= ϕ∗.
230

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
(⇐) Suppose that ϕ∗ is satisfied in a tt-model based on F = W, < . By Lemma C.1 (i),
ϕ∗ is satisfied in an Aleksandrov tt-model M = F, G, V , where G = V, R is a disjointunion of brooms. Denote by V0 ⊆ V the set of leaves of G and define a first-order temporalmodel M = F, V0, I by taking, for each w ∈ W ,
I(w)
I(w)
I(w) = V0, P
, . . .
and
P
= V(p
0
i
i, w) ∩ V0.
Clearly, for every X ⊆ V , we have IGX ∩ V0 = CGX ∩ V0 = X ∩ V0, where TG = V, IG isthe topological space induced by G. So we obtain by induction that for every quantifier-freeQT L12-formula ϑ, all w ∈ W and all d ∈ V0
(M , w) |= ϑ[d]
iff
(M, w, d ) |= ϑ∗.
A regular closed set X ⊆ V in TG coincides with V iff it contains V0. So, for all basicQ-formulas ∀x ϑ(x) and all w ∈ W , (M , w) |= ∀x ϑ(x) iff (M, w) |= EQ(ϑ∗,
). It follows
by induction that ϕ is satisfied in M .
K
Proof of Theorem 3.14, lower bound. By Lemmas C.6 and C.7 the satisfiability prob-lem for QT L12-formulas in first-order temporal models with finite domains and based on
N, < ,
Z, <
or arbitrary finite flows of time is polynomially reducible to satisfiabil-
ity of PT L2 × BRCC-8 formulas in tt-models with FSA. Since the former is known tobe EXPSPACE-hard (Hodkinson et al., 2003) for
N, <
and
Z, < , the latter is also
EXPSPACE-hard in these cases. It should be noted that the result of Hodkinson andhis colleagues (2003) can readily be extended to the case of arbitrary finite flows of time(by reduction of a finite version of the corridor tiling problem). This gives us the lowercomplexity bound for PT L2 × BRCC-8 in the case of finite flows of time.
K
C.5 PSPACE-complete Spatio-Temporal Logic
In this appendix we prove Theorem 3.8. In fact, we show that the satisfiability problem forPT L ◦ RC2—an extension of PT L ◦ RCC-8—is decidable in PSPACE, where RC2 is thesublanguage of S4u with spatial terms τ restricted to the following:
::=
CIp,
σ
::=
|
I ,
δ
::=
I
|
,
τ
::=
σ1
σ2
|
δ1
δ2
|
σ
δ.
As before, we denote by σ spatial terms representing regular closed sets (regions) and byδ those representing regular open sets (the interiors of regions). Clearly, this definition isequivalent to the definition on p. 190 (where we did not make an explicit distinction betweenσ and δ). It is easy to see that RC2 contains RCC-8, but is less expressive than BRCC-8.Spatio-temporal terms τ of PT L ◦ RC2 are constructed from region terms of the form
::=
CIp
|
CI
in the same way as spatial terms of RC2. Finally, PT L ◦ RC2-formulas are composed fromatomic formulas of the form 2
∀ τ using the Booleans and the temporal operators.
231

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
We will reduce the satisfiability problem for PT L◦RC2 to that for PT L. This reduction
will be done in a number steps.
Let F =
W, < be a flow of time (as in the formulation of Theorem 3.8) and ϕ a
PT L ◦ RC2-formula. We begin by removing the next-time operator from the subterms of ϕ.To this end, let ψ0 = ϕ and for each variable p from the set
Ω1
=
p | CI CIp ∈ term ψ0,
we introduce a fresh spatial variable p , and then put
ϕ1
=
ψ1
∧
2+2+
→ 2∀(CI CIp ≡ CIp ) ,
P
F
p∈Ω1
where ψ1 is the result of replacing each occurrence of CI CIp in ψ0 with CIp and2∀( 1 ≡ 2) stands for 2∀( 1
2) ∧ 2
∀ ( 1
2). Next, for each p from
Ω2
=
p | CI CIp ∈ term ψ1,
we introduce a fresh spatial variable p , and set
ϕ2
=
ψ2
∧
2+2+
→ 2∀(CI CIp ≡ CIp ) ,
P
F
p∈Ω1∪Ω2
where ψ2 is the result of replacing each occurrence of CI CIp in ψ1 with CIp . By repeatingthis process sufficiently many times we can obtain a formula
ϕ
=
ψϕ
∧
2+2+
→ 2∀(CI CIp ≡ CIp ) ,
(61)
P
F
p∈Ωϕ
where Ωϕ is a suitable set of spatial variables, and ψϕ contains no
in region terms, that
is, ψϕ is a PT L[RC2]-formula. (Note that Ωϕ is such that if a spatial variable p occurs inψϕ then either CI CIp /
∈ term ϕ or p ∈ Ωϕ.) It should be clear that the length of ϕ is
linear in the length of ϕ, and ϕ is satisfiable in a tt-model based on F iff ϕ is satisfiable ina tt-model based on F.
Thus, it suffices to reduce the satisfiability problem for PT L ◦ RC2-formulas of the
form (61) to the satisfiability problem for PT L-formulas. Let us now recall the function·∗ from Appendix B.1 which maps PT L[S4u]-formulas (in particular, PT L[RC2]-formulas)to PT L-formulas. Namely, for every atomic RC2-formula 2
∀ τ , let (2
∀ τ )∗ = pτ , where pτ is
a fresh propositional variable. Then, given the PT L[RC2]-formula ψϕ, define ψ∗ϕ to be theresult of replacing every occurrence of 2
∀ τ in it with (2
∀ τ )∗. As is shown in the proof of
Theorem 3.1, ψϕ is satisfiable in a tt-model over F = W, < iff
(s1) there exists a temporal model N = F, U satisfying ψ∗ϕ and,
(s2) for every w ∈ W , the set
Φw = 2
∀ τ | (N, w) |= pτ , τ ∈ term ψϕ ∪ ¬2
∀ τ | (N, w) |= ¬pτ , τ ∈ term ψϕ (62)
of RC2-formulas is satisfiable.
232

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
To preserve satisfiability of not only ψϕ but the whole ϕ, we have to ensure somehow that
(s3) the points satisfying Φw do have predecessors and successors satisfying Φw−1 and
Φw+1, respectively.
In the remainder of the appendix we first describe an encoding of the satisfiability
problem for sets of RC2-formulas of the form (62) in Boolean logic, which will be used aspart of our final reduction. Then we prove a completion property of RC2 (cf. Balbiani &Condotta, 2002) in the class of exhaustive models that contain ‘sufficiently many’ points ofevery type. Roughly, the completion property says that, given a set Φ of the form (62) andan exhaustive model satisfying some subset of Φ, one can extend the valuation of the modelto satisfy the whole Φ. This property will make it possible to solve problem (s3) above. It isworth noting that a similar construction works for stronger languages such as BRCC-8, butthen, to enjoy the completion property, sets (62) may need exponentially many formulas (inthe number of spatial variables) and, therefore, the reduction to PT L will be exponentialas well. For RC2 it suffices to consider sets (62) with a quadratic number of formulas, whichresults in a quadratic reduction.
C.5.1 Properties of RC2-formulas
For any finite set Ω = p1, . . . , pn of spatial variables, let
AtFmΩ
=
2∀τ | τ is an RC2-term with variables from Ω .
Clearly, every RC2-formula with spatial variables from Ω is a Boolean combination of spatialformulas from AtFmΩ. It should be also clear that |AtFmΩ| ≤ 16 · |Ω|2.
As the width of RC2-formulas is ≤ 2 (see p. 209 for the definition), by Lemmas A.1 and
C.2 (ii), an RC2-formula is satisfiable iff it is satisfiable in an Aleksandrov topological modelbased on a disjoint union of 2-brooms, alias forks. In what follows we will regard every suchmodel M as a disjoint union of fork models m = f, v , where f = W, R , W = x0, x1, x2,R is the reflexive closure of  x0, x1 , x0, x2  and v a valuation of the spatial variables.Given Ω0 ⊆ Ω, we say that fork models m1 = f, v1 and m2 = f, v2 are Ω0-equivalent andwrite m1 ∼Ω m
0
2, if v1(CIp) = v2(CIp) for every p ∈ Ω0.
Given some Φ ⊆ AtFmΩ and ψ ∈ AtFmΩ, we say that ψ is an f-consequence of Φ and
write Φ |=f ψ if m |= Φ implies m |= ψ for every fork model m based on f. Φ is said to beclosed (under f-consequences) if, for every ψ ∈ AtFmΩ, we have ψ ∈ Φ whenever Φ |=f ψ.Let Φc = ¬2
∀ τ | 2
∀ τ ∈ AtFmΩ − Φ . Then Φ ∪ Φc is satisfiable iff Φ is closed and satisfiable.
This means, in particular, that to check whether the set Φw in (62) is satisfiable, it is enoughto consider only the closure of 2
∀ τ | (N, w) |= pτ , τ ∈ term ψ.
Now we characterise |=f in terms of the Boolean consequence relation |=. As we know
from Appendix C.3, spatial formulas can be embedded into the one-variable fragment offirst-order logic.
More precisely, it can easily be shown that first-order translations of
formulas from AtFmΩ are (equivalent to) formulas of the form (which are actually Kromformulas; see, e.g., B¨
orger, Gr¨
adel, & Gurevich, 1997):
†1
†1
†2
†2
(2
∀ (σ
2
2
2
2
1
σ2))†2 = ∀x σ
∨ σ
∧ ∀x σ
∨ σ
,
(63)
1
2
1
2
†1
†1
†2
†2
(2
∀ (σ
2
2
2
2
1
δ2))†2 = ∀x σ
∨ δ
∧ ∀x σ
∨ δ
,
(64)
1
2
1
2
233

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
†1
†1
†1
†2
†2
†1
†2
†2
(2
∀ (δ
2
2
2
2
2
2
2
2
1
δ2))†2 = ∀x δ
∨ δ
∧ ∀x δ
∨ δ
∧ ∀x δ
∨ δ
∧ ∀x δ
∨ δ
, (65)
1
2
1
2
1
2
1
2
where
Pji(x),
if σ = CIpj,
Pji(x),
if δ = ICIpj,
σ†i2 =
and
δ†i2 =
for
i = 1, 2.
¬Pji(x), if σ = ICIpj
¬Pji(x), if δ = CIpj,
It follows from the proof of Lemma C.5 that an RC2-formula ψ is satisfied in an Aleksandrovmodel M based on a disjoint union of forks iff its first-order translation ψ†2 is satisfied ina first-order model where every fork f = W, R of M, W = x0, x1, x2 , x0Rx1 and x0Rx2,is encoded by a domain element df with Pji(x) being true on df iff (M, xi) |= CIpj, fori = 1, 2 (see Fig. 11). Since in the definition of closed sets we only consider Aleksandrovmodels based on a single fork f, the domains of respective first-order models contain a singleelement df. This means that (63)–(65) can be encoded by the Boolean formulas
(2
∀ (σ1
σ2))‡ = σ‡1 ∨ σ‡1
∧
σ‡2 ∨ σ‡2 ,
1
2
1
2
(2
∀ (σ1
δ2))‡ = σ‡1 ∨ δ‡1
∧
σ‡2 ∨ δ‡2 ,
1
2
1
2
(2
∀ (δ1
δ2))‡ = δ‡1 ∨ δ‡1
∧
δ‡1 ∨ δ‡2
∧
δ‡2 ∨ δ‡1
∧
δ‡2 ∨ δ‡2 ,
1
2
1
2
1
2
1
2
where
qji,
if σ = CIpj,
qji,
if δ = ICIpj,
σ‡i =
and
δ‡i =
for
i = 1, 2.
¬qji, if σ = ICIpj
¬qji, if δ = CIpj,
Thus, with every Φ ⊆ AtFmΩ we can associate the conjunction Φ‡ of the ·‡-translations offormulas in Φ such that the following holds:
Claim C.8. For every ψ ∈ AtFmΩ, Φ |=f ψ
iff
Φ‡ |= ψ‡.
To construct the closure of Φ ⊆ AtFmΩ and to check whether Φ is satisfiable, we can
use the following resolution-like inference rules:
2∀(σ1
)
2∀(I
σ2)
2∀(I
δ1)
2∀(
δ1)
(σσ)
(σδ)
(σδ)
2
1
2
∀ (σ1
σ2)
2∀(
δ1)
2∀(I
δ1)

2
θ = ,
θ = I ;
∀
2∀
2∀(δ1 θ)
2∀(θ
δ2)


(⊥)
(δδ)
for
θ = ,
θ = ;
⊥
2∀(δ1 δ2)

θ = I ,
θ = I ;
together with the equivalences:
2∀ = 2∀I ,
2∀ = 2∀I ,
2∀(
σ1) = 2
∀ (I
σ1),
2∀(
σ1) = 2
∀ (I
σ1),
where
= CIp for some p ∈ Ω, σ1 and σ2 are of the form
or I , and δ1 and δ2 of the form
I or . It is readily checked that the above rules are sound, and so if ⊥ is derivable from Φ,then Φ is not satisfiable. On the other hand, if Φ is not satisfiable then Φ‡ can be regarded
234

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
as an unsatisfiable set of binary and unary propositional clauses and, using the standardresolution procedure, one can construct a derivation of the empty clause from Φ‡—which,in turn, can be mimicked by applications of the above rules (and equivalences) to derive⊥ from Φ. Moreover, since the propositional resolution is subsumption complete (see, e.g.,Slagle, Chang, & Lee, 1969), we can also derive all consequences of Φ, thereby obtaining itsclosure.
Now we encode the above rules and equivalences as Boolean formulas with variables pτ ,
for 2
∀ τ ∈ AtFmΩ. For instance, (⊥) and (σσ) are encoded by
2
∗
∗
∀
∧ 2∀
→ ⊥
and
2∀(σ1
) ∧ 2
∀ (I
σ2) → 2
∀ (σ1
σ2) ,
respectively. Denote by ΓΩ the conjunction of all such formulas for spatial variables fromΩ. Then we have the following:
Claim C.9. For every Φ ⊆ AtFmΩ, Φ is closed and satisfiable iff the Boolean formula
ΓΩ
∧
p
∧
¬
τ
pτ
(66)
2∀τ∈Φ
2∀τ∈AtFmΩ−Φ
is satisfiable.
Finally, to ensure (s3), we need the following completion property of RC2:
Lemma C.10. Let Φ be a closed subset of AtFmΩ, Ω0 ⊆ Ω and Φ0 = Φ ∩ AtFmΩ . Then
0
(i) Φ0 is closed and (ii) for every fork model m0, if m0 |= Φ0 then there is a fork model msuch that m0 ∼Ω m and m |= Φ.
0
Proof. Claim (i) is clear. To show (ii), we define the characteristic formula χ of m0 on Ω0by taking:
¬qji, if (m0, xi) |= CIpj,
χ
=
l∗ji
and
l∗ji =
q
p
ji,
if (m0, xi) |= CIpj.
j ∈Ω0, i=1,2
If m0 |= Φ0 then it follows immediately from the definitions that Φ‡ ∧ χ is satisfiable. Our
0
aim is to show that Φ‡ ∧ χ is also satisfiable, which would mean that there is a fork modelm as required. Suppose otherwise. Then Φ‡ |= ¬χ. We can regard Φ‡ as a set of unary andbinary clauses and ¬χ as a clause with 2 · |Ω0| literals lji, the negations of the l∗ . According
ji
to the subsumption theorem (Slagle et al., 1969), by applying the standard resolution ruleto Φ‡, we can derive a clause lj
∨ l
which subsumes ¬χ (i.e., its both literals occur in
1i1
j2i2
¬χ). Since Φ is closed, we have lj
∨ l
among the clauses of Φ‡ and as the l
are the
1i1
j2i2
jkik
·‡ik -translations of spatial terms for spatial variables from Ω0, we conclude that lj
∨ l
1i1
j2i2
is indeed among the clauses of Φ‡ , contrary to Φ‡ ∧ χ being satisfiable.
0
0
K
C.5.2 The Polynomial Translation of PT L ◦ RC2 into PT L
Now we are in a position to define a polynomial (at most quadratic) translation ·• ofPT L ◦ RC2 into PT L. Starting with a given formula ϕ, we construct the PT L ◦ RC2-formula ϕ of the form (61):
ϕ
=
ψϕ
∧
2+2+
→ 2∀(CI CIp ≡ CIp ) ,
P
F
p∈Ωϕ
235

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
where ψϕ is a PT L[RC2]-formula. Let Ωϕ = p | p ∈ Ωϕ and let Ω denote the smallestset of spatial variables containing Ωϕ ∪ Ωϕ and all spatial variables occurring in ψϕ. Given2∀τ ∈ AtFmΩ , denote by 2∀τ the formula from AtFm
obtained from 2
∀ τ by replacing
ϕ
Ωϕ
every occurrence of p ∈ Ωϕ with p ∈ Ωϕ. Consider the PT L-formula
ϕ•
=
ψ∗
∧
2+2+
2+
→
ϕ
Γ
( 2
∀ τ ↔ 2
∀ τ )∗ .
P
F
Ω
∧
2+P F
2∀τ∈AtFmΩϕ
Lemma C.11. For every PT L ◦ RC2-formula ϕ, ϕ is satisfiable in a tt-model based onF = W, < iff ϕ• is satisfiable in a temporal model based on F.
Proof. (⇒) Let (M, w0) |= ϕ. Construct a temporal model N = F, V by taking, for2∀τ ∈ AtFmΩ,
V(pτ ) = w ∈ W | (M, w) |= 2
∀ τ .
It is easy to see that (N, w0) |= ϕ•.
(⇐) Let (N, w0) |= ϕ• for some w0 ∈ W . For every w ∈ W , set
Φw = 2
∀ τ ∈ AtFmΩ | (N, w) |= p 
τ .
Let Λw, for w ∈ W , be a set of all non-Ω-equivalent fork models m with m |= Φw. ByClaim C.9, the Φw are closed and satisfiable, so the sets Λw are nonempty. We use theelements of the Λw as building blocks for exhaustive states in the tt-model we are going toconstruct in order to satisfy ϕ.
First we show that each element of Λw has a successor in Λw+1 and a predecessor in
Λw−1 (provided that w has a successor and predecessor, respectively). More precisely, wesay that a pair of fork models m = f, v and m = f, v
is suitable and write m → m if
v(CIp ) = v (CIp), for every p ∈ Ωϕ.
(succ)
Let m ∈ Λw, m = f, v , and let w ∈ W have a successor w + 1. By the third
conjunct of ϕ•, we have
Φw ∩ AtFmΩ
=
2∀τ ∈ AtFm
| (N, w) |= p 
ϕ
Ωϕ
τ
=
2∀τ ∈ AtFmΩ
| (N, w + 1) |= p .
ϕ
τ
Therefore,
Φw+1 ∩ AtFmΩ
=
2∀τ ∈ AtFm
| (N, w) |= p .
ϕ
Ωϕ
τ
Now, by m ∈ Λw, we have m |= Φw ∩ AtFmΩ . So if we define a fork model m = f, v by
ϕ
taking v (p) = v(p ), for all p ∈ Ωϕ (and arbitrary otherwise), then m |= Φw+1 ∩ AtFmΩϕfollows. Since Φw+1 is closed, by Lemma C.10, we can find a fork model m = f, v
such
that m ∼Ω m and m |= Φ
ϕ
w+1. It follows that m → m
and m is Ω-equivalent to some
fork model in Λw+1 (i.e., we may assume that m ∈ Λw+1).
(pred )
Similarly, for every m ∈ Λm, m = f, v , and every w ∈ W with a predecessor
w − 1, there is m = f, v
such that m ∈ Λw−1 and m → m.
It should be clear that for every fork model m ∈ Λw and every w ∈ W , we can define a
function rm,w that gives for each u ∈ W a fork model rm,w(u) ∈ Λu such that rm,w(w) = m
236

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
and rm,w(u) → rm,w(u + 1), whenever u + 1 is a successor of u. Let ∆ be the set of all suchfunctions rm,w, for w ∈ W and m ∈ Λw.
We are now ready to define an Aleksandrov tt-model M = F, G, V satisfying ϕ. Let
G = W, R be a disjoint union of |∆|-many forks fr = Wr, Rr , Wr = x0

 
r , x1
r , x2
r , x0
r Rr x1
r
and x0
∈
r Rr x2
r , for each r ∈ ∆, and let V(p, w) = xir
W | (r(w), xir) |= CIp, for all p ∈ Ω
and w ∈ W . We show by induction on the construction of χ ∈ sub ψϕ that, for every w ∈ W ,
(M, w) |= χ
iff
(N, w) |= χ∗.
Case ψ = 2
∀ τ . Suppose that (M, w) |= 2
∀ τ but (N, w) |= pτ . Then 2
∀ τ /
∈ Φw and, since
Φw is closed (by Claim C.9 and ΓΩ being true at w), we have Φw |=f 2
∀ τ . It follows that
there is a fork model m ∈ Λw with m |= ¬2
∀ τ , and so there is r ∈ ∆ such that r(w) = m,
contrary to (M, w) |= 2
∀ τ . Conversely, if (N, w) |= pτ then, by construction, (M, w) |= 2
∀ τ .
The cases of the Booleans and temporal operators are trivial.As the second conjunct of ϕ is satisfied by construction, we obtain (M, w0) |= ϕ.
K
References
Aiello, M., & van Benthem, J. (2002a). Logical patterns in space. In Barker-Plummer,
D., Beaver, D. I., van Benthem, J., & Scotto di Luzio, P. (Eds.), Words, Proofs andDiagrams, pp. 5–25. CSLI Publications, Stanford.
Aiello, M., & van Benthem, J. (2002b). A modal walk through space. Journal of Applied
Non-Classical Logics, 12 (3–4), 319–364.
Alexandroff, P. (1937). Diskrete R¨
aume. Matematicheskii Sbornik, 2 (44), 501–518.
Allen, J. (1983). Maintaining knowledge about temporal intervals. Communications of the
ACM, 26, 832–843.
Areces, C., Blackburn, P., & Marx, M. (2000). The computational complexity of hybrid
temporal logics. Logic Journal of the IGPL, 8, 653–679.
Arhangel’skii, A., & Collins, P. (1995). On submaximal spaces. Topology and its Applica-
tions, 64, 219–241.
Asher, N., & Vieu, L. (1995). Toward a geometry of common sense: A semantics and a
complete axiomatization of mereotopology. In Mellish, C. (Ed.), Proceedings of the14th International Joint Conference on Artificial Intelligence (IJCAI-95), pp. 846–852. Morgan Kaufmann.
Balbiani, P., & Condotta, J.-F. (2002). Computational complexity of propositional linear
temporal logics based on qualitative spatial or temporal reasoning. In Armando, A.(Ed.), Proceedings of Frontiers of Combining Systems (FroCoS 2002), Vol. 2309 ofLecture Notes in Computer Science, pp. 162–176. Springer.
Balbiani, P., Tinchev, T., & Vakarelov, D. (2004). Modal logics for region-based theories of
space. Manuscript.
Bennett, B. (1994). Spatial reasoning with propositional logic. In Proceedings of the 4th
International Conference on Knowledge Representation and Reasoning, pp. 51–62.Morgan Kaufmann.
237

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Bennett, B. (1996). Modal logics for qualitative spatial reasoning. Logic Journal of the
IGPL, 4, 23–45.
Bennett, B., & Cohn, A. (1999). Multi-dimensional multi-modal logics as a framework
for spatio-temporal reasoning. In Proceedings of the ‘Hot topics in Spatio-temporalreasoning’ workshop, IJCAI-99, Stockholm.
Bennett, B., Cohn, A., Wolter, F., & Zakharyschev, M. (2002). Multi-dimensional modal
logic as a framework for spatio-temporal reasoning. Applied Intelligence, 17, 239–251.
Blackburn, P. (1992). Fine grained theories of time. In Aurnague, M., Borillo, A., Borillo,
M., & Bras, M. (Eds.), Proceedings of the 4th European Workshop on Semantics ofTime, Space, and Movement and Spatio-Temporal Reasoning, pp. 299–320, Chˆ
ateau
de Bonas, France. Groupe “Langue, Raisonnement, Calcul”, Toulouse.
B¨
orger, E., Gr¨
adel, E., & Gurevich, Y. (1997). The Classical Decision Problem. Perspectives
in Mathematical Logic. Springer.
Bourbaki, N. (1966). General topology, Part 1. Hermann, Paris and Addison-Wesley.
Chagrov, A., & Zakharyaschev, M. (1997). Modal Logic, Vol. 35 of Oxford Logic Guides.
Clarendon Press, Oxford.
Chlebus, B. (1986). Domino-tiling games. Journal of Computer and System Sciences, 32,
374–392.
Clarke, B. (1981). A calculus of individuals based on ‘connection’. Notre Dame Journal of
Formal Logic, 23, 204–218.
Clarke, B. (1985). Individuals and points. Notre Dame Journal of Formal Logic, 26, 61–75.
Clarke, E., & Emerson, E. (1981). Design and synthesis of synchronisation skeletons using
branching time temporal logic. In Kozen, D. (Ed.), Logic of Programs, Vol. 131 ofLecture Notes in Computer Science, pp. 52–71. Springer.
Clementini, E., Di Felice, P., & Hern´
andez, D. (1997). Qualitative representation of posi-
tional information. Artificial Intelligence, 95, 317–356.
Cohn, A. (1997). Qualitative spatial representation and reasoning techniques. In Brewka,
G., Habel, C., & Nebel, B. (Eds.), KI-97: Advances in Artificial Intelligence, Vol. 1303of Lecture Notes in Computer Science, pp. 1–30. Springer.
Davis, E. (1990). Representations of Commonsense Knowledge. Morgan Kaufmann.
Degtyarev, A., Fisher, M., & Konev, B. (2003). Monodic temporal resolution. In Baader,
F. (Ed.), Proceedings of the 19th International Conference on Automated Deduc-tion (CADE-19), Vol. 2741 of Lecture Notes in Artificial Intelligence, pp. 397–411.Springer.
Demri, S., & D’Souza, D. (2002). An automata-theoretic approach to constraint LTL. In
Agrawal, M., & Seth, A. (Eds.), Proceedings of the 22nd Conference on Foundationsof Software Technology and Theoretical Computer Science (FST TCS 2002), Vol. 2556of Lecture Notes in Computer Science, pp. 121–132. Springer.
Egenhofer, M., & Franzosa, R. (1991). Point-set topological spatial relations. International
Journal of Geographical Information Systems, 5, 161–174.
238

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Egenhofer, M., & Herring, J. (1991). Categorizing topological relationships between regions,
lines and points in geographic databases. Tech. rep., University of Maine.
Egenhofer, M., & Sharma, J. (1993). Assessing the consistency of complete and incomplete
topological information. Geographical Systems, 1, 47–68.
Emerson, E., & Halpern, J. (1985). Decision procedures and expressiveness in the temporal
logic of branching time. Journal of Computer and System Sciences, 30, 1–24.
Fine, K. (1974). Logics containing K4, part I. Journal of Symbolic Logic, 39, 229–237.
Finger, M., & Gabbay, D. (1992). Adding a temporal dimension to a logic system. Journal
of Logic, Language and Information, 2, 203–233.
Fisher, M., Dixon, C., & Peim, M. (2001). Clausal temporal resolution. ACM Transactions
on Computational Logic (TOCL), 2, 12–56.
Gabbay, D., Hodkinson, I., & Reynolds, M. (1994). Temporal Logic: Mathematical Found-
ations and Computational Aspects, Volume 1. Oxford University Press.
Galton, A., & Meathrel, R. (1999). Qualitative outline theory. In Dean, T. (Ed.), Proceedings
of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99), pp.1061–1066. Morgan Kaufmann.
Gerevini, A., & Nebel, B. (2002). Qualitative spatio-temporal reasoning with RCC-8 and Al-
len’s interval calculus: Computational complexity. In Proceedings of the 15th EuropeanConference on Artificial Intelligence (ECAI’02), pp. 312–316. IOS Press.
Gerevini, A., & Renz, J. (2002). Combining topological and size constraints for spatial
reasoning. Artificial Intelligence, 137, 1–42.
G¨
odel, K. (1933). Eine Interpretation des intuitionistischen Aussagenkalk¨
uls. Ergebnisse
eines mathematischen Kolloquiums, 4, 39–40.
Goldblatt, R. (1976). Metamathematics of modal logic, Part I. Reports on Mathematical
Logic, 6, 41–78.
Goranko, V., & Passy, S. (1992). Using the universal modality: gains and questions. Journal
of Logic and Computation, 2, 5–30.
Gotts, N. (1996). An axiomatic approach to topology for spatial information systems. Tech.
rep. 96.25, School of Computer Studies, University of Leeds.
Halpern, J., & Shoham, Y. (1986). A propositional modal logic of time intervals. In Proceed-
ings of the 1st Annual IEEE Symposium on Logic in Computer Science (LICS’86),pp. 279–292. IEEE Computer Society.
Halpern, J., & Vardi, M. (1989). The complexity of reasoning about knowledge and time I:
lower bounds. Journal of Computer and System Sciences, 38, 195–237.
Hodkinson, I. (2004). Complexity of monodic packed fragment over linear and real time. To
appear in Annals of Pure and Applied Logic, available at http://www.doc.ic.ac.uk// imh/papers/cxmonlin.pdf.
Hodkinson, I., Kontchakov, R., Kurucz, A., Wolter, F., & Zakharyaschev, M. (2003). On
the computational complexity of decidable fragments of first-order linear temporal
239

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
logics. In Reynolds, M., & Sattar, A. (Eds.), Proceedings of TIME-ICTL 2003, pp.91–98. IEEE Computer Society.
Hodkinson, I., Wolter, F., & Zakharyaschev, M. (2000). Decidable fragments of first-order
temporal logics. Annals of Pure and Applied Logic, 106, 85–134.
Hodkinson, I., Wolter, F., & Zakharyaschev, M. (2001). Monodic fragments of first-order
temporal logics: 2000–2001 A.D. In Nieuwenhuis, R., & Voronkov, A. (Eds.), Logicfor Programming, Artificial Intelligence and Reasoning, Vol. 2250 of Lecture Notes inArtificial Intelligence, pp. 1–23. Springer.
Hodkinson, I., Wolter, F., & Zakharyaschev, M. (2002). Decidable and undecidable frag-
ments of first-order branching temporal logics. In Proceedings of the 17th AnnualIEEE Symposium on Logic in Computer Science (LICS 2002), pp. 393–402. IEEEComputer Society.
Hughes, G., & Cresswell, M. (1996). A New Introduction to Modal Logic. Methuen, London.
Hustadt, U., & Konev, B. (2003). TRP++ 2.0: A temporal resolution prover. In Baader,
F. (Ed.), Proceedings of the 19th International Conference on Automated Deduction(CADE-19), Vol. 2741 of Lecture Notes in Computer Science, pp. 274–278. Springer.
Kontchakov, R., Lutz, C., Wolter, F., & Zakharyaschev, M. (2004). Temporalising tableaux.
Studia Logica, 76, 91–134.
Kutz, O., Sturm, H., Suzuki, N.-Y., Wolter, F., & Zakharyaschev, M. (2003). Logics of
metric spaces. ACM Transactions on Computational Logic, 4, 260–294.
Ladner, R. (1977). The computational complexity of provability in systems of modal logic.
SIAM Journal on Computing, 6, 467–480.
Lemon, O., & Pratt, I. (1998). On the incompleteness of modal logics of space: advan-
cing complete modal logics of place. In Kracht, M., de Rijke, M., Wansing, H., &Zakharyaschev, M. (Eds.), Advances in Modal Logic, Volume 1, pp. 115–132. CSLIPublications, Stanford.
Lewis, C., & Langford, C. (1932). Symbolic Logic. Appleton-Century-Crofts, New York.
Ligozat, G. (1998). Reasoning about cardinal directions. Journal of Visual Languages and
Computing, 9, 23–44.
Manna, Z., & Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems.
Springer.
McKinsey, J. (1941). A solution of the decision problem for the Lewis systems S2 and S4,
with an application to topology. Journal of Symbolic Logic, 6, 117–134.
McKinsey, J., & Tarski, A. (1944). The algebra of topology. Annals of Mathematics, 45,
141–191.
Muller, P. (1998a). A qualitative theory of motion based on spatio-temporal primitives.
In Cohn, A., Schubert, L., & Shapiro, S. (Eds.), Proceedings of the 6th InternationalConference on Principles of Knowledge Representation and Reasoning (KR’98), pp.131–142. Morgan Kaufmann.
240

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
Muller, P. (1998b). Space-time as a primitive for space and motion. In Guarino, N. (Ed.),
Proceedings of the International Conference on Formal Ontology in Information Sys-tems (FOIS’98), Vol. 46 of Frontiers in Artificial Intelligence and Applications, pp.63–76. IOS Press.
Nebel, B., & B¨
urckert, H. (1995). Reasoning about relations: A maximal tractable subclass
of Allen’s interval algebra. Journal of the ACM, 42, 43–66.
Nebel, B. (1996). Artificial intelligence: A computational perspective. In Brewka, G. (Ed.),
Principles of Knowledge Representation, pp. 237–266. CSLI Publications.
Nutt, W. (1999). On the translation of qualitative spatial reasoning problems into modal
logics. In Burgard, W., Christaller, T., & Cremers, A. (Eds.), Advances in Artifi-cial Intelligence. Proceedings of the 23rd Annual German Conference on ArtificialIntelligence (KI’99), Vol. 1701 of Lecture Notes in Computer Science, pp. 113–124.Springer.
Ono, H., & Nakamura, A. (1980). On the size of refutation Kripke models for some linear
modal and tense logics. Studia Logica, 39, 325–333.
Orlov, I. (1928). The calculus of compatibility of propositions. Mathematics of the USSR,
Sbornik, 35, 263–286. (In Russian).
Post, E. (1946). A variant of a recursively unsolvable problem. Bulletin of the AMS, 52,
264–268.
Pratt-Hartmann, I. (2002). A topological constraint language with component counting.
Journal of Applied Non-Classical Logics, 12, 441–467.
Randell, D., Cui, Z., & Cohn, A. (1992). A spatial logic based on regions and connection.
In Nebel, B., Rich, C., & Swartout, W. (Eds.), Proceedings of the 3rd InternationalConference on Principles of Knowledge Representation and Reasoning (KR’92), pp.165–176. Morgan Kaufmann.
Renz, J. (1998). A canonical model of the region connection calculus. In Cohn, A., Schubert,
L., & Shapiro, S. (Eds.), Proceedings of the 6th International Conference on Prin-ciples of Knowledge Representation and Reasoning (KR’98), pp. 330–341. MorganKaufmann.
Renz, J., & Nebel, B. (1998). Spatial reasoning with topological information. In Freksa, C.,
Habel, C., & Wender, K. (Eds.), Spatial Cognition—An Interdisciplinary Approachto Representation and Processing of Spatial Knowledge, Vol. 1404 of Lecture Notes inComputer Science, pp. 351–372. Springer.
Renz, J., & Nebel, B. (1999). On the complexity of qualitative spatial reasoning. Artificial
Intelligence, 108, 69–123.
Renz, J. (2002). A canonical model of the region connection calculus. Journal of Applied
Non-Classical Logics, 12, 469–494.
Renz, J., & Nebel, B. (2001). Efficient methods for qualitative spatial reasoning. Journal
of Artificial Intelligence Research, 15, 289–318.
Reynolds, M. (2003). The complexity of the temporal logic with ‘until’ over general linear
time. Journal of Computer and System Science, 66, 393–426.
241

 
Gabelaia, Kontchakov, Kurucz, Wolter, & Zakharyaschev
Reynolds, M. (2004). The complexity of the temporal logic over the reals. Submitted,
available at http://www.csse.uwa.edu.au/ mark/research/Online/CORT.htm.
Schwendimann, S. (1998). A new one-pass tableau calculus for PLTL. In de Swart, H. (Ed.),
Proceedings of the International Conference on Automated Reasoning with AnalyticTableaux and Related Methods (TABLEAUX-98), Vol. 1397 of Lecture Notes in Arti-ficial Intelligence, pp. 277–291. Springer.
Sistla, A., & Clarke, E. (1985). The complexity of propositional linear temporal logics.
Journal of the Association for Computing Machinery, 32, 733–749.
Sistla, A., & German, S. (1987). Reasoning with many processes. In Proceedings of the
Second IEEE Symposium on Logic in Computer Science (LICS’87), pp. 138–153. IEEEComputer Society.
Slagle, J., Chang, C.-L., & Lee, R. (1969). Completeness theorems for semantic resolution
in consequence-finding. In Proceedings of the 1st International Joint Conference onArtificial Intelligence (IJCAI’69), pp. 281–286. William Kaufmann.
Smith, T., & Park, K. (1992). An algebraic approach to spatial reasoning. International
Journal of Geographical Information Systems, 6, 177–192.
Stockmeyer, L. (1974). The Complexity of Decision Problems in Automata Theory and
Logic. Ph.D. thesis, MIT.
Stockmeyer, L. (1987). Classifying the computational complexity of problems. Journal of
Symbolic Logic, 52, 1–43.
Stone, M. (1937). Application of the theory of Boolean rings to general topology. Transac-
tions of the AMS, 41, 321–364.
Tarski, A. (1938). Der Aussagenkalk¨
ul und die Topologie. Fundamenta Mathematicae, 31,
103–134.
Tsao Chen, T. (1938). Algebraic postulates and a geometric interpretation of the Lewis
calculus of strict implication. Bulletin of the AMS, 44, 737–744.
van Benthem, J. (1995). Temporal logic. In Gabbay, D., Hogger, C., & Robinson, J. (Eds.),
Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, pp. 241–350. Oxford Scientific Publishers.
van Emde Boas, P. (1997). The convenience of tilings. In Sorbi, A. (Ed.), Complexity, Logic
and Recursion Theory, Vol. 187 of Lecture Notes in Pure and Applied Mathematics,pp. 331–363. Marcel Dekker Inc.
Wolper, P. (1985). The tableau method for temporal logic: An overview. Logique et Analyse,
28, 119–152.
Wolter, F. (1996). Properties of tense logics. Mathematical Logic Quarterly, 42, 481–500.
Wolter, F., & Zakharyaschev, M. (2000a). Spatial reasoning in RCC-8 with Boolean region
terms. In Horn, W. (Ed.), Proceedings of the 14th European Conference on ArtificialIntelligence (ECAI 2000), pp. 244–248. IOS Press.
Wolter, F., & Zakharyaschev, M. (2000b). Spatio-temporal representation and reasoning
based on RCC-8. In Cohn, A., Giunchiglia, F., & Seltman, B. (Eds.), Proceedings of
242

 
Combining Spatial and Temporal Logics: Expressiveness vs. Complexity
the 7th Conference on Principles of Knowledge Representation and Reasoning (KR2000), pp. 3–14. Morgan Kaufmann.
Wolter, F., & Zakharyaschev, M. (2002). Qualitative spatio-temporal representation and
reasoning: a computational perspective. In Lakemeyer, G., & Nebel, B. (Eds.), Ex-ploring Artificial Intelligence in the New Millenium, pp. 175–216. Morgan Kaufmann.
Zimmermann, K. (1995). Measuring without measures: the delta-calculus. In Frank, A., &
Kuhn, W. (Eds.), Proceedings of the 2nd International Conference on Spatial Inform-ation Theory (COSIT), Vol. 988 of Lecture Notes in Computer Science, pp. 59–67.Springer.
243

 
Document Outline
1 Introduction
2 Propositional Logics of Space and Time
2.1 Logics of Space
2.1.1 S4u
2.1.2 RCC-8 as a Fragment of S4u
2.1.3 BRCC-8 as a Fragment of S4u
2.1.4 RC
2.1.5 RCmax
2.2 Temporal Logics
3 Combinations of Spatial and Temporal Logics
3.1 Spatio-Temporal Logics with (PC)
3.2 `Maximal' Combinations with (PC) and (OC)
3.3 Decidable Spatio-Temporal Logics with (PC) and (OC)
4 Conclusion
A Complexity of Spatial Logics
B Spatio-Temporal Logics Based on S4u
B.1 Temporalisations of S4u
B.2 Undecidability of PTLoS4u and PTLxS4u
C Spatio-Temporal Logics Based on RC
C.1 Lower Complexity Bounds (I)
C.2 Upper Complexity Bounds (I): Quasimodels for PTLxRC
C.3 Upper Complexity Bounds (II): Embedding into First-Order Temporal Logic
C.4 Lower Complexity Bounds (II): Embedding First-Order Temporal Logic
C.5 PSPACE-complete Spatio-Temporal Logic
C.5.1 Properties of RC2-formulas
C.5.2 The Polynomial Translation of PTLoRC2 into PTL
References