Vincenzo Ciancia

Diego Latella

Michele Loreti

Mieke Massink

Specifying and Verifying Properties of Space

The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.

Introduction

Much attention has been devoted in Computer Science to formal verification of process behaviour. Several techniques, such as run-time monitoring and model-checking, are based on a formal understanding of system requirements through modal logics. Such logics typically have a temporal flavour, describing the flow of events along time, and are interpreted in various kinds of transition structures.

Recently, aspects of computation related to the distribution of systems in physical space have become more relevant. An example is provided by so called collective adaptive systems 3 , typically composed of a large number of interacting objects. Their global behaviour critically depends on interactions which are often local in nature. Locality immediately poses issues of spatial distribution of objects. Abstraction from spatial distribution may sometimes provide insights in the system behaviour, but this is not always the case. For example, consider a bike (or car) sharing system having several parking stations, and featuring twice as many parking slots as there are vehicles in the system. Ignoring the spatial dimension, on average, the probability to find completely full or empty parking stations at an arbitrary station is very low; however, this kind of analysis may be misleading, as in practice some stations are much more popular than others, often depending on nearby points of interest. This leads to quite different probabilities to find stations completely full or empty, depending on the spatial properties of the examined location. In such situations, it is important to be able to predicate over spatial aspects, and eventually find methods to certify that a given formal model of space satisfies specific requirements in this respect. In Logics, there is quite an amount of literature focused on so called spatial logics, that is, a spatial interpretation of modal logics. Dating back to early logicians such as Tarski, modalities may be interpreted using the concept of neighbourhood in a topological space. The field of spatial logics is well developed in terms of descriptive languages and computability/complexity aspects. However, the frontier of current research does not yet address verification problems, and in particular, discrete models are still a relatively unexplored field.

In this paper, we extend the topological semantics of modal logics to closure spaces. As we shall discuss in the paper, this choice is motivated by the need to use non-idempotent closure operators. A closure space (also called Čech closure space or preclosure space in the literature), is a generalisation of a standard topological space, where idempotence of closure is not required. By this, graphs and topological spaces are treated uniformly, letting the topological and graph-theoretical notions of neighbourhood coincide. We also provide a spatial interpretation of the until operator, which is fundamental in the classical temporal setting, arriving at the definition of a logic which is able to describe unbounded areas of space. Intuitively, the spatial until operator describes a situation in which it is not possible to "escape" an area of points satisfying a certain property, unless by passing through at least one point that satisfies another given formula. To formalise this intuition, we provide a characterising theorem that relates infinite paths in a closure space and until formulas. We introduce a model-checking procedure that is linear in the size of the considered space. A prototype implementation of a spatial model-checker has been made available; the tool is able to interpret spatial logics on digital images, providing graphical understanding of the meaning of formulas, and an immediate form of counterexample visualisation. 4Related work. We use the terminology spatial logics in the "topological" sense; the reader should be warned that in Computer Science literature, spatial logics typically describe situations in which modal operators are interpreted syntactically, against the structure of agents in a process calculus (see [START_REF] Cardelli | Anytime, anywhere: Modal logics for mobile ambients[END_REF][START_REF] Caires | A spatial logic for concurrency (part I)[END_REF] for some classical examples). The object of discussion in this research line are operators that quantify e.g., over the parallel subcomponents of a system, or the hidden resources of an agent. Furthermore, logics for graphs have been studied in the context of databases and process calculi (see [START_REF] Cardelli | A spatial logic for querying graphs[END_REF][START_REF] Gadducci | Graphical encoding of a spatial logic for the pi -calculus[END_REF], and references), even though the relationship with physical space is often not made explicit, if considered at all. The influence of space on agents interaction is also considered in the literature on process calculi using named locations [START_REF] De Nicola | Klaim: A kernel language for agents interaction and mobility[END_REF].

