{'fraction_non_alphanumeric': 0.063899049012436, 'fraction_numerical': 0.01632528651548403, 'mean_word_length': 3.6180395248015316, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 60, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Spatial logics with connectedness predicates

We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, ExpTime and, if component counting is allowed, to NExpTime.


Introduction
The field of Artificial Intelligence known as qualitative spatial reasoning is concerned with the problem of representing and manipulating spatial information about everyday, middle-sized entities. In recent decades, much activity in this field has centred on spatial logics-formal languages whose variables range over geometrical objects (not necessarily points), and whose non-logical primitives represent geometrical relations and operations involving those objects. (For a recent survey, see [10].) The hope is that, by using a formalism couched entirely at the level of these geometrical objects, we can avoid the expressive-hence computationally expensive-logical machinery required to reconstruct them in terms of sets of points.
What might such qualitative spatial relations typically be? Probably the most intensively studied collection is the set of six topological relations illustrated-for the case of closed disc-homeomorphs in R 2 -in Fig. 1. These relations-DC (disconnection), EC (external connection), PO (partial overlap), EQ (equality), TPP (tangential proper part) and NTPP (non-tangential proper part)-were popularized in the seminal treatments of spatial Figure 1: The RCC-8-relations illustrated for disc-homeomorphs in R 2 the two asymmetric relations TPP and NTPP, the resulting eight relations are frequently referred to under the moniker RCC-8 (for region connection calculus). To see how this collection of relations gives rise to a spatial logic, let r 1 , r 2 and r 3 be disc-homeomorphs in R 2 , and suppose that r 1 , r 2 stand in the relation TPP, while r 1 , r 3 stand in the relation NTPP. A little experimenting with diagrams suffices to show that r 2 , r 3 must stand in one of the three relations PO, TPP or NTPP. As we might put it, the RCC-8-formula TPP(r 1 , r 2 ) ∧ NTPP(r 1 , r 3 ) → PO(r 2 , r 3 ) ∨ TPP(r 2 , r 3 ) ∨ NTPP(r 2 , r 3 ) is valid over the spatial domain of disc-homeomorphs in the plane: all assignments of such regions to the variables r 1 , r 2 and r 3 make it true. Similar experimentation shows that, by contrast, the formula TPP(r 1 , r 2 ) ∧ NTPP(r 1 , r 3 ) ∧ EC(r 2 , r 3 ), is unsatisfiable: no assignments of disc-homeomorphs to r 1 , r 2 and r 3 make this formula true.
More generally, let L be a formal language featuring some collection of predicates and function symbols having (fixed) interpretations as geometrical relations and operations. The formulas of L may then be interpreted over any collection of subsets of some space T for which the relevant geometrical notions make sense: we refer to the elements of such a domain of interpretation as regions. Let K be a class of domains of interpretation for L. The notion of the satisfaction of an L-formula by a tuple of regions, and, derivatively, the notions of satisfiability and validity of an L-formula with respect to K, can then be understood in the usual way. We call the pair (L, K) a spatial logic. If all the primitives of L are topological in character-as in the case of RCC-8-we speak of a topological logic. For languages featuring negation, the notions of satisfiability and validity are dual in the usual sense. The primary question arising in connection with any spatial logic is: how do we recognize the satisfiable (dually, the valid) formulas? From an algorithmic point of view, we are particularly concerned with the decidability and complexity of these problems.
A second example will make this abstract characterization more concrete. Constraints featuring RCC-8 predicates give us no means to combine regions into new ones; and it is natural to ask what happens when this facility is provided. Let T be a topological space. A subset of T is regular closed if it is the topological closure of an open set in T . The collection of regular closed sets forms a Boolean algebra with binary operations +, · and a unary operation −. Intuitively, we are to think of r 1 + r 2 as the agglomeration of r 1 and r 2 , r 1 · r 2 as the common part of r 1 and r 2 , and −r as the complement of r. Further, the RCC-8-relations illustrated above can be generalized, in a natural way, so that they apply to regular closed subsets of any topological space T . (Details are given below.) By augmenting the language RCC-8 with the function symbols +, · and −, we obtain the more expressive formalism originally introduced in [57] under the name BRCC-8 (Boolean RCC-8), which we may interpret over any algebra of regular closed subsets of some topological space. Again, we can ask which of these formulas are satisfiable or valid over the class of domains in question. For instance, the formula EC(r 1 + r 2 , r 3 ) → EC(r 1 , r 3 ) ∨ EC(r 2 , r 3 ) , asserting that, if the sum of two regions r 1 and r 2 stands in the relation of external connection to a region r 3 , then one of the summands does as well, turns out to be valid; by contrast, the formula EC(r 1 , r 2 ) ∧ EC(r 1 , −r 2 ), asserting that r 1 is externally connected to both r 2 and its complement, is unsatisfiable.
Arguably, the topological primitive with the longest pedigree in the spatial logic literature is the relation now generally referred to as C (for contact). Intuitively, two regions are to be thought of as being in contact just in case they either overlap or have touching boundaries. This relation was originally introduced by Whitehead ( [56], pp. 294, ff.) under the name extensive connection, and formed the starting point for his region-based reconstruction of space. More recently, it has been studied within the framework of Boolean contact algebras [12,16]. It turns out that, in the presence of the operations +, · and −, all of the RCC-8-relations can be expressed in terms of the relations of equality and contact, and vice versa. Accordingly, and in order to unify these two lines of research, we shall denote the language BRCC-8 by C in this paper.
One familiar topological property that has been notable by its absence from the spatial logic literature, however, is connectedness (or, as it is occasionally called, 'self-connectedness' [6]). This lacuna is particularly surprising given the recognized significance of this concept in qualitative spatial reasoning [10]. The availability of connectedness as a primitive relation greatly expands the expressive power of topological logics, and in particular increases their sensitivity to the underlying domain of quantification. For example, let the connectedness predicate c be added to the language RCC-8, yielding the language RCC-8c; and consider the RCC-8c-formula 1≤i≤3 c(r i ) ∧ 1≤i<j≤3 EC(r i , r j ).
This formula states that regions r 1 , r 2 and r 3 are connected, and that any two of them touch at their boundaries without overlapping. It is easily seen to be satisfiable over the domain of regular closed sets in R 2 ; however, it is not satisfiable over the domain of regular closed sets in R. For a non-empty, regular closed subset of R is connected if and only if it is a nonpunctual, closed interval (possibly unbounded); and it is obvious that no three such intervals can touch in pairs without overlapping. More tellingly, consider the RCC-8c-formula c(r 1 ) ∧ 1≤i<j≤4 EC(r i , r j ), stating that r 1 is connected, and that any two of r 1 , . . . , r 4 touch at their boundaries without overlapping. This formula is satisfiable over the regular closed subsets of R, as shown in Fig. 2. However, such an arrangement is only possible provided at least two of the regions c(r 1 ) ∧ 1≤i<j≤4 EC(r i , r j ): the region r 1 is connected, while r 2 , r 3 and r 4 have infinitely many components, with a common accumulation point on the boundary of the r 1 -region. r 2 , r 3 and r 4 have infinitely many components. If-for whatever reason-our spatial ontology does not countenance regions with infinitely many components, the formula becomes unsatisfiable. Thus, simple logics featuring the connectedness predicate are sensitive to the underlying topological space, and indeed to the choice of subsets of that space we count as regions. By contrast, we shall see below that topological logics lacking the connectedness predicate-even ones much more expressive than RCC-8-are remarkably insensitive to the spatial domains over which they are interpreted. More generally, the above examples give a hint of the interesting mathematical challenges which the property of connectedness presents us with in the context of almost any topological logic. It is surprising that only sporadic attempts have been made to investigate the expressive power and computational complexity of topological logics able to talk about the connectedness of regions [8,51,57,40]. The present paper rectifies this omission by introducing the unary predicates c and c ≤k (for k ≥ 1). We read c(r) as 'region r is connected' and c ≤k (r) as 'region r has at most k connected components.' Our aim is to provide a systematic study of the impact of these predicates on the computational complexity of the satisfiability problem for topological logics. We restrict attention in this paper to quantifier-free languages-i.e. those in which formulas are Boolean combinations of atomic formulas-in line with the constraint satisfaction approach of [47]-since first-order spatial logics are generally undecidable [27,14,11,36]. 1 For an overview of first-order topological logics, see [41].
Specifically, we consider three principal base languages, characterized by various collections of topological primitives, and investigate the effect of augmenting each of these base languages with the predicates c and c ≤k . The weakest of these base languages, denoted B, features only the region-combining operators +, · and −, together with the equality predicate. Thus, B is essentially just the language of Boolean algebra equations: as such, this language can express no really characteristic topological properties; further, its satisfiability problem, when interpreted over the class of regular closed algebras of topological spaces, is easily seen to be NP-complete. If, however, we add the connectedness predicate c, we obtain the language Bc-a fully-fledged topological logic able to simulate (in a sense explained below) the contact relation C, and hence all the RCC-8-relations. More ambitiously, we can Figure 3: (a) A closed set in the plane, (b) its interior and (c) the closure of its interior. Note that X • ⊆ X • − ⊆ X.

Background: topological logics without connectedness
A topological space is a pair (T, O), where T is a set and O a collection of subsets of T containing ∅ and T , and closed under arbitrary unions and finite intersections. The elements of O are referred to as open sets; their complements are closed sets. If O is clear from context, we refer to the topological space (T, O) simply as T . Given any X ⊆ T , the interior of X, denoted X • , is the largest open set included in X, and the closure of X, denoted X − , is the smallest closed set including X. These sets always exist. It is convenient, where the space T is clear from context, to denote T by 1, the empty set by 0, and, for any X ⊆ T , the complement T \ X by X. Evidently, Let T be a topological space. A subset of T is called regular closed if it is the closure of an open set. We denote the set of regular closed subsets of T by RC(T ). It is a standard result (for example, [31], pp. [25][26][27] that, for any topological space T , the collection of sets RC(T ) forms a Boolean algebra, with the top and bottom elements 1 = T and 0 = ∅, respectively, Boolean operations given by and Boolean order ≤ coinciding with the subset relation. In the context of the Euclidean plane R 2 , the regular closed sets are-roughly speaking-those closed sets with no 'filaments' or 'isolated points' (Fig. 3). When dealing with the Boolean algebra RC(T ), for some topological space T , we generally write X + Y in preference to X ∪ Y (though these are, formally, equivalent); similarly, we generally write X ≤ Y in preference to X ⊆ Y . We establish a general framework for defining the topological languages studied in this paper. Fix a countably infinite set R. We refer to the elements of R as region variables (or, more simply: variables) and denote them by r, s, etc. possibly with sub-or superscripts. Let F be any set of function symbols (of fixed arities) and P any set of predicate symbols (of fixed arities). In practice, the symbols in F and P may be assumed to have fixed topological interpretations, along the lines indicated in Section 1. For example, F might contain function symbols denoting the operations +, · and − on regular closed sets defined in (2.1); likewise, P might contain predicates denoting the RCC-8 relations. The L(F, P )terms, τ , are given by the rule: where r is a variable in R, f n a function symbol of arity n in F , and the τ i L(F, P )-terms. The L(F, P )-formulas, ϕ, are given by the rule: where p n is a predicate symbol of arity n in P , and ϕ 1 , ϕ 2 are L(F, P )-formulas. The topological language L(F, P ) is the set of L(F, P )-formulas. We shall write L in place of L(F, P ) if F and P are understood. As usual, formulas of the form p n (τ 1 , . . . , τ n ) and ¬p n (τ 1 , . . . , τ n ) are called literals. Notice that, for the purposes of this paper, topological languages involve no quantifiers. We now turn to the semantics of these languages. A topological frame is a pair of the form (T, S), where T is a topological space, and S ⊆ 2 T . We refer to the elements of S as regions; there is no requirement for S to be closed under any operations. A topological model on (T, S) is a triple M = (T, S, · M ), where · M is a map from R to S, referred to as a valuation. Assuming the function symbols in F and predicates in P to have standard interpretations, any topological model M determines the truth-value of an L-formula in the obvious way. We write M |= ϕ if the formula ϕ is true in M.
Let K be a class of topological frames and ϕ a formula of a topological language L. We say that ϕ is satisfiable over K if M |= ϕ for some topological frame (T, S) in K and some topological model M on (T, S); dually, ϕ is valid over K if M |= ϕ for every topological frame (T, S) in K and every topological model M on (T, S). As usual, ϕ is valid if and only if ¬ϕ is not satisfiable. The satisfiability problem for L-formulas over topological frames in K is the decision problem for the set that is: given an L-formula ϕ, decide whether it is satisfiable in a topological model based on a topological frame from K. A topological logic is a pair (L, K), where L is a topological language (whose primitives are taken to have fixed topological interpretations) and K a class of topological frames.
In the sequel, except where indicated to the contrary, we generally speak of frames, models, logics etc., taking the qualifier 'topological' to be implicit.
The primary motivation for introducing the notion of a frame (T, S) is to provide a mechanism for confining attention to those subsets S of the space T which we regard as bona fide regions. For example, it is frequently observed (see, e.g., [22]) that no clear sense can be given to the question of whether a given physical object occupies a topologically closed, semi-closed or open region of space. Consequently, spatial logics in AI conventionally identify regions differing only with respect to boundary points. A convenient way to finesse the issue of boundary points in a topological space T is to restrict attention to the regular closed sets RC(T ). For, given any closed subset X of T , there exists a unique Y ∈ RC(T ) such that X • ⊆ Y ⊆ X (see Fig. 3). Moreover, these regular closed sets, as noted above, form a Boolean algebra with +, · and − providing reasonable reconstructions of the intuitive operations of agglomeration, intersection, and complementation, respectively. In this paper, we shall be principally concerned with the classes of frames All and RegC given by One word of caution: the Boolean algebras RC(R 2 ) and RC(R 3 ) include many sets which are not at all obviously suited to model regions occupied by physical objects. For this reason, we may decide to interpret our languages over topological frames (T, S) where S is a sub-algebra of RC(T ), a restriction which turns out to have interesting mathematical consequences (see, e.g., [41]). With these semantic preliminaries behind us, we now survey some of the most familiar topological logics occurring in the AI literature. This survey will occupy the remainder of this section. Remember: our aim in the sequel is to investigate the effect of increasing the expressive resources available to these logics by adding predicates expressing connectedness and related notions.
The logic RCC-8: We begin with a formal account of the topological language RCC-8, which we encountered in Section 1. As a preliminary, we define the following six binary relations on RC(T ), where T is any topological space: All of these relations except TPP and NTPP are symmetric. Counting the converses of TPP and NTPP, we thus obtain eight binary relations altogether: these eight relations are easily seen to be jointly exhaustive and mutually exclusive over non-empty elements of RC(T ). In Fig. 1, we illustrated them in the special case where the relata are closed disc-homeomorphs in the plane. We remark in passing that, when restricted to closed disc-homeomorphs in the plane, these relations are actually the atoms of a finite relation algebra [15,35].
We now define the language RCC-8 by with the symbols DC, EC, PO, EQ, TPP, NTPP taken to be binary predicates. There are no function symbols; so RCC-8-terms are simply variables. We always interpret this language over (some sub-class of) RegC-that is: variables are always taken to range over (certain) regular closed sets of (certain) topological spaces. The semantics for RCC-8 may then be given by specifying the interpretations of the predicates in obvious way, thus: Note the overloading of the symbols DC, EC, etc. here: on the left-hand sides of these equations, they are predicates of RCC-8; on the right-hand side, they denote the relations on RC(T ) defined in (2.2). Since these predicates will always be used with their standard meanings, no confusion need arise. In the literature, the language RCC-8 is sometimes subject to the additional restriction that variables range only over non-empty regular closed subsets of the space in question. We do not impose this requirement, remarking, however, that non-emptiness is anyway expressible in RCC-8 (on our interpretation) by adding conjuncts of the form ¬DC(r, r).
It is known that Sat(RCC-8, RegC) is NP-complete [43]. (Proofs of all the complexity results mentioned in this section are discussed in Section 4.) The logic BRCC-8: Since, as we have observed, the regular closed subsets of a topological space form a Boolean algebra, it makes sense to augment RCC-8 with function symbols denoting the obvious operations and constants of this Boolean algebra. The language BRCC-8 (for Boolean RCC-8, [57]) is defined by: where the function symbols + and · are binary, − is unary, and 0 and 1 are nullary (i.e. individual constants). Again, we confine attention to the class of frames RegC, with the function symbols interpreted as the obvious operations on regular closed sets. Formally: Note the overloading of the symbols: on the left-hand side of these equations, they are function symbols of BRCC-8; on the right-hand side, they denote the corresponding Boolean algebra operations in RC(T ) as defined in (2.1). The predicates are interpreted in the same way as for RCC-8.
Despite its increased expressive power, BRCC-8 is in the same complexity class as RCC-8-at least when interpreted over arbitrary topological spaces. That is: the problem Sat(BRCC-8, RegC) is NP-complete [57]. (However, as we shall see below, this situation changes even under very mild restrictions on the class of frames.) The logic C: We can re-formulate BRCC-8 more elegantly using the binary predicates = (equality) and C (contact). The language C is defined by: As with RCC-8 and BRCC-8, we confine our attention to the class of frames RegC. The equality predicate = denotes identity (as usual), and the contact predicate C is interpreted as follows: That is: two regions are taken to be in contact just in case they intersect. Notice that C(τ 1 , τ 2 ) is not equivalent to the condition τ 1 · τ 2 = 0 (a shorthand for ¬(τ 1 · τ 2 = 0)), which states that the interiors of τ 1 and τ 2 intersect. In the context of any logic involving the function symbols +, ·, −, 0, 1 and the equality predicate, we standardly write τ 1 ≤ τ 2 as an abbreviation for τ 1 · (−τ 2 ) = 0; ¬(τ 1 ≤ τ 2 ) is abbreviated by τ 1 τ 2 .
Evidently, C(τ 1 , τ 2 ) is equivalent to ¬DC(τ 1 , τ 2 ), and = is just another symbol for EQ; hence, BRCC-8 is at least as expressive as C. Conversely, it is easy to verify that the four remaining RCC-8-relations can easily be equivalently expressed in C, as follows: Hence, we may regard the languages C and BRCC-8 as equivalent.
The predicate C has an interesting history. Originally introduced by Whitehead [56] under the name 'extensive connection,' it provided the inspiration for many of the early approaches to topological logics in AI. To avoid confusion with the familiar topological property of connectedness, Whitehead's relation is now generally referred to as contact. Investigation of the contact-structure of the regular closed algebras of topological spaces gave rise to the study of so-called Boolean connection algebras (BCAs). The relationship between BCAs and the topological spaces that generate them is now well-understood [49,16,12,13]. Our logic C (that is: BRCC-8) is, in essence, the quantifier-free fragment of the first-order theory of BCAs. For an up-to-date account of this work, see [3].
The logic C m : As formulas in C are built from C-terms using the binary predicates τ 1 = τ 2 and C(τ 1 , τ 2 ), they are not capable of expressing, for example, the predicate EC 3 (τ 1 , τ 2 , τ 3 ) stating that three regions τ 1 , τ 2 , τ 3 are externally connected and have some common border. One way to extend the expressive power of C is to generalize the contact predicate and consider its extension C m with arbitrary k-ary contact relations C k (τ 1 , . . . , τ k ), for k ≥ 2. The language C m is defined by: Again, we confine attention to the class of frames RegC. The predicates C k are interpreted as follows: The ternary predicate EC 3 (τ 1 , τ 2 , τ 3 ) above can now be expressed in a straightforward way: which is not expressible in C. Obviously, the predicates C and C 2 have identical semantics; thus, C is a sub-language of C m . Again, the increased expressive power makes no difference to the complexity class: Sat(C m , RegC) is still NP-complete [21].
The logic B: We mention at this point a sub-language of C so inexpressive that no distinctively topological facts can be expressed in it, but which will nevertheless prove significant in the sequel. The language B, again interpreted over sub-classes of RegC, is defined by: Thus, B is the language of the variety of Boolean algebras. In the present context, it can be seen as capturing the essential content of mereology-the logic of 'part-whole' relations. (For a discussion of the relationship between mereology and Boolean algebra, see [53,28].) Trivially, Sat(B, RegC) is NP-complete.
The logic S4 u : Returning to matters topological, we come to the most expressive topological logic to have been considered in the literature. The language S4 u is defined by: and we write τ 1 ⊆ τ 2 as an abbreviation for τ 1 ∩ τ 2 = 0. We interpret the terms of this language as follows: where M is a model over some frame (T, S). As before, we have deliberately equivocated between function symbols in our formal language and the operations they denote. Since these operations do not in general preserve the property of being regular closed, it is unnatural to confine attention to the frame class RegC. Accordingly, we standardly interpret S4 u over the class All of all frames.
The richer term-language of S4 u means that, even though = is the only predicate, we are still able to formulate distinctively topological (not just mereological) statements. Consider, for example, the formula This formula states that, if an open set r • 1 intersects the closure of a set r 2 , then it also intersects r 2 . Thus, it is valid over the class of frames All.
The language S4 u may be regarded as the richest of all the languages considered here, in the following sense. Given a C m -term τ , we define inductively the S4 u -term τ † as follows: For any topological space T , the regular closed subsets of T are exactly the sets of the form X • − , where X ⊆ T . Hence, as the variable r ranges over 2 T , the S4 u -term r † = (r • ) − ranges over exactly the regular closed subsets of T . Using this observation, it is readily checked that ϕ is satisfiable over a frame (T, RC(T )) if and only if ϕ † is satisfiable over the frame (T, 2 T ). Thus, we may informally regard any logic (L, RegC), where L is a fragment of C m , as contained within the logic (S4 u , All). 2 Furthermore, the logic (S4 u , All) has essentially the same expressive power as the modal logic S4 (under McKinsey and Tarski's [37] topological interpretation) extended with the universal and existential modalities ∀ and ∃ of [24]. More precisely, define S4 u to be the set of terms formed using the variables in R together with the function symbols ∪, ∩, · , · • , · − , ∀, ∃, 0, 1.
Here, ∃ and ∀ are unary, with the remaining symbols having their usual arities. Given any interpretation M, we define τ M for any S4 u -term τ using (2.3) together with: Thus, ∃ is interpreted as the discriminator function, and ∀ as its dual. We say that an S4 uterm τ is valid if τ M = T for any model M over any topological frame (T, S). By replacing each equality τ 1 = τ 2 with the term ∀ (τ 1 ∩ τ 2 ) ∪ (τ 1 ∩ τ 2 ) and the Boolean connectives with the corresponding function symbols, we obtain a validity-preserving embedding of S4 u into S4 u -terms. On the other hand, it is well known (see, e.g., [1,30]) that every S4 u -term can be equivalently transformed to a term without occurrences of ∀ and ∃ in the scope of • , − , ∀ and ∃. Any such term can easily be rewritten as an equivalent S4 u -formula by replacing ∀τ and ∃τ with τ = 1 and τ = 0, respectively, and by replacing Boolean function symbols with the corresponding Boolean connectives. (Note, however, that this transformation in general results in an exponential increase in size.) As the validity and satisfiability problems for both S4 and S4 u are known to be PSpace-complete [34,39,2], it follows that the problem Sat(S4 u , All) is PSpace-complete as well.
In this section, we introduced the languages RCC-8, B, BRCC-8 (=C), C m and S4 u . The variables of these languages range over certain distinguished subsets of some topological space, and their non-logical symbols denote various fixed primitive topological relations and operations. The topological space in question and its collection of distinguished subsets together form a (topological) frame; and the pair of a language and a class of frames is a (topological) logic. In particular, we interpreted RCC-8, B, BRCC-8 (=C) and C m over the frame-class RegC, and the language S4 u over the frame-class All. We explained how all of these logics can be seen as fragments of (S4 u , All), which has essentially the expressive power of the modal logic S4 u . We observed that the complexity of the satisfiability problems for all of these logics is known. However, none of the above languages can express the property of being a connected region. Our question is: what happens to the complexity of satisfiability when that facility is provided?

Topological logics with connectedness
A topological space T is connected just in case it is not the union of two non-empty, disjoint, open sets. Note that this definition can be expressed by the following S4 u -formula (see [51]): The simplest way to introduce connectedness into topological logics is to restrict attention to frames over connected topological spaces. For example, consider the classes of frames given by Thus, it makes sense to consider the problems Sat(L, ConRegC) for L any of RCC-8, B, C or C m , as well as the problem Sat(S4 u , Con). An alternative, and more flexible, approach, however, is to expand the languages in question. Let c be a unary predicate. If L is one of the topological languages introduced in Section 2, denote by Lc (L with connectedness) the result of augmenting the topological primitives of L by c. Formally, if L = L(F, P ), The predicate c is given the expected fixed interpretation as follows: Thus, from the languages RCC-8, B, C, C m and S4 u , we obtain RCC-8c, Bc, Cc, C m c, S4 u c.
Consider, for example, the language Bc, which includes the formula It is a well-known fact that, if T is a topological space, any two connected subsets of T with non-empty intersection have a connected union; further, if X is connected, and X ⊆ Y ⊆ X − , then Y is also connected. But if r and s are regular closed subsets of T , At the other end of the expressive spectrum, consider the language S4 u c, which includes the formula Using one of the facts we have just alluded to, it follows that (3.2) is valid over All.
The predicate c can be generalized in the following way. Let c ≤k be a unary predicate, where k ≥ 1 is represented in binary. If L is one of the languages introduced in Section 2, we denote by Lcc (L with component counting) the result of augmenting the topological primitives of L by all of the predicates c ≤k (k ≥ 1). Formally, if L = L(F, P ), The predicates c ≤k are given fixed interpretations as follows, where M is a model over some frame (T, S): Thus, from the languages RCC-8, B, C, C m and S4 u , we obtain RCC-8cc, Bcc, Ccc, C m cc, S4 u cc. We write ¬c ≤k (τ ) as c ≥k+1 (τ ) and abbreviate c ≤1 (τ ) by c(τ ). Thus, we may regard Lc as a sub-language of Lcc. To illustrate, consider the Bcc-formula Using the same argument as for (3.1), this formula is easily shown to be valid over RegC.
For rich topological languages, such as S4 u c, the predicates c ≤k give us-in some senseno expressive power that c does not already give us. Let τ be an S4 u c-term and r 1 , . . . , r k variables not occurring in τ . Consider the S4 u c-formulas together with some model M over a topological frame (T, S). Let us assume that (T, S) has the property that, if r ∈ S, and s is a component of r, then s ∈ S-a very natural requirement for topological frames. If (3.4) is true in M, then τ M is seen to have at most k components. Conversely, if τ M has at most k components, then, by modifying the regions assigned to r 1 , . . . , r k if necessary, we easily obtain a model M ′ satisfying (3.4). It follows that, if ϕ is an S4 u cc-formula, then any instance of c ≤k (τ ) having positive polarity may be equisatisfiably replaced by (3.4) (with fresh variables r 1 , . . . , r k ). Similarly, any instance of c ≥k (τ ) having positive polarity may be equisatisfiably likewise replaced by (3.5). However, while the number of symbols in the predicate c ≤k is proportional to log k, the number of symbols in (3.4) is proportional to k. That is: S4 u c-formulas are in general exponentially longer than the S4 u cc-formulas they replace. So, although the componentcounting predicates c ≤k can usually be eliminated in this way, doing so may affect the complexity of the satisfiability problem.
The main contribution of this paper is to determine the computational complexity of the satisfiability problems for topological logics based on the languages Lc and Lcc, where L is any of the languages introduced in Section 2. To date, there are only two known complexity results for such logics. On the one hand, according to [40], satisfiability of S4 u cc-formulas over All is NExpTime-complete, which gives the NExpTime upper bound for all of the other logics considered in this section. On the other, according to [57], satisfiability of C-formulas is PSpace-complete over ConRegC.

Aleksandrov spaces.
The close connection between spatial logics and the modal logic S4 u mentioned above suggests that instead of topological semantics one may try to employ Kripke semantics (which gives rise to topological spaces with a very transparent structure) and the corresponding modal logic machinery.
Recall that Kripke frames for S4 u are pairs of the form (W, R), where W is a set, and R is a reflexive and transitive relation on W ; such frames are also called quasi-orders. Every quasi-order (W, R) can be regarded as a topological space by declaring X ⊆ W to be open if and only if X is upward closed with respect to R, that is, if x ∈ X and xRy then y ∈ X. In other words, for every X ⊆ W , The most important property distinguishing topological spaces T induced by quasi-orders is that arbitrary (not only finite) intersections of open sets in T are open. Topological spaces with this property are called Aleksandrov spaces. It is also known (see, e.g., [7]) that every Aleksandrov space is induced by a quasi-order.
Another important feature of such topological spaces is that the topological notion of connectedness in T coincides with the graph-theoretic notion of connectedness in the undirected graph induced by (W, R). More precisely, one can easily check that a set X ⊆ W is connected in T if and only if, for any points x, y ∈ X, there is a path x = x 1 , . . . , x n = y such that, for all i, 1 ≤ i < n, we have x i ∈ X and either x i Rx i+1 or x i+1 Rx i .
Henceforth, we shall identify an Aleksandrov space with the quasi-order generating it, alternating freely between topological and graph-theoretic perspectives. Denote by Alek the class of finite Aleksandrov frames. A topological model based on an Aleksandrov space will be called an Aleksandrov model.
The next lemma, originating in [37] and [33], shows that, for many topological logics, it suffices to work with finite Aleksandrov spaces. It can be proved by the standard filtration argument (see, e.g., [9]).
This lemma has a number of important consequences. First, it follows immediately that Sat(S4 u , All) = Sat(S4 u , Alek). Using the translation · † of B-terms and C m -formulas into S4 u defined in Section 2, we obtain Sat(C m , RegC) = Sat(C m , Alek ∩ RegC), etc. The PSpace upper bound for Sat(S4 u , All) follows from Lemma 4.1 and the fact (well-known in modal logic) that the model A in Lemma 4.1 can be 'unravelled' into a forest of trees of clusters, 3 with the length of branches not exceeding the maximal size of terms in Θ-the so-called tree-model property of S4 u . Finally, the fact that f is continuous guarantees that the number of components in f (τ M ) does not exceed the number of components in τ M , which will be used in the case of logics with connectedness predicates.
For the topological logics with B-terms only, say C m cc, even simpler Aleksandrov models are enough. Call a quasi-order (W, R) a quasi-saw if W = W 0 ∪ W 1 , for some disjoint W 0 and W 1 , and R is the reflexive closure of a subset of W 1 × W 0 . In this case we also say that the points in W i are of depth i in (W, R); see Fig. 4. Aleksandrov models over quasi-saws will be called quasi-saw models.

Lemma 4.2. For every finite Aleksandrov model
Proof.Let W 0 be the set of maximal points in (W, R A )-the set of points from the final clusters in (W, R A ), to be more precise-i.e., In every final cluster C ⊆ W 0 with |C| ≥ 2 we select some point and denote by U the set of all such selected points. Then we set V 0 = W 0 \ U and V 1 = W \ V 0 , and define R B to be the reflexive closure of R A ∩ (V 1 × V 0 ). Clearly, (W, R B ) is a quasi-saw, with V 0 and V 1 being the sets of points of depth 0 and 1, respectively. For every variable r, let r B = r A . As the extension of a B-term τ in A is regular closed and A is finite, it is straightforward to show: if y ∈ τ A then there exists z ∈ V 0 such that yR A z and z ∈ τ A . (4.1) We now prove (i) and (ii) by induction on the construction of τ .
(i) The basis of induction follows from the definition.
As τ A is regular closed, it is the closure under R − A of the set of final clusters in X. It follows immediately from the definition of R B that all non-final points in X have precisely the same R B -and R A -accessible final points. This means that X is connected in (W, R B ) as well.
Recall now that every satisfiable C m -formula is satisfiable in a finite Aleksandrov model, and so, by Lemma 4.2, in a quasi-saw model (over RegC). The following lemma imposes restrictions on the branching factor and the number of points of depth 1 in such models. Let us call a k-fork any partial order of the form depicted in Fig. 5.
then it is satisfiable in a quasisaw model over the disjoint union of n-many k i -forks, 1 ≤ i ≤ n, where n ≤ |ϕ| and each k i does not exceed the largest value k such that the predicate C k occurs in ϕ. We construct a quasi-saw model A = (T A , RC(T A ), · A ) induced by a disjoint union of forks (W A , R A ) and a map f : T A → T B as follows: i ; in the former case we add a fresh 1-fork ({u, v}, {(u, v)} * ) to (W A , R A ) and set f (u) = x and f (v) = x; in the latter case we add a fresh k-fork , for every v of depth 0, and u ∈ r A iff there is v ∈ r A of depth 0 with uR A v, for every u of depth 1. By definition, r A is regular closed in A, and it is easily checked that A |= Λ.
As an immediate consequence of Lemma 4.3 we obtain the following: they can. For example, maximal tractable (polynomial) fragments of RCC-8 were identified in [44,46], and it was shown in [26] that the problem of determining the satisfiability of a conjunction of atomic formulas of RCC-8 over the class RegC is NLogSpace-complete.
We close this section with some remarks about logics interpreted over connected spaces. The language C can distinguish between connected and disconnected spaces, because the formula ¬C(r, −r) ∧ (r = 0) ∧ (r = 1) (4.2) is satisfiable, but only in models over disconnected spaces. By contrast, the languages B and RCC-8 cannot distinguish between connected and disconnected spaces: Indeed, suppose that an RCC-8-formula ϕ is satisfied in a quasi-saw model A with the underlying quasi-order (W A , R A ) constructed in the proof of Lemma 4.3. To make this model connected, we can simply add to W A a new point w of depth 0 and extend R A by the arrows uR A w, for all u of depth 1 in A. It is easy to see that, under the same valuation as in A, ϕ is satisfiable in the extended connected model. For the less expressive language B, it suffices to add a new point of depth 1 to A and connect it to all points of depth 0; details are left to the reader.
On the other hand, equipping even the weakest spatial logics such as RCC-8 or B with the connectedness predicates (or even just interpreting them over connected spaces) invalidates various model-theoretic properties employed above-most notably the 'tree-model' property, heavily used in the proof of Lemma 4.3. Consider, for example, the Bc-formula ¬c(r) ∧ c(1). Its smallest satisfying quasi-saw model is illustrated in Fig. 6. Note that this model cannot be transformed to a forest, because the underlying frame must stay connected. Indeed, as we shall see in the next section, to satisfy Bc-formulas, or C-formulas in connected spaces, quasi-saw models with exponentially many points in the length of the formulas may be required. It is these phenomena that are responsible for the increased complexity of satisfiability which we shall encounter below.

Computational complexity
We are now in a position to prove tight complexity results for spatial logics in the range between Bc and S4 u cc. The NExpTime upper bound for all the logics considered in this paper was obtained in [40]: The idea of the proof is based on the following observations. Let ϕ be any S4 u ccformula. Evidently, ϕ is satisfiable if and only if there exists a set Φ of S4 u cc-literals, involving all the atoms occurring in ϕ, such that: (i) Φ is satisfiable; and (ii) Φ ∪ {ϕ} is satisfiable in propositional logic (where we treat all the atoms as propositional variables). Since propositional satisfiability can be checked in NP, it suffices to restrict attention to S4 u cc-formulas which are conjunctions of literals-i.e. those of the form: The conjuncts of the form c ≥k ′ i (σ ′ i ) can be eliminated using the following lemma [40]: 40]). Let ϕ be any S4 u cc-formula, and τ an S4 u -term. Then, for every n ≥ 0, there exists an S4 u c-formula ψ, with |ψ| bounded by a polynomial function of n + |τ |, such that ϕ ∧ ψ is satisfiable if and only if ϕ ∧ c ≥2 n (τ ) is satisfiable.
By repeated applications of Lemma 5.2, it is then a straightforward matter to transform (5.1), in polynomial time, into an equisatisfiable formula of the form Suppose that ψ is true in some model M over a space T , and let Θ be the set of terms occurring in ψ.
Let A and f be as guaranteed by Lemma 4.1. Then τ A = f (τ M ) for all τ ∈ Θ, and f is continuous, whence A |= ψ. Thus, if ψ is satisfiable, then it is satisfied over a topological space whose size is bounded by an exponential function of |ψ|, which gives the NExpTime upper bound of Theorem 5.1.
We turn next to the language S4 u c. By similar reasoning to the above, we may without loss of generality confine attention to the problem of determining the satisfiability of formulas of the form Proof. The proof is by reduction to the satisfiability problem for propositional dynamic logic PDL with converse and nominals, which is known to be ExpTime-complete [23,Section 7.3]. Let ψ be as in (5.3). Take two atomic programs α and β and, for each σ i , a nominal ℓ i . For a term τ , denote by τ ‡ the PDL-formula obtained by replacing in τ , recursively, each sub-term ϑ • with [α * ]ϑ. Thus the transitive and reflexive accessibility relation of the modal logic S4 is simulated by α * , and the universal modality ∀ (see the end of Section 2) is simulated by It is easy to see that ψ ′ is satisfiable if and only if ψ is satisfiable: the first conjunct of ψ ′ states that ρ is empty, the second that all τ i are non-empty, the third states that each σ i holds at a point where ℓ i holds and that from each σ i -point there is a path (along α ∪ α − ) to ℓ i which lies entirely within σ i .
If ψ is parsimonious in its use of connectedness, we can do somewhat better. Denote by S4 u c 1 the set of S4 u c-formulas with at most one occurrence of an atom of the form c(τ ).
Proof. The lower bound follows from [34]. We sketch a nondeterministic PSpace algorithm recognizing Sat (S4 u c 1 , All). We may assume without loss of generality that the input ψ has the form (5.3), with n ≤ 1. If n = 0, i.e. if ψ does not contain a conjunct of the form c(σ)∧ (σ = 0), then a standard satisfiability checking algorithm for S4 u is applied. Assume, then, that n = 1 in (5.3); and write σ for σ 1 for all τ ∈ B. Now, guess a type t σ containing σ and start (m + 1) S4-tableau procedures (see, e.g., [19,25]) with inputs τ 1 ∩ ρ • , τ 2 ∩ ρ • , . . . , τ m ∩ ρ • , and t σ ∩ ρ • in the usual way, expanding nodes branch-by-branch, and recovering the space once branches are checked. We may as well assume that the nodes of these tableaux are types. Suppose t is a type occurring in one of them. If σ ∈ t, it suffices to check that t can be connected by a σ-path of ≤ 2 |ψ| points to t σ . This can be done in PSpace by the following non-deterministic subroutine. We start with t and count from 1 to 2 |ψ| . At each step we guess a new type t ′ with σ, ρ • ∈ t ′ , and check that • either (i) τ ∈ t ′ for all τ • ∈ t, or (ii) τ ∈ t, for all τ • ∈ t ′ (in the former case, t ′ is accessible from t, in the latter, the other way around); • an S4-tableau with root t ′ can be constructed (which can be discarded after completion).
Note that, although this tableau may contain types t ′′ with σ ∈ t ′′ , these types can never threaten the connectedness of σ, since they are all accessible from the root t ′ of the tableau, and so are connected to both t and t σ , by the transitivity of the accessibility relation. If both checks are successful and t ′ = t σ , the subroutine succeeds; if t ′ = t σ we set t = t ′ and continue to the next step (provided that the step number < 2 |ψ| , otherwise the subroutine fails). Clearly, this subroutine succeeds if there is a σ-path connecting t and t σ and fails in every computation otherwise; moreover, it requires only polynomial memory to store the tableau for t ′ and the step number.
To reduce notational clutter we denote, for any topological space T , the (singleton) frame-class {(T, 2 T )} simply by T , and the (singleton) frame-class {(T, RC(T ))} simply by RC(T ). This notation is not entirely uniform, but it should be obvious what is meant.
As shown in [51] (see also Theorem 6.1 below), Sat(S4 u , Con) = Sat(S4 u , R n ) for any n ≥ 1. Recalling now that the modal logic S4 is PSpace-hard, we immediately obtain the following: Corollary 5.5. Sat(S4 u , Con) and Sat(S4 u , R n ) are all PSpace-complete for any n ≥ 1.
The proof of Theorem 5.4 can be generalized in various ways. For example, assume that ψ = ψ 1 ∧ ψ 2 is an S4 u c-formula in which ψ 2 = 1≤i<j≤n (σ i ∩ σ j = 0), where {σ 1 , . . . , σ n } is the collection of all σ i such that c(σ i ) occurs in ψ 1 . A straightforward extension of the algorithm in the proof of Theorem 5.4 shows that satisfiability of ψ is still in PSpace. Thus, if the connectedness predicate is applied only to regions that are known to be pairwise disjoint, then it does not matter how many times this predicate occurs in the formula: satisfiability is still in PSpace.
Our next theorem gives matching lower bounds for Theorem 5.4 and Corollary 5.5.
Proof. Let L be a language in PSpace. Then there is a polynomial-space-bounded deterministic Turing machine M recognizing L. Without loss of generality, we may assume that, given some input a ∈ L on the tape, M starts in the initial state, reaches the accepting state (with the resulting tape being empty and the head positioned over the first cell) and then moves to the halting state, from which no transition is possible. Moreover, throughout the computation the machine never goes to the left of the first cell and to the right of the s'th cell, where s = p(| a|) for some polynomial p(·).
Let where a 1 , . . . , a s (a j ∈ Σ) is the current contents of the tape, q ∈ Q the current state, and i the current position of the head. If a configuration c ′ is obtained from a configuration c by applying one instruction of M then we write c → c ′ . It will be convenient for us to represent M as the following set T of 4-tuples, where t, b are two fresh auxiliary symbols (see Fig. 7) :  • (a, t, a, t) and (a, b, a, b), for every a ∈ Σ, • (a ′ , (q ′ , b), (q ′ , a ′ ), b) and (a ′ , t, (q ′ , a ′ ), (q ′ , t)), for all a ′ ∈ Σ and q ′ ∈ Q, • ((q, a), t, (q ′ , a ′ ), b), for every instruction (q, a) → (q ′ , a ′ , 0) in M , • ((q, a), t, a ′ , (q ′ , b)), for every instruction (q, a) → (q ′ , a ′ , −1) in M , • ((q, a), (q ′ , t), a ′ , b), for every instruction (q, a) → (q ′ , a ′ , +1) in M . Now we describe the computations of M in terms of C-formulas. While constructing the formulas, we will assume that A is a connected quasi-saw model induced by (W, R) and W 0 is the set of points of depth 0 in (W, R).
We need s variables T 1 k , . . . , T s k , for each T k ∈ T , and three additional variables B 0 , B 1 and B 2 . Consider the following C-formulas: If the conjunction of (5.6)-(5.7) holds in A then every point x ∈ W 0 is precisely in one of (B ℓ ) A , 0 ≤ ℓ ≤ 2. We will use the B ℓ to introduce 'direction' in our quasi-saw model in the following sense. If x 1 , x 2 ∈ W 0 and zRx i , i = 1, 2, then there are only three possibilities: where ⊕ denotes addition modulo 3. (Here we remind the reader that τ 1 · τ 2 = 0 holds in a quasi-saw model A iff τ A 1 and τ A 2 contain no common points of depth 0. This means, in particular, that (τ 1 · τ 2 ) A = ∅ may hold even though τ A 1 ∩ τ A 2 = ∅, i.e., A |= C(τ 1 , τ 2 ).) Suppose also that the following formulas hold in A: Consider now the following formulas, for 1 ≤ i ≤ s, 0 ≤ ℓ ≤ 2, T k 1 , T k 2 ∈ T : Suppose that all of (5.6)-(5.14) are true in A. It easy to see that, if x, y ∈ W 0 and there exists z ∈ W with zRx and zRy, then: left(x) = left(y) and right(x) = right(y) whenever x, y ∈ (B ℓ ) A , for 0 ≤ ℓ ≤ 2. (5.16) Finally, we require the following formulas: T 1 j 1 · · · · · T s js = 0, where left(T i 1 ), . . . , left(T is ) is the initial configuration (with a written on the tape) and right(T j 1 ), . . . , right(T js ) is the accepting configuration (with empty tape and the head scanning the first cell). Denote the conjunction of (5. We may assume without loss of generality that the u i and v j are all distinct. It should be noted that left(u i ) is not the accepting configuration for any i ≤ m. For brevity, we write c i for left(u i ) and c m+1 for right(u m ). We shall show that c 0 , . . . , c m , c m+1 contains a sub-sequence that is an accepting run of M . From (5.15) and (5.16), and the fact that left(x) → right(x) for any point x, we see that, for all i (0 ≤ i ≤ m), one of the following conditions holds: We shall presently establish the following claim: Claim 5.7. If 0 ≤ j ≤ m and c j ← c j+1 , then there exists k such that j + 1 < k ≤ m and c k = c j .
Taking this claim on trust for the moment, define the sub-sequence c j 0 , c j 1 , . . . by setting j 0 to be the largest j ≤ m such that c j = c 0 , and, for i ≥ 0, j i+1 to be the largest j ≤ m such that c j = c j i +1 , until we eventually reach (say), c j K = c m . It is then immediate from the claim that c j i → c j i +1 = c j i+1 for all i (0 ≤ i < K), and we have the desired accepting run of M . Proof of Claim 5.7. The claim is proved by (decreasing) induction on j. For j = m, the result is trivial, since c m+1 has no successor configurations. Assume, then, that 0 ≤ j < m, and the claim holds for all larger values of j up to m. Let k be the largest number (j + 1 ≤ k ≤ m + 1) such that c j+1 = c k . Thus, k ≤ m (since c j+1 is, by assumption, not the accepting configuration), and c k → c k+1 (since otherwise, using the inductive hypothesis, we could find a larger value k ′ with c j+1 = c k ′ ). Thus, c j ← c j+1 = c k → c k+1 . But M is deterministic, so c j = c k+1 , completing the induction, and proving the claim.
The proof of the converse direction is straightforward: for an accepting computation c 0 → · · · → c m+1 of M on a, we construct a model A over RC(R). Define the closed intervals I 0 , . . . , I m in R by   RegC) and Sat(C, RC(R n )) for any n ≥ 1 are all PSpace-complete.
Having established a lower bound for Cc 1 , we now proceed to do the same for the larger language Cc. Observe that when constructing a model for an S4 u c 1 -formula with one positive occurrence of c(τ ), in the proof of Theorem 5.4, we could check the 'connectability' of two τ -points by an (exponentially long) path using a PSpace-algorithm, because we did not need to keep in memory all the points on the path. However, if two statements c(τ 1 ) and c(τ 2 ) have to be satisfied, then, while connecting two τ 1 -points using a path, one has to check whether the τ 2 -points on that path can be connected by a path, which, in turn, can contain another τ 1 -point, and so on. The crucial idea in the proof below is to simulate infinite binary (non-transitive) trees using quasi-saws. Roughly, the construction is as follows. We start by representing the root v 0 of the tree as a point also denoted by v 0 (see Fig. 8), which is forced to be connected to an auxiliary point w by means of some c(τ 0 ). On the connecting path from v 0 to w we represent the two successors v 1 and v 2 of the root, which are forced to be connected in turn to w by some other c(τ 1 ). On each of the two connecting paths, we again take two points representing the successors of v 1 and v 2 , respectively. We treat these four points in the same way as v 0 , reusing c(τ 0 ), and proceed ad infinitum, alternating between τ 0 and τ 1 when forcing the paths which generate the required successors. Of course, we also have to pass certain information from a node to its two successors. Such information can be propagated along connected regions. Note now that all points are connected to w. To distinguish between the information we have to pass from distinct nodes of even (respectively, odd) level to their successors, we have to use two connectedness formulas of the form c(f i + a), i = 0, 1, in such a way that the f i points form initial segments of the paths to w and a contains w. The f i -segments are then used locally to pass information from a node to its successors without conflict. We now present the reduction in more detail.
Proof. The proof is by reduction of the following problem. Denote by D f 2 the bimodal logic (with 2 1 and 2 2 ) determined by Kripke models based on the full infinite binary tree G = (V, R 1 , R 2 ) with functional accessibility relations R 1 and R 2 . Consider the global consequence relation |= f 2 defined as follows: χ |= f 2 ψ iff K |= χ implies K |= ψ, for every Kripke model K based on G. This global consequence relation is ExpTime-hard, see, e.g., [52]. We construct a Cc-formula Φ(χ, ψ), for any D f 2 -formulas χ, ψ, such that (i ) ψ) is satisfiable over ConRegC. While constructing Φ(χ, ψ), we will assume that A is a quasi-saw model induced by (W, R) and W 0 is the set of points of depth 0 in (W, R).
Let sub(χ, ψ) be the closure under single negation of the set of subformulas of χ, ψ. For each ϕ ∈ sub(χ, ψ) we take a fresh variable q ϕ , and for each 2 i ϕ ∈ sub(χ, ψ), a pair of fresh variables m i,j ϕ , j = 0, 1. We also need fresh variables a and s i j , for j = 0, 1 and 0 ≤ i ≤ 6.  Figure 8: First 4 steps of encoding the full binary tree using 7-saws.
following Cc-formulas hold in A a = s 6 0 ∧ a = s 6 (5.20) where f j = s 0 j +s 1 j +s 2 j +s 3 j +s 4 j +s 5 j , for j = 0, 1. It follows that, for j = 0, 1, if there is a point x 0 ∈ (s 0 j ) A ∩ W 0 then there is a (not necessarily unique) sequence of points . Points x 2 and x 4 will be used to construct similar sequences for the two successors of the node represented by hold in A and x 0 ∈ (s 0 j ) A ∩ W 0 , then one can recover from A the infinite binary tree with the root at x 0 . The formula ensures then that there is x 0 ∈ (s 0 0 ) A ∩ W 0 , the root of the tree, in which ¬ψ holds, and χ holds everywhere in the tree, while the formulas for all ¬ϕ, ϕ 1 ∧ ϕ 2 ∈ sub(χ, ψ), capture the meaning of the Boolean connectives from sub(χ, ψ) relativized to d. The formulas, for all 2 i ϕ ∈ sub(χ, ψ) and j = 0, 1, are used to propagate information regarding 2 i ϕ along the components of f j using the markers m i,j ϕ . We define Φ(χ, ψ) to be the conjunction of all the above formulas. Clearly, |Φ(χ, ψ)| is polynomial in |χ| + |ψ| and contains only two occurrences of the connectedness predicate, c, in (5.19).
Suppose that Φ(χ, ψ) is satisfied over RegC; we proceed to show that χ |= f 2 ψ. By Lemmas 4.1 and 4.2, Φ(χ, ψ) is satisfied in a finite quasi-saw model A induced by some (W, R). Denote by W 0 the set of points of depth 0 in (W, R). Our aim is to construct, by induction, a Kripke model K based on the full infinite binary tree G = (V, R 1 , R 2 ) such that K |= χ and K, v 0 |= ψ, for the root v 0 of G. The points of V will be copies of some points Step 0. Take some x 0 ∈ (q ¬ψ · s 0 0 ) A ∩ W 0 . It exists by (5.22). Take a fresh v 0 and let κ(v 0 ) = x 0 and G 0 = ({v 0 }, ∅, ∅) and set v 0 |= p for each propositional variable p ∈ sub(χ, ψ) such that x 0 ∈ q A p .
Step n + 1. Suppose that we have already constructed G n = (V n , R n 1 , R n 2 ) and defined a valuation in G n for the variables in sub(χ, ψ). Let v be a point of minimal co-depth in G n which does not have R 1 -and R 2 -successors yet, and let κ(v) = x ∈ (s 0 j ) A ∩ W 0 , for some j ∈ {0, 1}. We have x ∈ f A j , and so by (5.19), there is a finite path π from x to some w ∈ (s 6 j ) A ∩ W 0 such that all the points on this path belong to (f j + a) A , and so to 6 k=0 (s k j ) A . Fix such a path π. By the first conjunct of (5.20), x = w and in view of the second conjunct of (5.20), of all (s k j ) A on the path π the set (s 0 j ) A can only be in contact with (in fact, externally connected to) (s 1 j ) A . Take the last point y 1 ∈ (s 1 j ) A ∩ W 0 on π. By a similar argument, the next point of depth 0 on π can only be from (s 2 j ) A . Let x 1 be the last point in (s 2 j ) A ∩ W 0 on π. In the same way we find the last point y 2 ∈ (s 3 j ) A of depth 0 on π, and then the last point where ⊕ denotes addition modulo 2, and we can move on to Step n + 2.
Step ω. Finally, we set V = n<ω V n , R 1 = n<ω R n 1 , R 2 = n<ω R n 2 , G = (V, R 1 , R 2 ). Clearly, G is the full binary tree with functional R 1 and R 2 . The Kripke model K is based on G with the valuation defined by the inductive procedure above.
It remains to show by induction that, for every ϕ ∈ sub(χ, ψ) and every v ∈ V , The basis of induction follows from the definition, and the case of Boolean connectives from (5.23). Suppose now that v is the point considered at Step n + 1 above. Let i = 1 or 2 and v i ∈ V be such that (v, v i ) ∈ R i (it is defined uniquely as R i is functional). We have Figure 9: A 7-saw for v.
κ(v) ∈ (s 0 j ) A , for either j = 0 or j = 1, and, by (5.21), Suppose, finally, that χ |= f 2 ψ; we proceed to show that Φ(χ, ψ) is satisfied over ConRegC, thus completing the proof of the theorem. Let K be a model for D f 2 based on the full infinite binary tree G = (V, R 1 , R 2 ) with root v 0 such that K |= χ and K, v 0 |= ψ. We construct a connected quasi-saw model A satisfying Φ(χ, ψ). The model A will be induced by the quasi-saw (W, R) constructed by induction from (infinitely many copies of) the 7-saws shown in Fig. 9. For each node v of the infinite binary tree G, we take a fresh , for 0 ≤ i < 5, and z v 5 R v w v , and identify the following points if v 1 and v 2 are the R 1 -and R 2 -successors of v. We present our construction in a step-by-step manner (see Fig. 8).
Step n + 1. Suppose now that v is a node of minimal co-depth in G such that the constructed quasi-saw (W n , R n ) contains y v 0 but does not contain a copy of S v for v and let v 1 and v 2 be the R 1 -and R 2 -successors of v. Then we take a fresh 7-saw S v and 'hook' it to (W n , R n ) by identifying the first point of S v with y v 0 and its last point with w (see Fig. 8): , and define the valuation · A n+1 by taking p A n+1 = p An ∪ p Av , where · Av is defined for the new points as follows: where j = 0 if v is of even co-depth in G and j = 1 otherwise, and ⊕ denotes addition modulo 2.
Step ω. Finally, we set W = n<ω W n , R = n<ω R n and · A = n<ω · An . Note that y v 1 and y v 3 are required to make the set of points in f A j representing a node v of G disconnected from the subset of f A j representing another node v ′ of G and thus satisfy (5.24); y v 5 are required to satisfy the last conjunct of (5.20). We leave the remaining details to the reader. Proof. Follows from Theorems 5.3 and 5.9.
The argument of Theorem 5.9 goes through unproblematically when we restrict attention to the spaces R n for n ≥ 3, thus showing that Sat(Cc, RC(R n )) is ExpTime-hard for these values of n. If n = 2, however, this approach fails. The difficulty is that the construction of the model A of Φ(χ, ψ) from the Kripke structure K will result in sets (s k j ) A that have infinitely many components lying in a bounded region of the plane. These infinitely many components will give rise to accumulation points, meaning that we can no longer guarantee the truth of the formulas ¬C(s k j , s k ′ j ) of (5.20) and (5.24). Fortunately, the proof can be rescued, either by means of the finite model property for |= f 2 , or, alternatively, via the following explicit construction based on polynomial-space alternating Turing machines. We remind the reader, in this connection, that APSpace = ExpTime (see e.g., [32]).
Theorem 5.11. The problems Sat(Cc, RC(R n )) for all n ≥ 2 are ExpTime-hard.
Proof. Let M be an alternating Turing machine that uses ≤ p(n) cells on each input of length n, for some polynomial p(·). Let q Y and q N be the accepting and rejecting states of M , respectively (they have no transitions from them). Without loss of generality we assume that every branch of the computation tree of M is of finite length and its final state is either q Y or q N (indeed, for if it is not the case we can augment M with a subroutine that at each step of M increases the current step number written on an auxiliary tape and makes M go into the rejecting state q N whenever the step number reaches the total number of configurations of M ; as M uses a polynomial working tape, we need only a polynomial number of cells on that auxiliary tape to represent the maximum number of configurations of M ). All states of M (except q Y and q N ) are divided into existential and universal states. We assume without loss of generality that there are exactly two transitions from each state, i.e., for q ∈ Q \ {q Y , q N }, a ∈ Σ and j = 1, 2, we have (q, a) → j (q ′ , a ′ , d), where d ∈ {−1, 0, +1}. We assume that M never goes beyond special markers at the beginning and the end of the tape. We denote p(n) by s, and employ propositional variables with the following intuitive meanings: placed onto (0, 0), and (iii ) if T tiles the 2 d × 2 d grid, with T 0 being placed onto (0, 0), then Θ(T , T 0 , d) is satisfiable over RC(R n ), n ≥ 2. While constructing the formula, we will assume that A is a quasi-saw model induced by (W, R) and W 0 is the set of points of depth 0 in (W, R).
We partition all points of W 0 with the help of a pair of variable triples H 0 , H 1 , H 2 and V 0 , V 1 , V 2 . Suppose that the formulas, for 0 ≤ ℓ ≤ 2, and their V -counterparts hold in A. Then every point in W 0 is in exactly one of the (H ℓ ) A , 0 ≤ ℓ ≤ 2, and exactly one of the (V ℓ ) A , 0 ≤ ℓ ≤ 2 (these variables play the same role as the B ℓ in the proof of Theorem 5.6).
To encode coordinates of the tiles in binary, we take a pair of variables X j and Y j , for each j, d ≥ j ≥ 1. For n < 2 d , let n X be the B-term X ′ d · X ′ d−1 · · · · · X ′ 1 , where X ′ j = X j if the jth bit in the binary representation of n is 1, and X ′ j = −X j otherwise. For a point u ∈ W 0 , we denote by X(u) the binary d-bit number n, called the X-value of u, such that u ∈ n A X (note that the X-value is defined uniquely for the points in W 0 ); the jth bit of X(u) is denoted by X j (u). The term m Y , the Y -value Y (u) of u and its jth bit Y j (u) are defined analogously. For a point u ∈ W 0 we write coor(u) for (X(u), Y (u)). We will use the variables X i and Y j to generate the 2 d × 2 d grid, which consists of pairs (n X , m Y ), for n, m < 2 d . Consider the following formulas, for 0 ≤ ℓ ≤ 2, ¬C(X d · · · · · X 1 · H ℓ , H ℓ⊕1 ), (5.35) where ⊕ denotes addition modulo 3. Suppose that A satisfies (5.28)-(5.35). If u, v ∈ W 0 and zRu and zRv, for some z ∈ W , then (cf. (5.15) and (5.16)) Let k be the minimal number such that u ∈ (−X k ) A , i.e., u ∈ ((−X k ) · X k−1 · · · · · X 1 · H ℓ ) A . Then, by (5.33), v ∈ X A k and, by (5.34), v ∈ (−X i ) A , for all i, k > i ≥ 1. By (5.31) and (5.32), v ∈ (−X j ) A iff u ∈ (X j ) A , for all d ≥ j > k. It follows that X(v) = X(u) + 1. The case of v ∈ (H ℓ ) A and u ∈ (H ℓ⊕1 ) A is similar.
Suppose now that (5.28)-(5.35) with their the Y -counterparts (X i and H ℓ replaced by Y i and V ℓ , respectively) hold in A. It follows that for every u, v ∈ W 0 with zRu and zRv, for some z ∈ W , we have which means that every point of depth 0 may be surrounded by all of its 8-neighbours (in the sense that they have a common predecessor of depth 1). We are, however, interested only in the 4-neighbours since only the 4-neighbours restrict the tile that can be assigned to the point. Formally, given a pair (n, m) in the 2 d × 2 d grid, denote by 4-nb(n, m) the set that consists of (n, m) and its (at most four) neighbours in the grid, i.e., (n − 1, m), (n + 1, m), (n, m − 1), (n, m + 1); see Fig. 10. Let G be a fresh variable, which will represent the points of the grid. Suppose now that in addition the formulas hold in A. Then, by (5.37), if u, v ∈ G A ∩ W 0 and zRu and zRv, for some z ∈ W , then either X 1 (u) = X 1 (v) or Y 1 (u) = Y 1 (v), and thus, by (5.36), coor(u) ∈ 4-nb(coor(v)) and coor(v) ∈ 4-nb(coor(u)). Suppose now that the following formulas are true in A as well: These constraints guarantee that in the connected set (G · (0 X + (2 d − 1) Y )) A there are points u (0,n) and u (n,2 d −1) , for n < 2 d , such that coor(u (0,n) ) = (0, n) and coor(u (n,2 d −1) ) = (n, 2 d − 1). Similarly for the connected set (G · (2 d − 1) X + 0 Y ) A . This gives us the border of the 2 d × 2 d grid we are after (see Fig. 11 (a)). And the constraints c(G·((−X 1 )+0 Y )), c(G·(X 1 +0 Y )), c(G·(0 X +(−Y 1 ))), c(G·(0 X +Y 1 )) (5.39) ensure that we can find inner points of the grid (see Fig. 11 (b)).
say that every point in G A ∩ W 0 is covered by precisely one tile and for 0 ≤ ℓ, ℓ ′ ≤ 2, says that all points in the same component of (H ℓ · V ℓ ′ ) A are covered by the same tile. That the colours of adjacent tiles match is ensured by for 0 ≤ ℓ ≤ 2. Finally, we have to say that (0, 0) is covered with T 0 : One can check that the conjunction Θ(T , T 0 , d) of these Ccc-formulas is as required. For instance, a quasi-saw model A satisfying Θ(T , T 0 , d) (if a tiling exists) is shown in Fig. 12 (a): all points belong to G A , solid white points to w A , solid black to b A and grey to both of the sets. Note that each point of depth 0 has at most 4 predecessors (of depth 1) and the same number of neighbours (points of depth 0 that share a common point of depth 1).
The second statement of the theorem follows from the fact that the model constructed above can be embedded in RC(R n ) for all n ≥ 2: indeed, in R 2 , we may represent tiles as octagons (see Fig. 12(b)), taking G to be the union of all those tiles. Note that the tiles' corners are cut to ensure that every tile has at most 4 neighbours and thus b A and w A have precisely 2 d−1 components.
We now consider lower complexity bounds for the languages Bc and Bcc, which will be obtained by reduction of satisfiability in Cc and Ccc, respectively. The basic idea is that two connected closed sets are in contact if and only if their union is connected and they are non-empty; in other words, the formula is a Cc-validity. Thus, if a Ccc-formula contains a subformula C(τ 1 , τ 2 ), where τ 1 and τ 2 denote connected non-empty regions, then we may replace that subformula by c(τ 1 + τ 2 ), thus eliminating an occurrence of C. The problem we face, of course, is that this 'reduction' of C to c cannot be directly applied to our formulas in which τ 1 and τ 2 are not necessarily connected and non-empty. The next three lemmas show how to overcome this problem.
We write ϕ[ψ] to indicate that ϕ contains a positive occurrence of ψ; then ϕ[ψ/χ] denotes the result of replacing all positive occurrences of ψ in ϕ by χ. Recall that topological spaces are allowed to be empty. There is exactly one frame based on the empty topological space, and exactly one model over that frame. (It is trivial to check whether a formula ϕ is satisfied in this model.) Accordingly, we define: Lemma 5.14. Let ϕ[C(τ 1 , τ 2 )] be a Ccc-formula, and t, t 1 , t 2 fresh variables. Then ϕ is equisatisfiable (in RegC and ConRegC) with the formula Proof. If ϕ is satisfiable over the empty space, there is nothing to prove; so assume otherwise. Evidently, Conversely, let A |= ϕ, for an Aleksandrov model A = (T, RC(T ), · A ); we then construct A * = (T, RC(T ), · A * ), where r A * = r A , for all variables occurring in ϕ. If A |= C(τ 1 , τ 2 ), then setting t A * = T secures A * |= ϕ * . If, on the other hand, . It is routine to check that both of the t A * i are regular closed and connected. Moreover, their sum is connected, since they share the point z. This secures A * |= ϕ * .
We note that the above lemma does not work in any R n , as intersecting sets do not necessarily share an open subset.
Suppose T is a topological space, and S a regular closed subset of T . Then S is itself a topological space (with the subspace topology), which has its own regular closed algebra. The following lemma is tedious to show in full generality, but simple for finite Aleksandrov spaces (which, by Lemma 4.1, is sufficiently general for our purposes). We state it here without proof.
Lemma 5.15. If S ∈ RC(T ), then RC(S) = {S · X | X ∈ RC(T )}. Furthermore, denoting the Boolean operations in RC(S) by + S , · S and − S , etc., we have, for any X, Y ∈ RC(S): (v ) X has the same number of components in S and T .
Proof. Again, we may assume that ϕ is not satisfiable over the empty space. Evidently, i=1,2 (c(t i ) ∧ (τ i · s ≤ t i ))∧¬c(t 1 +t 2 ) → ¬C(τ 1 ·s, τ 2 ·s) is a Ccc-validity. So any model A of ϕ * is a model of ϕ |s , whence, by Lemma 5.16, A |s |= ϕ. Note that A |s is connected whenever A |= c(s). Conversely, suppose A |= ϕ[¬C(τ 1 , τ 2 )], for a quasi-saw model A induced by (W, R). Let W i (i = 0, 1) be the set of points of depth i in (W, R). Without loss of generality, we may assume that every point in W 0 has an R-predecessor in W 1 . If A |= C(τ 1 , τ 2 ), let A * be exactly like A except that s A * and t A * are both the whole space. Then A * |= ϕ * . On the other hand, if A |= C(τ 1 , τ 2 ) then, for i = 1, 2, we add an extra point u i to W to connect up the points in τ A i (if there are any). Formally, let W * = W ∪ {u 1 , u 2 }, where u 1 , u 2 ∈ W , and let R * be the reflexive closure of the union of R and {(z, u i ) | z ∈ τ A i ∩ W 1 }, for i = 1, 2. Note that (W * , R * ) is connected if (W, R) is connected. Clearly, W is a regular closed subset of the topological space (W * , R * ). Now define the model A * over (W * , R * ) by setting s A * = W , t A * = ∅, t A * i = τ A i ∪ {u i } (i = 1, 2), and r A * = r A for all other variables r. Thus, A = A * |s , whence, by Lemma 5.16, A * |= ϕ |s , and so A * |= ϕ[¬C(τ 1 , τ 2 )/t = 0] |s . By construction, A * |= i=1,2 (c(t i ) ∧ (τ i · s ≤ t i )) ∧ ¬c(t 1 + t 2 ). Thus, A * |= ϕ * .
Proof. Given a Cc-formula, by repeated applications of Lemmas 5.14 and 5.17, we can compute an equisatisfiable Bc-formula in polynomial time. Similarly, given a Ccc-formula, we can compute an equisatisfiable Bcc-formula in polynomial time. It then follows from Theorem 5.9 that Sat(Bc, RegC) is ExpTime-hard, and from Theorem 5.12 that Sat(Bcc, RegC) is NExpTime-hard. Noting that Lemmas 5.14 and 5.17, and Theorems 5.9 and 5.12 all hold when we restrict attention to connected spaces, we obtain the remaining statements of the theorem.
We mention here that although Lemma 5.17 does not hold for R n , a simple modification of the proof of Theorem 5.18 can be used to show the following: Theorem 5.19. Sat(Bc, RC(R n )) is ExpTime-hard and Sat(Bcc, RC(R n )) is NExpTimehard, for any n ≥ 3.
Proof. Consider the formula Φ ′ (χ M , ψ a ) constructed in the proof of Theorem 5.11. It contains only negative occurrences of the predicate C. So, we can iteratively apply the transformation of Lemma 5.17 to obtain a Bc-formula Φ * . Denote by s the product of all regions s that have been used to relativize the formula. It follows from the proof of Theorem 5.11 that if M does not accept a then Φ ′ (χ M , ψ a ) is satisfiable in a quasi-saw model, for which we construct a new quasi-saw model A * over (W * , R * ) as described in the proof of Lemma 5.17. It follows from the proof of Lemma 5.17 that A * |= Φ * . We then embed the graph of the quasi-saw model A * into R n by associating with each point of depth 0 an n-dimensional ball with attached cylinders, which touch only if there is a respective point of depth 1. As Φ * is a Bc-formula and A * |= Φ * , Φ * is satisfied in the constructed model over RC(R n ). Conversely, if Φ * is satisfiable over RC(R n ) then, by Lemmas 4.1 and 4.2, it is satisfied in a quasi-saw model A. As i=1,2 (c(t i ) ∧ (τ i · s ≤ t i ))∧¬c(t 1 +t 2 ) → ¬C(τ 1 ·s, τ 2 ·s) is a validity, A is a model of Φ ′ (χ M , ψ a ) |s , whence, by Lemma 5.16, A |s |= Φ ′ (χ M , ψ a ) and thus, M does not accept a.
For the second statement of the Theorem, we proceed in a similar fashion, using Lemma 5.17 to remove all (negative) occurrences of C in the formula Θ(T , T 0 , d) constructed in the proof of Theorem 5.12.