Variants of spatial logics have also been proposed for the symbolic representation of the contents of images, and, combined with temporal logics, for sequences of images [START_REF] Del Bimbo | Symbolic description and visual querying of image sequences using spatio-temporal logic[END_REF]. The approach is based on a discretisation of the space of the images in rectangular regions and the orthogonal projection of objects and regions onto Cartesian coordinate axes such that their possible intersections can be analysed from different perspectives. It involves two spatial until operators defined on such projections considering spatial shifts of regions along the positive, respectively negative, direction of the coordinate axes and it is very different from the topological spatial logic approach.

A successful attempt to bring topology and digital imaging together is represented by the field of digital topology [START_REF] Rosenfeld | Digital topology[END_REF][START_REF] Kong | Digital topology: Introduction and survey[END_REF]. In spite of its name, this area studies digital images using models inspired by topological spaces, but neither generalising nor specialising these structures. Rather recently, closure spaces have been proposed as an alternative foundation of digital imaging by various authors, especially Smyth and Webster [START_REF] Smyth | Discrete spatial models[END_REF] and Galton [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF]; we continue that research line, enhancing it with a logical perspective. Kovalevsky [START_REF] Kovalevsky | Geometry of Locally Finite Spaces: Computer Agreeable Topology and Algorithms for Computer Imagery[END_REF] studied alternative axioms for topological spaces in order to recover well-behaved notions of neighbourhood. In the terminology of closure spaces, the outcome is that one may impose closure operators on top of a topology, that do not coincide with topological closure. The idea of interpreting the until operator in a topological space is briefly discussed in the work by Aiello and van Benthem [START_REF] Aiello | Spatial Reasoning: Theory and Practice[END_REF][START_REF] Van Benthem | Modal logics of space[END_REF]. We start from their definition, discuss its limitations, and provide a more fine-grained operator, which is interpreted in closure spaces, and has therefore also an interpretation in topological spaces. In the specific setting of complex and collective adaptive systems, techniques for efficient approximation have been developed in the form of mean-field / fluid-flow analysis (see [START_REF] Bortolussi | Continuous approximation of collective system behaviour: A tutorial[END_REF] for a tutorial introduction). Recently (see e.g., [START_REF] Chaintreau | The age of gossip: Spatial mean field regime[END_REF]), the importance of spatial aspects has been recognised and studied in this context. In this work, we aim at paving the way for the inclusion of spatial logics, and their verification procedures, in the framework of mean-field and fluid-flow analysis of collective adaptive systems.

Closure spaces

In this work, we use closure spaces to define basic concepts of space. Below, we recall several definitions, most of which are explained in [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF]. Definition 1. A closure space is a pair (X, C) where X is a set, and the closure operator C : 2 X → 2 X assigns to each subset of X its closure, obeying to the following laws, for all A, B ⊆ X:

1. C(∅) = ∅; 2. A ⊆ C(A); 3. C(A ∪ B) = C(A) ∪ C(B).
As a matter of notation, in the following, for (X, C) a closure space, and A ⊆ X, we let A = X \ A be the complement of A in X. Definition 2. Let (X, C) be a closure space, for each A ⊆ X:

1. the interior I(A) of A is the set C(A); 2. A is a neighbourhood of x ∈ X if and only if x ∈ I(A); 3. A is closed if A = C(A) while it is open if A = I(A).
Lemma 1. Let (X, C) be a closure space, the following properties hold: Closure spaces are a generalisation of topological spaces. The axioms defining a closure space are also part of the definition of a Kuratowski closure space, which is one of the possible alternative definitions of a topological space. More precisely, a closure space is Kuratowski, therefore a topological space, whenever closure is idempotent, that is, C(C(A)) = C(A). We omit the details for space reasons (see e.g., [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF] for more information).

1. A ⊆ X is open if and only if A is closed; 2.
Next, we introduce the topological notion of boundary, which also applies to closure spaces, and two of its variants, namely the interior and closure boundary (the latter is sometimes called frontier ). Definition 3. In a closure space (X, C), the boundary of A ⊆ X is defined as

B(A) = C(A)\I(A). The interior boundary is B -(A) = A\I(A), and the closure boundary is B + (A) = C(A) \ A.
Proposition 1. The following equations hold in a closure space:

B(A) = B + (A) ∪ B -(A) (1)
B + (A) ∩ B -(A) = ∅ (2)
B(A) = B(A) (3)
B + (A) = B -(A) (4)
B + (A) = B(A) ∩ A (5) B -(A) = B(A) ∩ A (6)
B(A) = C(A) ∩ C(A) (7)
3 Quasi-discrete closure spaces

In this section we see how a closure space may be derived starting from a binary relation, that is, a graph. The following comes from [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF].

Definition 4. Consider a set X and a relation R ⊆ X × X. A closure operator is obtained from R as C R (A) = A ∪ {x ∈ X | ∃a ∈ A.(a, x) ∈ R}.
Remark 1. One could also change Definition 4 so that C R (A) = A ∪ {x ∈ X | ∃a ∈ A.(x, a) ∈ R}, which actually is the definition of [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF]. This does not affect the theory presented in the paper. Indeed, one obtains the same results by replacing R with R -1 in statements of theorems that explicitly use R, and are not invariant under such change. By our choice, closure represents the "least possible enlargement" of a set of nodes.

Proposition 2. The pair (X, C R ) is a closure space.

Closure operators obtained by Definition 4 are not necessarily idempotent. Lemma 11 in [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF] provides a necessary and sufficient condition, that we rephrase below. We let R = denote the reflexive closure of R (that is, the least relation that includes R and is reflexive).

Lemma 2. C R is idempotent if and only if R = is transitive. Note that, when R is transitive, so is R = , thus C R is idempotent. The vice-versa is not true, e.g., when (x, y) ∈ R, (y, x) ∈ R, but (x, x) / ∈ R. Y Y R Y Y R B B R R B G G B B G G B B B Fig. 1. A graph inducing a quasi-discrete closure space Remark 2.
In topology, open sets play a fundamental role. However, the situation is different in closure spaces derived from a relation R. For example, in the case of a closure space derived from a connected symmetric relation, the only open sets are the whole space, and the empty set.

Proposition 3. Given R ⊆ X × X, in the space (X, C R ), we have:

I(A) = {x ∈ A | ¬∃a ∈ A.(a, x) ∈ R} (8)
B -(A) = {x ∈ A | ∃a ∈ A.(a, x) ∈ R} (9)
B + (A) = {x ∈ A | ∃a ∈ A.(a, x) ∈ R} (10)
We note in passing that [START_REF] Galton | The mereotopology of discrete space[END_REF] provides an alternative definition of boundaries for closure spaces obtained from Definition 4, and proves that it coincides with the topological definition (our Definition 3). Closure spaces derived from a relation can be characterised as quasi-discrete spaces (see also Lemma 9 of [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF] and the subsequent statements). Definition 5. A closure space is quasi-discrete if and only if one of the following equivalent conditions holds: i) each x ∈ X has a minimal neighbourhood 5

N x ; ii) for each A ⊆ X, C(A) = a∈A C({a}). Theorem 1. (Theorem 1 in [17]) A closure space (X, C) is quasi-discrete if and only if there is a relation R ⊆ X × X such that C = C R .

A Spatial Logic for Closure Spaces

In this section we present a spatial logic that can be used to express properties of closure spaces. The logic features two spatial operators: a "one step" modality, turning closure into a logical operator, and a binary until operator, which is interpreted spatially. Before introducing the complete framework, we first discuss the design of an until operator φ Uψ.

The spatial logical operator U is interpreted on points of a closure space. The basic idea is that point x satisfies φ Uψ whenever it is included in an area A satisfying φ, and there is "no way out" from A unless passing through an area B that satisfies ψ. For instance, if we consider the model of Figure 1, yellow nodes satisfy yellow U red while green nodes satisfy green U blue. To turn this intuition into a mathematical definition, one should clarify the meaning of the words area, included, passing, in the context of closure spaces.

In order to formally define our logic, and the until operator in particular, we first need to introduce the notion of model, providing a context of evaluation for the satisfaction relation, as in M, x |= φ Uψ. From now on, fix a (finite or countable) set P of proposition letters. Definition 6. A closure model is a pair M = ((X, C), V) consisting of a closure space (X, C) and a valuation V : P → 2 X , assigning to each proposition letter the set of points where the proposition holds.