Topological logics over Euclidean spaces
So far, we have been mainly concerned with the computational complexity of various topological logics interpreted over the very general classes of frames All, Con, RegC and ConRegC. In this section, we discuss what happens when we restrict consideration to the specific topological spaces R, R 2 or R 3 .
These equations can be established by embedding any model over RegC into one over the domain RC(R n ) in such a way that the satisfaction of formulas in the relevant language is unaffected. A suitable embedding for RCC-8 is described in [43]; the case of B is even more straightforward.
The corresponding equations fail for the languages C, C m and S4 u . For example, we saw that the C-formula (4.2) is satisfiable over frames in RegC, but only when the underlying space is disconnected. Thus, Sat(C, RC(R n )) = Sat(C, RegC), whence Sat(S4 u , R n ) = Sat(S4 u , All), for all n ≥ 1. However, it turns out that (4.2) is, so to speak, the only fly in the ointment: 51]). Let T be any connected, dense-in-itself, separable metric space. Then Sat(S4 u , T ) = Sat(S4 u , Con).
Hence, Sat(S4 u , K) = Sat(S4 u , Con) for any class of frames K included in Con and containing R n for any n, and similarly, Sat(C, K) = Sat(C, ConRegC) for any class of frames K included in ConRegC and containing RC(R n ) for any n.
The predicate c, however, changes the above picture dramatically.
Proof. Let r i (1 ≤ i ≤ 5) and r i,j (1 ≤ i < j ≤ 5) be variables. As we observed in Section 1, the formula is not satisfiable over RC(R), since the non-empty, regular closed, connected subsets of R are exactly the closed, non-punctual intervals. On the other hand, ϕ 1 is visibly satisfiable over RC(R n ) for all n ≥ 2.
Think of the regions (assigned to) r 1 , . . . , r 5 as 'vertices' and the regions (assigned to) r i,j (1 ≤ i < j ≤ 5) as 'edges', with r i,j connecting r i and r j . The literals of ϕ 2 having the form TPP(r i , r j,k ) ensure that 'vertices' (are non-empty and) are contained in any 'edges' which involve them. The literals of ϕ 2 having the form DC(r i,j , r k,l ) ensure that 'edges' lacking a common 'vertex' are not in contact. It is easy to construct a model for this formula over RC(R n ) for all n > 2. To show that ϕ 2 is not satisfiable over RC(R 2 ), suppose otherwise; we show, contrary to fact, that the graph K 5 has a plane embedding.
To avoid notational clutter, take r i (1 ≤ i ≤ 5) and r i,j (1 ≤ i < j ≤ 5) to denote regular closed sets of R 2 satisfying ϕ 2 . For any point p in any of the r i,j , let ε ′ p be the minimum Euclidean distance to any point q in any r k,l such that {i, j} ∩ {k, l} = ∅; let ε p = max(1, ε ′ p ); and let D p be the closed disc centred on p of radius ε p /3. For all i, j (1 ≤ i < j ≤ 5), let r ′ i,j = {D p | p ∈ r i,j }. The following are simple to verify: (i) r ′ i,j is regular closed; (ii) the open set (r ′ i,j ) • is connected (hence path-connected) and contains both r i and r j ; (iii) for all k, l (1 ≤ k < l ≤ 5) such that {i, j} ∩ {k, l} = ∅, r ′ i,j ∩ r ′ k,l = ∅. r 1 r 2 Figure 13: Two non-intersecting, connected, closed sets r 1 and r 2 on a torus: note that r 1 and r 2 are connected, but r 1 ∩ r 2 is not.
For all i (1 ≤ i ≤ 5), choose a point v i ∈ r i and, for all i, j, (1 ≤ i < j ≤ 5), join v i and v j with an arc α i,j lying in r ′ i,j . It is straightforward to draw these arcs in such a way that, for each i, the arcs with v i as an endpoint meet only at v i . However, if {i, j} ∩ {k, l} = ∅, the arcs α i,j and α k,l do not intersect.
Proof. Almost identical to Theorem 6.2, noting that, for r, s connected, DC(r, s) if and only if r + s is not connected.
It is not known whether Sat(Bc, RC(R 3 )) and Sat(Bc, ConRegC) are different. However, Sat(S4 u , R n ) = Sat(S4 u , Con) for all n ≥ 1. To see this, we rely on the following fact: Theorem 6.4 ([38], p. 137). If r 1 and r 2 are non-intersecting closed sets in R n , and points x and y are connected in r 1 and also in r 2 , then x and y are connected in r 1 ∩ r 2 .
The formula (r 1 ∩ r 2 = 0) ∧ i=1,2 (r − i ⊆ r i ) ∧ c(r i ) ∧ ¬c(r 1 ∩ r 2 ) (6.1) states that r 1 and r 2 are non-intersecting, closed, connected regions having connected complements, such that the intersection of their complements is not connected. This formula is not satisfiable over any R n , by Theorem 6.4. However, it is satisfiable over T for many natural, connected topological spaces T . For example, let T be a torus, and let r 1 and r 2 be interpreted as rings in T , arranged as in Fig. 13; it is then obvious that r 1 and r 2 satisfy (6.1). Thus, for all of our base languages L, the language Lc (and therefore also Lcc) is more sensitive than L to the spatial domain over which it is interpreted. Since we know the complexity of the satisfiability problems for Lc and Lcc for very general classes of spatial domains, the question naturally arises as to the complexity of these problems for spatial domains based on low-dimensional Euclidean spaces.
For n = 1, we have a reasonably complete picture.
This concludes our discussion of the complexity of satisfiability for topological logics interpreted over R.
Over R 2 , topological logics become harder to analyze. The encodings used to obtain lower complexity bounds in Section 5 apply unproblematically to Euclidean spaces of dimension at least 2. In particular, Theorem 5.9 states that Sat(Cc, RC(R n )) is ExpTime-hard, for all n ≥ 2, whence Sat(S4 u c, R n ) is ExpTime-hard, for all n ≥ 2. Similarly, Theorem 5.12 states that Sat(Ccc, RC(R n )) is NExpTime-hard, for all n ≥ 2, whence Sat(S4 u cc, R n ) is NExpTime-hard, for all n ≥ 2.
Upper bounds for Sat(Cc, RC(R n )), Sat(S4 u c, R n ), Sat(Ccc, RC(R n )) or Sat(S4 u cc, R n ), where n ≥ 2, are not known. However, for the smaller language RCC-8, upper bounds are known from the literature in the case where the spatial domain is limited to certain wellbehaved regions in R 2 . One such domain is the set D of closed disc-homeomorphs in R 2 , with which we began this paper. We mention the following remarkable fact, the proof of which is too involved to repeat here: Theorem 6.8 ( [50]). The problem Sat(RCC-8, (R 2 , D)) is NP-complete.
Finally, we remark that, if n ≥ 3, no upper complexity bound is currently known for the problem Sat(Bc, RC(R n )), or, therefore, for any more expressive spatial logic.