When (X, C) is a topological space (that is, C is idempotent), we call M a topological model, in line with [START_REF] Van Benthem | Modal logics of space[END_REF], and [START_REF] Aiello | Spatial Reasoning: Theory and Practice[END_REF], where the topological until operator is presented. We recall it below.

Definition 7. The topological until operator U T is interpreted in a topo- logical model M as M, x |= φ U T ψ ⇐⇒ ∃A open .x ∈ A∧∀y ∈ A.M, y |= φ ∧ ∀z ∈ B(A).M, z |= ψ.
The intuition behind this definition is that one seeks for an area A (which, topologically speaking, could sensibly be an open set) where φ holds, and that is completely surrounded by points where ψ holds. Unfortunately, Definition 7 cannot be translated directly to closure spaces, even if all the used topological notions have a counterpart in the more general setting of closure spaces. Open sets in closure spaces are often too coarse (see Remark 2). For this reason, we can modify Definition 7 by not requiring A to be an open set. However, the usage of B in Definition 7 is not satisfactory either. By Proposition 1 we have

B(A) = B + (A)∪B -(A), where B -(A) is included in A while B + (A) is in A.
For instance, when B is used in Definition 7, we have that the green nodes in Figure 1 do not satisfy green U T blue. Indeed, as we remarked in Example 1, the boundary of the set G of green nodes coincide with the closure of G that contains both green and blue nodes.

A more satisfactory definition can be obtained by letting B + play the same role as B in Definition 7 and not requiring A to be an open set. We shall in fact require that φ is satisfied by all the points of A, and that in B + (A), ψ holds. This allows us to ensure that there are no "gaps" between the region satisfying φ and that satisfying ψ.

Syntax and Semantics of SLCS

We can now define SLCS: a Spatial Logic for Closure Spaces. The logic features boolean operators, a "one step" modality, turning closure into a logical operator, and a spatially interpreted until operator. More precisely, as we shall see, the SLCS formula φ Uψ requires φ to hold at least on one point. The operator is similar to a weak until in temporal logics terminology, as there may be no point satisfying ψ, if φ holds everywhere. Definition 8. The syntax of SLCS is defined by the following grammar, where p ranges over P :

Φ ::= p | | ¬Φ | Φ ∧ Φ | ♦Φ | Φ UΦ
Here, denotes true, ¬ is negation, ∧ is conjunction, ♦ is the closure operator, and U is the until operator. Closure (and interior, see Figure 2) operators come from the tradition of topological spatial logics [START_REF] Van Benthem | Modal logics of space[END_REF]. Definition 9. Satisfaction M, x |= φ of formula φ at point x in model M = ((X, C), V) is defined, by induction on terms, as follows:

M, x |= p ⇐⇒ x ∈ V(p) M, x |= ⇐⇒ true M, x |= ¬φ ⇐⇒ M, x |= φ M, x |= φ ∧ ψ ⇐⇒ M, x |= φ and M, x |= ψ M, x |= ♦φ ⇐⇒ x ∈ C({y ∈ X|M, y |= φ}) M, x |= φ Uψ ⇐⇒ ∃A ⊆ X.x ∈ A ∧ ∀y ∈ A.M, y |= φ∧ ∧∀z ∈ B + (A).M, z |= ψ ⊥ ¬ φ ∨ ψ ¬(¬φ ∧ ¬ψ) φ ¬(♦¬φ) ∂φ (♦φ) ∧ (¬ φ) ∂ -φ φ ∧ (¬ φ) ∂ + φ (♦φ) ∧ (¬φ) φ Rψ ¬((¬ψ) U(¬φ)) Gφ φ U⊥ Fφ ¬G(¬φ)

Fig. 2. SLCS derivable operators

In Figure 2, we present some derived operators. Besides standard logical connectives, the logic can express the interior ( φ), the boundary (∂φ), the interior boundary (∂ -φ) and the closure boundary (∂ + φ) of the set of points satisfying formula φ. Moreover, by appropriately using the until operator, operators concerning reachability (φ Rψ), global satisfaction (Gφ) and possible satisfaction (Fφ) can be derived.

To clarify the expressive power of U and operators derived from it we provide Theorem 2 and Theorem 3, giving a formal meaning to the idea of "way out" of φ, and providing an interpretation of U in terms of paths.

Definition 10. A closure-continuous function f : (X 1 , C 1 ) → (X 2 , C 2 ) is a function f : X 1 → X 2 such that, for all A ⊆ X 1 , f (C 1 (A)) ⊆ C 2 (f (A)).
Definition 11. Consider a closure space (X, C), and the quasi-discrete space (N, C Succ ), where (n, m) ∈ Succ ⇐⇒ m = n+1. A (countable) path in (X, C) is a closure-continuous function p : (N, C Succ ) → (X, C). We call p a path from x, and write p : x ∞, when p(0) = x. We write y ∈ p whenever there is l ∈ N such that p(l) = y. We write p : x A y ∞ when p is a path from x, and there is l with p(l) = y and for all l ≤ l.p(l ) ∈ A. Theorem 2 can be strengthened to a necessary and sufficient condition in the case of models based on quasi-discrete spaces. First, we establish that paths in a quasi-discrete space are also paths in its underlying graph.

Lemma 3. Given path p in a quasi-discrete space (X, C R ), for all i ∈ N with p(i) = p(i + 1), we have (p(i), p(i + 1)) ∈ R, i.e., the image of p is a (graph theoretical, infinite) path in the graph of R. Conversely, each path in the graph of R uniquely determines a path in the sense of Definition 11. Function Sat(M, φ)

Input: Quasi-discrete closure model M = ((X, C), V), SLCS formula φ Output: Set of points {x ∈ X | M, x |= φ} Match φ case : return X case p : return V(p) case ¬ψ : let P = Sat(M, ψ) in return X \ P case ψ ∧ ξ : let P = Sat(M, ψ) in let Q = Sat(M, ξ) in return P ∩ Q case ♦ψ : let P = Sat(M, ψ) in return C(P ) case ψ Uξ : return CheckUntil (M,ψ, ξ)
Algorithm 1: Decision procedure for the model checking problem. Remark 3. Directly from Theorem 3 and from the definitions in Figure 2 we have also that in a quasi-discrete closure model M: Note that, a point x satisfies φ Rψ if and only if either ψ is satisfied by x or there exists a sequence of points after x, all satisfying φ, leading to a point satisfying both ψ and φ. In the second case, it is not required that x satisfies φ.

Model checking SLCS formulas

In this section we present a model checking algorithm for SLCS, which is a variant of standard CTL model checking [START_REF] Baier | Principles of model checking[END_REF]. Function Sat, presented in Algorithm 1, takes as input a finite quasi-discrete model M = ((X, C R ), V) and an SLCS formula φ, and returns the set of all points in X satisfying φ. The function is inductively defined on the structure of φ and, following a bottom-up approach, computes the resulting set via an appropriate combination of the recursive invocations of Sat on the sub-formulas of φ. When φ is , p, ¬ψ or ψ ∧ ξ, definition of Sat(M, φ) is as expected.

Function CheckUntil (M,ψ, ξ) let V = Sat(M, ψ) in let Q = Sat(M, ξ) in var T := B + (V ∪ Q) while T = ∅ do T := ∅ for x ∈ T do N := pre(x) ∩ V V := V \ N T := T ∪ (N \ Q) T := T ; return V
Algorithm 2: Checking until formulas in a quasi-discrete closure space.

To compute the set of points satisfying ♦ψ, the closure operator C of the space is applied to the set of points satisfying ψ.