Conclusion
In this paper, we have investigated the effect of augmenting various topological logics in the qualitative spatial reasoning literature with predicates able to express the property of connectedness. We considered three principal base languages: B, the language of the variety of Boolean algebras; C, the extension of the well-known language RCC-8 with regioncombining operations; and S4 u , the extension of Lewis' system S4 with a universal operator, under the topological interpretation of McKinsey and Tarski. And we considered two kinds of connectedness predicate: c(r), for 'region r is connected'; and c ≤k (r), for 'region r has at most k connected components.' For each base language L, we defined the languages Lc (by adding the predicate c) and Lcc (by adding the predicates c ≤k (r) for k ≥ 1); and we considered the complexity of the satisfiability problems for L, Lc and Lcc over various natural (classes of) spatial domains, both very general-as in the case of RegC, ConRegC, All and Con-and also very specific-as in the case of RC(R n ) and R n for various n.
We showed that, whereas the base languages display a surprising indifference to the frames over which they are interpreted, the corresponding languages with connectedness predicates are highly sensitive in this regard. We also showed that the addition of connectedness predicates increases the complexity of satisfiability over general classes of framestypically from NP or PSpace (for the base language L) to ExpTime (for the corresponding language Lc) and NExpTime (for the language Lcc). We observed that this increase in complexity is 'stable': over the most general classes of frames, the extensions of such different formalisms as B and S4 u with connectedness predicates are of the same complexity. We further observed that by restricting these languages to formulas with just one connectedness  Table 1: Satisfiability complexity for the topological logics considered in this paper.
constraint of the form c(r), we obtain logics that are still in PSpace, while two such constraints lead to ExpTime-hardness. Finally, we turned our attention to the complexity of the satisfiability problems for these languages when interpreted over Euclidean spaces, summarizing what is currently known and stating several open problems. The results obtained are summarized in Table 6.