When φ is of the form ψ Uξ, function Sat relies on the function CheckUntil defined in Algorithm 2. This function takes as parameters a model M and two SLCS formulas ψ and ξ and computes the set of points in M satisfying ψ Uξ by removing from V = Sat(M, ψ) all the bad points. A point is bad if there exists a path passing through it, that leads to a point satisfying ¬ψ without passing through a point satisfying ξ. Let Q = Sat(M, ξ) be the set of points in M satisfying ξ. To identify the bad points in V the function CheckUntil performs a backward search from T = B + (V ∪ Q). Note that any path exiting from V ∪ Q has to pass through points in T . Moreover, the latter only contains points that satisfy neither ψ nor ξ. Until T is empty, function CheckUntil first picks an element x in T and then removes from V the set of (bad) points N that can reach x in one step. To compute the set N we use the function pre(x) = {y ∈ X | (y, x) ∈ R}. 6 At the end of each iteration the set T is updated by considering the set of new discovered bad points.

A model checker for spatial logics

The algorithm described in Section 5 is available as a proof-of-concept tool 7 . The tool, implemented using the functional language OCaml, contains a generic implementation of a global model-checker using closure spaces, parametrised by the type of models. An example of the tool usage is to approximately identify regions of interest on a digital picture (e.g., a map, or a medical image), using spatial formulas. In this case, digital pictures are treated as quasi-discrete models in the plane Z × Z. The language of propositions is extended to simple formulas dealing with colour ranges, in order to cope with images where there are different shades of certain colours.

In Figure 3 we show a digital picture of a maze. The green area is the exit. The blue areas are start points. The input of the tool is shown in Figure 5, where the Paint command is used to invoke the global model checker and colour points satisfying a given formula. Three formulas, making use of the until operator, are used to identify interesting areas. The output of the tool is in Figure 4. The colour red denotes start points from which the exit can be reached. Orange and yellow indicate the two regions through which the exit can be reached, including and excluding a start point, respectively.

In Figure 6 is delimited by main streets, and the delimiting main streets. The output of the tool is shown in Figure 7, where the station area is coloured in orange, the surrounding main streets are red, and other main streets are in green. We omit the source code of the model checking session for space reasons (see the source code of the tool). As a mere hint on how practical it is to use a model checker for image analysis, the execution time on our test image, consisting of about 250000 pixels, is in the order of ten seconds on a standard laptop equipped with a 2Ghz processor.

Conclusions and Future Work

In this paper, we have presented a methodology to verify properties that depend upon space. We have defined an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. The topological definitions have been lifted to a more general setting, also encompassing discrete, graph-based structures. The proposed framework has been extended with a spatial variant of the until operator, and we have also defined an efficient model checking procedure, which is implemented in a proof-of-concept tool.

As future work, we first of all plan to merge the results presented in this paper with temporal reasoning. This integration can be done in more than one way. It is not difficult to consider "snapshot" models consisting of a temporal model (e.g., a Kripke frame) where each state is in turn a closure model, and atomic formulas of the temporal fragment are replaced by spatial formulas. The various possible combinations of temporal and spatial operators, in linear and branching time, are examined for the case of topological models and basic modal formulas in [START_REF] Kontchakov | Spatial logic + temporal logic = ?[END_REF]. Snapshot models may be susceptible to state-space explosion problems as spatial formulas could need to be recomputed at every state. On the other hand, one might be able to exploit the fact that changes of space over time are incremental and local in nature. Promising ideas are presented both in [START_REF] Galton | A generalized topological view of motion in discrete space[END_REF], where principles of "continuous change" are proposed in the setting of closure spaces, and in [START_REF] Kremer | Dynamic topological logic[END_REF] where spatio-temporal models are generated by locally-scoped update functions, in order to describe dynamic systems. In the setting of collective adaptive systems, it will be certainly needed to extend the basic framework we presented with metric aspects (e.g., distance-bounded variants of the until operator), and probabilistic aspects, using atomic formulas that are probability distributions. A thorough investigation of these issues will be the object of future research.

A challenge in spatial and spatio-temporal reasoning is posed by recursive spatial formulas, a la µ-calculus, especially on infinite structures with relatively straightforward generating functions (think of fractals, or fluid flow analysis of continuous structures). Such infinite structures could be described by topologically enhanced variants of ω-automata. Classes of automata exist living in specific topological structures; an example is given by nominal automata (see e.g., [START_REF] Bojanczyk | Automata with group actions[END_REF][START_REF] Gabbay | Freshness and name-restriction in sets of traces with names[END_REF][START_REF] Kurz | On nominal regular languages with binders[END_REF]), that can be defined using presheaf toposes [START_REF] Fiore | Comparing operational models of name-passing process calculi[END_REF]. This standpoint could be enhanced with notions of neighbourhood coming from closure spaces, with the aim of developing a unifying theory of languages and automata describing space, graphs, and process calculi with resources.

  closure and interior are monotone operators over the inclusion order, that is: A ⊆ B =⇒ C(A) ⊆ C(B) and I(A) ⊆ I(B) 3. Finite intersections and arbitrary unions of open sets are open.

Example 1 .

 1 Every graph induces a quasi-discrete closure space. For instance, we can consider the (undirected) graph depicted in Figure 1. Let R be the (symmetric) binary relation induced by the graph edges, and let Y and G denote the set of yellow and green nodes, respectively. The closure C R (Y ) consists of all yellow and red nodes, while the closure C R (G) contains all green and blue nodes. The interior I(Y ) of Y contains a single node, i.e. the one located at the bottom-left in Figure 1. On the contrary, the interior I(G) of G is empty. Indeed, we have that B(G) = C(G), while B -(G) = G and B + (G) consists of the blue nodes.

Theorem 2 .

 2 If M, x |= φ Uψ, then for each p : x ∞ and l, if M, p(l) |= ¬φ, there is k ∈ {1, . . . , l} such that M, p(k) |= ψ.

Theorem 3 .

 3 In a quasi-discrete closure model M, M, x |= φ Uψ if and only if M, x |= φ, and for each path p : x ∞ and l ∈ N, if M, p(l) |= ¬φ, there is k ∈ {1, . . . , l} such that M, p(k) |= ψ.

1 .

 1 M, x |= φ Rψ iff. there is p : x ∞ and k ∈ N such that M, p(k) |= ψ and for each j ∈ {1, . . . , k} M, p(j) |= φ; 2. M, x |= Gφ iff. for each p : x ∞ and i ∈ N, M, p(i) |= φ; 3. M, x |= Fφ iff. there is p : x ∞ and i ∈ N such that M, p(i) |= φ.

Lemma 4 .

 4 Let X a finite set and R ⊆ X × X. For any finite quasidiscrete model M = ((X, C R ), V) and SLCS formula φ with k operators, Sat terminates in O(k • (|X| + |R|)) steps.

Theorem 4 .Fig. 4 .

 44 Fig. 3. A maze.

  we show a digital image 8 depicting a portion of the map of Pisa, featuring a red circle which denotes a train station. Streets of different importance are painted with different colors in the map. The model checker is used to identify the area surrounding the station which Let reach(a,b) = !( (!b) U (!a) ); Let reachThrough(a,b) = a & reach((a|b),b); Let toExit = reachThrough(["white"],["green"]); Let fromStartToExit = toExit & reachThrough(["white"],["blue"]); Let startCanExit = reachThrough(["blue"],fromStartToExit); Paint "yellow" toExit; Paint "orange" fromStartToExit; Paint "red" startCanExit;

Fig. 5 .

 5 Fig. 5. Input to the model checker.

Fig. 6 . 7 .

 67 Fig. 6. Input: the map of a town. Fig. 7. Output of the tool.

Due to lack of space all the proofs are omitted and can be found in[START_REF] Ciancia | Specifying and verifying properties of space -extended version[END_REF].

A minimal neighbourhood of x is a set that is a neighbourhood of x (Definition 2 (2)) and is included in all other neighbourhoods of x.

Function pre can be pre-computed when the relation R is loaded from the input.

Web site: http://www.github.com/vincenzoml/slcs.

c OpenStreetMap contributorshttp://www.openstreetmap.org/copyright.

Research partially funded by EU ASCENS (nr. 257414), EU QUANTICOL (nr. 600708), IT MIUR CINA and PAR FAS 2007-2013 Regione Toscana TRACE-IT. 3 See e.g. the web site of the QUANTICOL project: http://www.quanticol.eu