Spatial logics and model checking for medical imaging

Abstract

Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces—closure spaces being a generalisation of topological spaces, covering also discrete space structures—and topochecker, a model checker for SLCS (and extensions thereof). We introduce the logical language ImgQL (“Image Query Language”). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distance-based operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our approach by means of an example of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema.

1 Introduction

Computer Science plays a fundamental role in the field of medical image analysis. Computational methods are currently in use for several different purposes, such as: computer-aided diagnosis (CAD), aiming at the classification of areas in images, based on the presence of signs of specific diseases [34]; Image Segmentation, tailored to identify areas that exhibit specific features or functions (such as organs or sub-structures) [43]; Automatic contouring of Organs at Risk or target volumes for radiotherapy applications [12]; Identification of indicators, computed from the acquired images, enabling early diagnosis, or understanding of microscopic characteristics of specific diseases, or helping in the identification of prognostic factors to predict a treatment output [18, 77] (examples of indicators are the mean diffusivity and the fractional anisotropy obtained from Magnetic Resonance (MR) Diffusion-Weighted Images, or the magnetisation transfer ratio maps obtained from a Magnetisation Transfer acquisition [32, 55]).

Such kinds of analyses are strictly tied to the spatial features of images.

In this paper, we focus on image segmentation, in particular to identify glioblastomas which are the most common malignant intracranial tumours. For the treatment of glioblastomas, neuroimaging protocols are used before and after treatment to evaluate the effect of treatment strategies and to monitor the evolution of the disease. In clinical studies and routine treatment, magnetic resonance images (MRI) are evaluated based mostly on qualitative criteria such as the presence of hyperintense tissue appearing in the images [60]. The study and development of automatic and semi-automatic segmentation algorithms are aiming at overcoming the current time-consuming practise of manual delineation of such tumours and at providing an accurate, reliable and reproducible method of segmentation of the tumour area and related tissues [35].

Segmentation of medical images, and brain segmentation in particular, is nowadays an important topic on its own in many applications in neuroimaging; several automatic and semi-automatic methods have been proposed, constituting a very active research area (see for example [33, 35, 38, 54, 72, 80]). Segmentation methods are often divided into two broad categories [60]: generative models, which rely on domain-specific prior knowledge about the appearance of specific brain tissues and anatomy, and discriminative models, which exploit little prior knowledge and instead rely mostly on the extraction of a large number of low-level image features such as local histograms, texture features and raw input pixel values. Among the main principles of segmentation algorithms is the exploitation of the variation of grey-scale intensity and texture of images. These features are then used in a wide range of fully automatic and semi-automatic techniques. Among them, we find techniques such as region growing, deformable templates, thresholding and pattern recognition techniques like adaptive fuzzy clustering, artificial neural networks, particle swarm optimisation and random forest. There are also hybrid techniques in which several such techniques are combined. Semi-automatic techniques include fuzzy cognitive maps, support vector machines and neural networks. For further details on the enormous variety of proposed techniques and their performance in terms of accuracy and time complexity, we refer to the following surveys [8, 60, 62]. At the time of writing, the state of the art in automated segmentation of brain tumours, which is our running example, is almost entirely constituted by various machine learning methods¹. One of the technical challenges of the development of automated (brain) tumour segmentation is that lesion areas are only defined through changes in the intensity (luminosity) in the (black & white) images that are relative to surrounding normal tissue. Even manual segmentation by experts shows significant variations when intensity gradients between adjacent tissue structures are smooth or partially obscured [60]. Furthermore, there is a considerable variation across images from different patients and images obtained with different MRI scanners.

In this paper, we propose a novel approach to image segmentation, namely an interactive, logic-based method, supported by spatial model checking, tailored to loosely identify a region of interest in MRI on which to focus the analysis of glioblastoma or other types of tumours. This approach is particularly suitable to exploit the relative spatial relations between tissues of interest mentioned earlier. With respect to the aforementioned categories, our approach is that of a hybrid methodology in which the different segmentation methods (such as texture features, local histogram processing, and prior knowledge) can be freely combined and nested, since they are mapped to operators of a domain-specific language for image analysis.

Spatial and Spatio-temporal logics and model checking are the subject of a recent trend in Computer Science (see for instance [22,23,24, 31, 45, 46, 64]) that uses specifications written in logical languages describing space—called spatial logics—to automatically identify patterns and structures of interest in a variety of domains, ranging from Collective Adaptive Systems [20, 25, 26] to signals [64] and images [23, 46].

The research presented in the present paper stems from the topological approach to spatial logics, dating back to the work of Alfred Tarski, who first recognised the possibility of reasoning on space using topology as a mathematical framework for the interpretation of modal logic (see [78] for a thorough introduction). In this context, formulas are interpreted as sets of points of a topological space, and in particular the modal operator $\diamond$ is usually interpreted as the (logical representation of the) topological closure operator. A standard reference is the Handbook of Spatial Logics [3]. Therein, several spatial logics are described, with applications far beyond topological spaces; such logics treat not only aspects of morphology, geometry and distance, but also advanced topics such as dynamic systems, and discrete structures, that are particularly difficult to deal with from a topological perspective (see, for example [39]); in addition, the idea of investigating a spatial, topological, interpretation of the temporal logic until operator is discussed (see [78]). In recent work [22, 23], Ciancia et al. pushed such theoretical developments further to encompass arbitrary graphs as models of space, by choosing Closure spaces, a generalisation of topological spaces [39, 40], as underlying model for the logic. This resulted in the definition of the Spatial Logic for Closure Spaces (SLCS), and a related model checking algorithm. SLCS includes both the closure modality $\diamond$—denoted by ${\mathcal {N}}$ (to be read for “near”) for avoiding confusion—and a spatial until operator—denoted by ${\mathcal {S}}$ (to be read “surrounded”); a point satisfies $\varPhi _1 \; {\mathcal {S}}\; \varPhi _2$ if it satisfies $\varPhi _1$ and there is no way for moving away to a point not satisfying $\varPhi _1$ without first passing by a point satisfying $\varPhi _2$, i.e. the points satisfying $\varPhi _1$ are surrounded by points satisfying $\varPhi _2$. Subsequently, in [21], a spatio-temporal logic, combining Computation Tree Logic and the newly defined spatial operators, was introduced; the (extended) model checking algorithm has been implemented in the prototype spatio-temporal model checkertopochecker.²

The broader aim of our research in the context of medical imaging is to enable the declarative description and automatic or semi-automatic, efficient identification of regions in images using spatial logic formulas. This is possible by considering such images as instances of (quasi-discrete) closure spaces. The tools and methods we introduce can be used both for two-dimensional (2D) and three-dimensional (3D) MI; we remark that modern MRI machines can usually provide 3D data for analysis; however, in standard practice, 3D information is often discarded in favour of 2D (slice by slice) analysis, due to the lack of well-established methods for 3D analysis. Using 3D information may lead to improved accuracy, and it is therefore of high interest, in current research, to identify techniques for this purpose.

1.1 Original contributions

This paper details and extends the ideas outlined in [9], providing several further original contributions:

• extension of the spatial logic SLCS to ImgQL, introducing distance-based operators and showing their formal relation to the other spatial logic operators of SLCS. A novel approach to model checking of distance-based operators is provided based on so-called distance transforms, that forms the basis for the definition an efficient algorithm to solve the model checking problem. Asymptotic time complexity of the procedure we propose is linear or quasi-linear, depending on the kind of distance used. This result makes such procedure suitable for the analysis of higher resolution or 3D images;

• introduction of a novel logical connective aimed at estimating similarity between regions. This operator is based on statistical texture analysis and is able to classify points of the space based on the similarity between the area where they are localised, and a target region, expressed in logical terms. The connective is specific for medical image analysis. Its embedding shows how such connectives can be integrated into the spatial logic. This provides an example of how other specialised existing algorithms could be introduced and exploited within the spatial logic model checking framework;

• enhancement of the results in the glioblastoma case study first introduced in [9], providing the relevant technical details on the logical specification;

• development of efficient model checking algorithms, that are competitive in computational efficiency w.r.t. state-of-the-art (semi-)automatic segmentation approaches.

A major advantage of our formal verification approach, with respect to the state of the art in (semi-)automated segmentation, is that logical specifications are transparent, reproducible, accurate, human readable, and applicable to both 2D and 3D images.

Texture analysis, distance, and reachability in space can be freely combined as high-level logical operators with a clear and well-defined topological semantics. The interplay of these aspects is the key to obtain our experimental results. The work in [9] constituted a first proof-of-concept study. In that study, topochecker was used for the declarative specification of regions in medical images. The model checker was used to automatically and efficiently identify and colour glioblastoma and the surrounding oedema in MRI scans, on the basis of a declarative definition of the two regions of interest, given in terms of their visual appearance. The latter is defined by image features such as proximity, interconnection, and texture similarity. The input to the model checker consists of a precise, declarative, unambiguous logical specification, that besides being fairly close to the level of abstraction of an expert description of the process, is also remarkably concise, human readable, robust and reproducible.

1.1.1 Related work

The idea of using model checking, and in particular spatial or spatio-temporal model checking, for the analysis of medical images is relatively recent and there are only a few articles exploring this field so far. In particular, [74] uses spatio-temporal model checking techniques inspired by [45]—pursuing machine learning of the logical structure of image features—for the detection of tumours. In contrast, our approach is more focused on human-intelligible logical descriptions that can be reused and extended. Other interesting work is that in [66] where spatio-temporal meta model checking is used for the analysis of biological processes, with an interesting focus on multi-scale aspects.

Among the fully automated approaches that recently are gaining interest are those based on machine learning and, in particular, deep learning (see for example [4] for a recent review). Although manual segmentation is still the standard for in vivo images, this method is expensive and time-consuming, difficult to reproduce and possibly inaccurate due to human error. Machine learning and deep learning approaches have shown promising results in pattern recognition in areas where large, reliable datasets are available and are currently being developed for application in MRI based brain segmentation with the aim to obtain reliable automatic segmentation methods. Deep learning is based on the use of artificial neural networks, consisting of several layers, that can extract a hierarchy of features from raw input data. These methods depend heavily on the availability of large training datasets. Furthermore, some machine learning approaches require the generation of manual ground truth labels, i.e. data sets in which segments of interest are indicated by experts manually in a standard way. This is a complicated task not only because it is very laborious, but also because of the relatively high intra-expert and inter-expert variability of 20±15% and 28±12%, respectively, for manual segmentations of brain tumour images [59]. Interactive approaches based on spatial model checking may therefore also be of help to improve the generation of manual ground truth labels in a more efficient, transparent, and reproducible way.

Spatial (and spatio-temporal) model checking is a relatively new area of research, so that there are not that many proposals available in the literature. In [63], SSTL, a spatial extension of the linear time, time-bounded, Signal Temporal Logic (STL), is presented which provides a logical framework for reasoning about (stochastic) population models where agents live—and move around—in a discrete patch-based representation of space, i.e. a finite (cost-)weighted graph. The logic has a single spatial operator, namely the bounded somewhere operator, $_{I}\varPhi$—reminiscent of the somewhere operator of [67]—which requires $\varPhi$ to hold in a location reachable from the current one with a total cost falling in interval I. A monitoring—rather than model checking—algorithm is also provided, extending the similar algorithm for STL with the spatial component. In [64, 65], some of the co-authors of the present paper, jointly with Nenzi et al. proposed an extension of SSTL with a bounded surrounded operator ${\mathcal {S}}_I$ which, in turn, extends the surrounded operator of [22, 23] with the additional requirement that, in order for a point x to satisfy $\varPhi _1 \; {\mathcal {S}}_I \; \varPhi _2$, it must also be the case that the length of the shortest path from x to the “boundary” $\varPhi _2$ must fall in I. Finally, in [5], an alternative characterisation of the bounded surrounded operator is proposed, which defines it as derived from a (basic) reachability operator and a new operator, called escape. Note that in [22, 23], reachability is available in turn as a derived operator—namely, the dual of ${\mathcal {S}}$.

1.1.2 Outline

A technical introduction to spatial logics and distance-based operators is provided in Sect. 2. Syntax and semantics of the fragment of SLCS we will use in this paper are recalled, as well as the main notions of spatial model checking for the fragment. The definition of a distance operator for ImgQL is presented in Sect. 3 together with the related extension of the model checking algorithm. In Sect. 4, the logic framework we propose for statistical texture analysis is presented. Section 5 briefly describes the tool topochecker, and provides the results of some benchmarks of its spatial analysis capabilities. In Sect. 6, the glioblastoma case study is presented in detail, including a first assessment of validation. Some concluding remarks are provided in Sect. 7.

2 Logics for closure spaces

In this section, we discuss the background knowledge that we use in the technical developments of the paper. In particular, we briefly introduce the notion of closure spaces, the fragment of SLCS [22, 23] we use in this paper, and the related model checking algorithm.

In the sequel, we will often make explicit reference to 2D images and their pixels; here, we point out that this is done only for the sake of simplicity and that all notions, notations, definitions, and results equally apply to 3D images and their voxels (i.e. volumetric picture elements, the 3D counterpart of pixels).

2.1 Closure spaces, spatial logics, and model checking

In spatial logics, modal operators are interpreted using the concept of neighbourhood in a topological space, enabling one to reason about points of the space using familiar concepts such as proximity, distance, or reachability. A comprehensive reference for these theoretical developments is [3]. Transferring the results in the field to applications, and in particular to model checking, requires one to use finite models. However, finite topological spaces are not satisfactory in this respect; for instance, they cannot encode arbitrary graphs, including e.g. those with a non-transitive/non-symmetric edge relation, that may be the object of spatial reasoning in several applications (for instance, consider the graph of roads in a town, including the one-way streets). Extending topological spaces to closure spaces (see [39]) is the key to generalise these results. In this paper, we use a fragment of SLCS comprising an operator, called near, interpreted as proximity, and the surrounded connective, which is a spatial variant of the classical temporal weak until operator, able to characterise unbounded areas of space, based on their boundary properties. The surrounded connective is similar in spirit to the spatial until operator for topological spaces discussed by Aiello and van Benthem in [2, 78], although it is interpreted in closure spaces. Several derived operators may be defined, among which, notably, variants of the notion of reachability in space. The combination of SLCS with temporal operators from the well-known branching time logic CTL (Computation Tree Logic) [28] has been explored in [21]. Some related case studies have been analysed in [19, 26] where the logic caters for spatio-temporal reasoning and model checking. In the present paper, we focus on spatial properties; therefore, we restrict our attention to spatial aspects of our framework.

2.2 A fragment of SLCS

SLCS is a logic for space, where the latter is modelled by means of closure spaces. Before introducing the fragment of SLCS we use in the present paper, we recall some basic notions of closure spaces [39, 40].

Definition 1

A closure space is a pair $(X,{\mathcal {C}})$ where X is a non-empty set (of points) and ${\mathcal {C}}: 2^X \rightarrow 2^X$ is a function satisfying the following three axioms:

• 1. ${\mathcal {C}}(\emptyset )=\emptyset$;

• 2. $Y \subseteq {\mathcal {C}}(Y)$ for all $Y \subseteq X$;

• 3. ${\mathcal {C}}(Y_1 \cup Y_2) = {\mathcal {C}}(Y_1) \cup {\mathcal {C}}(Y_2)$ for all $Y_1,Y_2\subseteq X$. $\square$

According to the well-known Kuratowski definition, adding the idempotence axiom${\mathcal {C}}({\mathcal {C}}(Y))={\mathcal {C}}(Y)$ for all $Y \subseteq X$ in Definition 1 makes it a definition of topological spaces [40]. Consequently, the latter are a subclass of closure spaces.

Given any relation $R\subseteq X \times X$, function ${\mathcal {C}}_{R}:2^X \rightarrow 2^X$ with ${\mathcal {C}}_{R}(Y) = Y\cup \{x | \exists y \in Y. y \, R\,x\}$ satisfies the axioms of Definition 1 thus making $(X,{\mathcal {C}}_{R})$ a closure space. The class of closure spaces generated by binary relations on the set of points represent a very interesting subclass of closure spaces, known as quasi-discrete closure spaces. Quasi-discrete closure spaces include discrete structures like graphs, where each graph $(X,R)$ with set of nodes X and set of the edges $R$ is in one-to-one correspondence with closure space $(X,{\mathcal {C}}_{R})$. Clearly, finite closure spaces are quasi-discrete closure spaces.

The following definition is instrumental for the definition of paths over quasi-discrete closure spaces.

Definition 2

A continuous function$f : (X_1, {\mathcal {C}}_1) \rightarrow (X_2, {\mathcal {C}}_2)$ is a function $f : X_1\rightarrow X_2$ such that, for all $Y \subseteq X_1$, we have $f({\mathcal {C}}_1(Y)) \subseteq {\mathcal {C}}_2(f(Y))$. $\square$

In the definition below, $({\mathbb {N}}, {\mathcal {C}}_{Succ})$ is the closure space of natural numbers with the successor relation: $(n,m) \in Succ \Leftrightarrow m=n+1$.

Definition 3

A path$\pi$ in $(X,{\mathcal {C}}_{R})$ is a continuous function $\pi : ({\mathbb {N}}, {\mathcal {C}}_{Succ}) \rightarrow (X,{\mathcal {C}}_{R})$. $\square$

The elements of ${\mathbb {N}}$ will be called indexes in the context of paths.

A quasi-discrete closure space $(X,{\mathcal {C}}_{R})$ can be used as the basis for a mathematical model of a 2D digital image; X represents the finite set of pixels, and $R$ is the reflexive and symmetric adjacency relation between pixels [41]. We note in passing that several different adjacency relations can be used. For instance, in the orthogonal adjacency relation (sometimes called von Neumann adjacency) only pixels which share an edge count as adjacent, so that each pixel is adjacent to (itself and) four other pixels; on the other hand, in the orthodiagonal adjacency relation pixels are adjacent as long as they share at least either an edge or a corner, so that each pixel is adjacent to (itself and) eight other pixels. Pixels are usually associated with specific attributes, such as colours and/or colour-intensity. We model this by assuming that a set $A$ of point attribute names is given and by enriching $(X,{\mathcal {C}}_{R})$ with an attribute evaluation function $\mathcal{A}:X \times A\rightarrow V$ from points and their attributes to some value set V such that $\mathcal{A}(x,a) \in V$ is the value of attribute a of point x. For given set $P$ of atomic predicatesp, the syntax of the fragment of SLCS we use in this paper is given in Fig. 1.

Fig. 1

Syntax of the fragment of SLCS

Informally, it is assumed that space is modelled by a set of points; each atomic predicate $p \in P$ models a specific feature of points and is thus associated with the set of points which have this feature. A point x satisfies ${\mathcal {N}}\; \varPhi$ if a point satisfying $\varPhi$ can be reached from x in at most one (closure) step, i.e. if x is near (or close) to a point satisfying $\varPhi$. A point x satisfies $\varPhi _1 \; {\mathcal {S}}\; \varPhi _2$ if it satisfies $\varPhi _1$ and in any path $\pi$ rooted in x (i.e. such that $\pi (0)=x$) and passing through a point $\pi (\ell )$not satisfying $\varPhi _1$, there is a point $\pi (j)$ before or at $\ell$ (i.e. $0 < j \le \ell$) that satisfies $\varPhi _2$. In other words, x belongs to an area satisfying $\varPhi _1$ and one cannot escape from such an area without hitting a point $\varPhi _2$, i.e. x is surrounded by $\varPhi _2$. Finally, the fragment includes logical negation ($\lnot$) and conjunction ($\wedge$).

The above description is formalised by the definition of model and satisfaction relation:

Definition 4

A closure model is a tuple $((X,{\mathcal {C}}), \mathcal{A}, \mathcal{V})$ consisting of a closure space $(X,{\mathcal {C}})$, a valuation $\mathcal{A}: X \times A\rightarrow V$, assigning to each point and attribute the value of the attribute at that point, and a valuation $\mathcal{V}: P\rightarrow 2^X$ assigning to each atomic predicate the set of points where it holds. $\square$

In the sequel, we assume that an atomic predicate p can be bound to an assertion $\alpha$, the latter stating a property of attributes, and we use the syntax $p:=\alpha$ for atomic predicate definitions, to this purpose. Assertions are standard Boolean expressions, e.g. comparisons of the form $a \ge c$, for $c \in V$, and compositions thereof; we refrain from specifying the actual syntax of assertions, and we assume valuation $\mathcal{A}$ be extended in the obvious way in order to evaluate assertions, e.g. $\mathcal{A}(x,a \ge c) = \mathcal{A}(x,a)\ge c$.

Definition 5

Satisfaction${\mathcal {M}}, x \models \varPhi$ at point $x \in X$ in model ${\mathcal {M}}= ((X,{\mathcal {C}}), \mathcal{A}, \mathcal{V})$ is defined by induction on the structure of formulas, as in Fig. 2. $\square$

Fig. 2

Satisfaction relation for the fragment of SLCS; whenever $p:=\alpha$ is a definition for p, we assume $x\in \mathcal{V}(p)$ if and only if $\mathcal{A}(x,\alpha )$ yields the truth-value true

Fig. 3

An example model: a the points satisfying atomic predicate p are shown in violet, those satisfying q are shown in yellow; the points satisfying $\lnot {\mathcal {N}}q$ (b), those satisfying $q \; {\mathcal {S}}\; p$ (c), and those satisfying $p \; \mathcal{T}\lnot ({\mathcal {N}}\; q)$ (d) are shown in green (colour figure online)

Fig. 4

Some derived operators

In Fig. 3a, a simple finite closure model is shown for which the orthogonal adjacency relation is assumed. All the points satisfying atomic predicate p are shown in violet, whereas those satisfying q are shown in yellow (no point satisfies $p \wedge q$ in this example). Figure 3b shows in green the points that satisfy $\lnot {\mathcal {N}}q$, while Fig. 3c shows in green the points satisfying $q \; {\mathcal {S}}\; p$ (i.e. all q-points that are surrounded by p-points; note that, in the example, these are exactly allq-points).

A number of useful derived operators are defined in Fig. 4. A few words of explanation are worth for the $\mathcal{T}$ operator, while we refer the reader to [23] for a general discussion on SLCS derived operators. A point satisfies $\varPhi _1 \; \mathcal{T}\; \varPhi _2$ if and only if it lays in an area $Y_1 \subseteq X$ the points of which satisfy $\varPhi _1$ and $Y_1$ “touches” a non-empty area $Y_2$, the points of which satisfy $\varPhi _2$; for this reason, sometimes we call the From-To operator “touches”. Figure 3d shows in green the points satisfying $p \; \mathcal{T}\lnot ({\mathcal {N}}\; q)$. A useful pattern, that may be used for filtering noise in images, is formula ${\mathcal {N}}\; {\mathcal {I}}\;\varPhi$. The effect of such a formula is to capture the regular region [52] included in the set of points satisfying $\varPhi$; point x satisfies ${\mathcal {N}}\; {\mathcal {I}}\;\varPhi$ if and only if it is adjacent to at least one point y satisfying $\varPhi$ which, in turn, is not adjacent to points satisfying $\lnot \;\varPhi$. The effect of such a filter is to eliminate small regions, e.g. those consisting of a single point, when these are considered noise or artefacts.

2.3 Model checking SLCS

In this section, we will briefly recall model checking of SLCS [22, 23] over finite models. Note that, in the context of the present paper, we are concerned with so-called global model checking, i.e. a procedure that, given a finite model and a logic formula, returns the set of all points in the model satisfying the formula [29]. More precisely, the model checking algorithm computes a function $\mathtt {Sat}$ such that, for every finite closure model ${\mathcal {M}}= ((X,{\mathcal {C}}_{R}), \mathcal{A}, \mathcal{V})$ and formula $\varPhi$, we have $\mathtt {Sat}(\varPhi )=\{x\in X | {\mathcal {M}}, x \models \varPhi \}$. The algorithm uses recursion on the structure of the formulas and is sketched in Fig. 5. In the present paper, we will focus on the surrounded operator only and we will describe the related section of the model checking algorithm by means of an example. The details of model checking for the other operators are a matter of standard routine and can be found in [22, 23].

Fig. 5

Sketch of the model checking algorithm for computing the set $\mathtt {Sat}({\mathcal {M}},\varPhi )$ of points in X satisfying $\varPhi$

For a formula $\varPhi _1 \; {\mathcal {S}}\; \varPhi _2$ the algorithm, roughly speaking, first identifies areas of bad points, that is points that can reach a point satisfying $\lnot \varPhi _1$ without passing by a point satisfying $\varPhi _2$; then returns the points that satisfy $\varPhi _1$ and that are not bad.

Fig. 6

Model checking $yellow \;{\mathcal {S}}\; pink$: a input model; b set $\{x | {\mathcal {M}},x\models \lnot (yellow \vee pink)\}$; c set $\{x | {\mathcal {M}},x\models yellow\} \cap {\mathcal {C}}_{R}(blue)$; e set $\{x | {\mathcal {M}},x\models yellow\} \cap {\mathcal {C}}_{R}(blue)_{6d}$ (colour figure online)

Below, we give a brief description of how the algorithm works, using the graphs shown in Fig. 6. Let us consider the model of Fig. 6a as input model, where points are represented by coloured squares and the adjacency relation is the orthogonal one. In this example, we assume that the set of atomic predicates is the set $\{pink, yellow, white\}$—represented in the figure in the obvious way—and that $\mathcal{V}(p) \cap \mathcal{V}(p') = \emptyset$ whenever $p\not = p'$. Suppose the input formula is $yellow \;{\mathcal {S}}\; pink$. The result of the assignment Bad := TempBad of the first iteration of the repeat is shown in Fig. 6b, where all nodes that satisfy $\lnot (yellow \vee pink)$ are marked blue. Note that this blue-colouring is not part of the model; we use it at a “meta-level” and only for describing the behaviour of the algorithm; the same will apply to points marked in cyan in the sequel. In Fig. 6c, the (only two) yellow points in the closure of the points indicated in blue are shown in cyan³; these are the points to be selected for being added to TempBad in the first iteration of the repeat. The new value of TempBad, resulting from the assignment, consists of all blue points of Fig. 6d. The body of the repeat is executed now with the new value of TempBad. In Fig. 6e, the (again only two) yellow points in the closure of the set of points in blue are shown in cyan. Note that such a closure refers to the model of Fig. 6d; this is abbreviated in Fig. 6e as ${\mathcal {C}}_{R}(blue)_{6d}$. The new value of TempBad, resulting from the assignment, consists of all points indicated in blue in Fig. 6f. The body of the repeat is executed now for the third time, and this results in no change in the value of TempBad: the fixed point is reached, the repeat block is exited and the points satisfying $yellow \;{\mathcal {S}}\; pink$ are the four yellow points in the bottom-left corner of Fig. 6f. In [23], it has been shown that, for any finite closure model ${\mathcal {M}}= ((X,{\mathcal {C}}_{R}), \mathcal{A}, \mathcal{V})$ and SLCS formula $\varPhi$ of size k, the model checking procedure terminates in ${{\mathcal {O}}}(k\cdot (|X| + |R|))$ steps.⁴

3 Incorporating distance

In this section, we detail the use of so-called distance operators in our research line, and we extend the logic fragment with a distance operator parametric on the specific notion of distance; we also give an account of the extension of the model checking algorithm necessary for the efficient implementation of the distance operator, based on the notion of distance transform.

Models of space as well as spatial logics can be extended with notions of distance (see e.g. [52, 53, 63, 64]). Distances are very often expressed using the non-negative real numbers ${\mathbb {R}}_{\ge 0}$, like the Euclidean distance on continuous space.

For quasi-discrete closure spaces, especially when used as a representation of finite graphs, it is natural to consider shortest-path distance, where a path between two nodes is a sequence of consecutive edges connecting the first node to the second, and its length is given by the sum of the lengths of such edges. The length of an edge is often taken to be 1; however, other notions of distance can be more appropriate. For example, sampling a multi-dimensional Euclidean space is often done using a regular grid, that is, a graph in which the nodes are arranged on multiples of a chosen unit interval that may vary along each dimension of the space. Nodes are connected by edges using a chosen notion of adjacency (e.g. the orthogonal or orthodiagonal adjacency relations discussed before, but any choice may be reasonable, depending on the application context). Such graphs can then be weighted by associating with each edge the Euclidean distance between the nodes it connects. Graphs with nodes in a Euclidean space and weighted by Euclidean distance are known as Euclidean graphs and are naturally equipped with both Euclidean distance between nodes and (weighted) shortest-path distance—which is also called Chamfer distance in the particular case of Euclidean graphs with nodes arranged on a regular grid, which is the case of interest for MI. In two-dimensional imaging, pixels—with an application-dependent choice of adjacency—form a Euclidean graph, and Euclidean distance is the reference distance between (the centres of) two pixels.

Euclidean and Chamfer distances obviously divert, no matter how fine is the grid or how many neighbours are chosen in the adjacency relation, unless all pairs of nodes are linked by an edge (labelled with the Euclidean distance between the end-points of the edge). Therefore, in this context, Euclidean distance is considered error-free, and Chamfer distance is considered an approximation of the former. The chosen adjacency relation determines the precision-efficiency trade-off of the computed distance: the more pixels are considered adjacent, the more precise is the approximation, at the expenses of generating graphs with larger out-degrees. This is illustrated in Figs. 7 and 8. In the first figure, we show a two-dimensional, rectangular image where all and only points at a Euclidean distance larger than a given threshold k from the centre of the figure are coloured in red. In Fig. 8a, the points in red are those at a Chamfer distance larger than k from the centre; in particular, orthodiagonal adjacency has been used (each pixel has 8 other adjacent pixels). Figure 8b shows the percentage of error for each pixel with respect to the Euclidean distance, in a scale from 0 to $10\%$. Finally, in Fig. 8c we use Chamfer distance, the same threshold k and an adjacency relation where each pixel has 24 other adjacent pixels (i.e. the pixels that are adjacent to any pixel form a $5 \times 5$ square centred in the pixel). Figure 8d shows the percentage of error w.r.t. the Euclidean distance, in a scale from 0 to $2\%$. The percentage error $\delta (x)$ for Chamfer distance $d_C$ is defined for each pixel x as $\delta (x)=\frac{\left| d_E(y,x)-d_C(y,x)\right| }{d_E(y,x)}$, where y is the central point of the image and $d_E$ denotes the Euclidean distance.

Fig. 7

Threshold imposed on Euclidean distance from a point in the centre of image

Fig. 8

Percentage error of Chamfer distance: a Chamfer distance with 8 adjacent pixels per node, i.e. $3\times 3$ square centred on node; b percentage error, scale: 0–10; c Chamfer distance with 24 adjacent pixels per node, i.e. $5\times 5$ square centred on node; d percentage error, scale: 0–2

3.1 SLCS with distance operators

In this section, we extend the fragment of SLCS presented in Sect. 2.2 with logic distance operators. We first introduce the notion of distance closure spaces and, to that purpose we recall the well-known notion of metric space:

Definition 6

A metric space is a pair (X, d) where X is a non-empty set (of points) and $d: X \times X \rightarrow {\mathbb {R}}_{\ge 0}$ is function that satisfies the following axioms, for all $x,y,z \in X$:

• 1. $d(x,y)=0$ iff $x=y$[identity of indiscernible];

• 2. $d(x,y)=d(x,y)$[symmetry];

• 3. $d(x,z) \le d(x,y) + d(y,z)$[triangle inequality].

Whenever X is a closure space $(X,{\mathcal {C}})$, $((X,{\mathcal {C}}),d)$ is called a metric closure space.$\square$

Metric functions are easily extended to sets as follows:

Definition 7

Given metric space (X, d), $x \in X$ and $Y, Z \subseteq X$ we let

• 1. $d(x,Y) = \inf \{d(x,y) | y \in Y\}$

• 2. $d(Y,Z) = \inf \{d(y,z) | y \in Y \text{ and } z \in Z\}$

Note that if $Y\not =\emptyset$ is finite, then $\inf \{d(x,y) | y \in Y\} = \min \{d(x,y) | y \in Y\}$; we let $d(x,\emptyset ) =\infty$ by definition. $\square$

In the case of quasi-discrete closure spaces, symmetry may turn out to be too much restrictive. This is for instance the case when the relation $R$ underlying the closure operator ${\mathcal {C}}_{R}$ is not symmetric. Similarly, the triangle inequality is not fitting well when more qualitative distance “measures” are used, for instance when the codomain of d is composed of only three values, representing short, medium, and large distance, respectively. For all these reasons, for quasi-discrete closure spaces we often use the less restrictive notion of distance space, where only Axiom 1 of Definition 6 above is required.

Definition 8

A distance closure space is a tuple $((X,{\mathcal {C}}),d)$ where $(X,{\mathcal {C}})$ is a closure space and $d: X \times X \rightarrow {\mathbb {R}}_{\ge 0} \cup \{\infty \}$ is function satisfying $d(x,y)=0$ iff $x=y$.

A quasi-discrete distance closure space is a distance closure space $((X,{\mathcal {C}}_{R}),d)$ where $(X,{\mathcal {C}}_{R})$ is a quasi-discrete closure space. $\square$

Distance operators can be added to spatial logics in various ways (see [52] for an introduction). For the purposes of the present paper, we extend SLCS with the operator ${\mathcal {D}}^{I}$, where I is an interval of ${\mathbb {R}}_{\ge 0}$. The intended meaning is that a point x of a distance closure model satisfies ${\mathcal {D}}^{I} \; \varPhi$ if its distance from the set of points satisfying $\varPhi$ falls in interval I. Below we provide the necessary formal definitions.

Definition 9

    A distance closure model is a tuple $(((X,{\mathcal {C}}),d), \mathcal{A}, \mathcal{V})$ consisting of a distance closure space $((X,{\mathcal {C}}),d)$, a valuation $\mathcal{A}: X \times A\rightarrow V$, assigning to each point and attribute the value of the attribute of the point and a valuation $\mathcal{V}: P\rightarrow 2^X$ assigning to each atomic predicate the set of points where it holds. A quasi-discrete distance closure model is a distance closure model $(((X,{\mathcal {C}}_{R}),d), \mathcal{A}, \mathcal{V})$ where $((X,{\mathcal {C}}_{R}),d)$ is a quasi-discrete distance closure space. $\square$

As the definition of d might require the elements of $R$ to be weighted—as in the case of Euclidean graphs—quasi-discrete distance closure models are often enriched with a $R$-weighting function $\mathcal{W}:R\rightarrow {\mathbb {R}}$ assigning the weight $\mathcal{W}(x,y)$ to each $(x,y)\in R$.

The satisfaction relation of our fragment of SLCS is extended as expected:

Definition 10

Satisfaction${\mathcal {M}}, x \models \varPhi$ at point $x \in X$ in model ${\mathcal {M}}= (((X,{\mathcal {C}}),d), \mathcal{A}, \mathcal{V})$ is defined by induction on the structure of formulas, by adding the equation below to those in Fig. 2:

$$\begin{aligned} {\mathcal {M}}, x \models {\mathcal {D}}^{I} \; \varPhi \; \Leftrightarrow \; d(x, \{y | {\mathcal {M}}, y \models \varPhi \}) \in I \end{aligned}$$

Note that the definition of the SLCS distance operator is parametric on the specific distance used. The particular meaning of the distance operator is fully characterised by the specific distance d of the underlying distance closure model. In this paper, we will use the Euclidean distance $d_E$ and the Chamfer distance $d_C$.

We close this section with the definition of an additional set of derived operators shown in Fig. 9.

Fig. 9

Additional derived operators

Again, with reference to Fig. 3a, Fig. 10a shows in green all the points satisfying ${\mathcal {D}}^{\, > 2} \; p$, according to the Chamfer distance (over the orthogonal adjacency relation).

Intuitively, the $\mathcal{J}^{< c}$ operator can be used as a form of filtering, eliminating small details caused by noise in the fine-scale structure of an image; this method is akin to the nested application of ${\mathcal {N}}$ and ${\mathcal {I}}$ described in Sect. 2.2, parameterised with respect to a chosen maximum size c of details to be suppressed. To see this, recall that ${\mathcal {I}}\varPhi$ is defined as $\lnot {\mathcal {N}}\lnot \varPhi$, therefore ${\mathcal {N}}{\mathcal {I}}\varPhi$ is the same as ${\mathcal {N}}(\lnot {\mathcal {N}}\lnot \varPhi )$, which is very similar to the definition of $\mathcal{J}^{< c}$, with ${\mathcal {N}}$ replaced by ${\mathcal {D}}^{<c}$.

Fig. 10

The points of Fig. 3a satisfying ${\mathcal {D}}^{\, > 2} \; p$ (a), those satisfying $\mathcal{J}^{< 3} q$ (b), and those satisfying $\mathcal{J}^{< 2} q$ (c) are shown in green (colour figure online)

With reference to Fig. 3a, Fig. 10b shows in green the points satisfying $\mathcal{J}^{< 3} q$, whereas those satisfying $\mathcal{J}^{< 2} q$ are given in Fig. 10c.

The bounded surrounded operator$\varPhi _1 {\mathcal {S}}^{I} \varPhi _2$ is satisfied by a point x if and only if x satisfies $\varPhi _1$ and is strongly surrounded by points satisfying $\varPhi _2$ and its distance from such points falls in interval I. Note that, in the first argument of ${{\mathcal {S}}_!}$, it is required that $\lnot \varPhi _2$ holds as well; this ensures that all $\varPhi _2$-points are at a distance of at least $\inf I$ from x.

Fig. 11

The points of Fig. 3a satisfying $q\; {\mathcal {S}}^{[2,2]} \; p$ (a) and those satisfying $q\; {\mathcal {S}}^{[2,3]} \; p$ (b) are shown in green (colour figure online)

In Fig. 11a (Fig. 11b, respectively), the points satisfying $q\; {\mathcal {S}}^{[2,2]} \; p$ ($q\; {\mathcal {S}}^{[2,3]} \; p$, respectively) are shown in green. Note that a similar operator has been defined in [64], which turns out to be stronger than ${\mathcal {S}}^{[a,b]}$, i.e. denoting the former operator by $\hat{{\mathcal {S}}}^{[a,b]}$, we have that, for all formulas $\varPhi _1, \varPhi _2$, $(\varPhi _1 \wedge \lnot \varPhi _2) \; \hat{{\mathcal {S}}}^{[a,b]} \; \varPhi _2$ implies $\varPhi _1 {\mathcal {S}}^{[a,b]} \varPhi _2$.

We close this section pointing out that, for finite models, the operator ${\mathcal {D}}^{\le c}$ coincides with the operator $\exists ^{\le c}$ proposed in [71]:

$$\begin{aligned} {\mathcal {M}},x \models \exists ^{\le c} \varPhi \Leftrightarrow \exists y. d(x,y) \le c \text{ and } {\mathcal {M}},y \models \varPhi \end{aligned}$$

and similarly for ${\mathcal {D}}^{< c}$ and $\exists ^{< c}$. Note that this coincidence does not hold in general, e.g. for Euclidean spaces. Our choice of the specific distance operator is motivated by its natural compatibility with distance transforms, as we illustrate in Sect. 3.2.

3.2 Model checking SLCS with distance operators

For distance-based operators, generally speaking, the time complexity of naive model checking algorithms is quadratic in the size of the space (see [64] for an example). However, given a Euclidean graph representing a multi-dimensional image, spatial model checking of formulas ${\mathcal {D}}^{I} \varPhi$ for Euclidean or Chamfer distance can be done in linear time or quasi-linear time, respectively, with respect to the number of points of the space. This is achieved via so-called distance transforms, that are one of the subjects of topology and geometry in computer vision [51] and are extensively used in modern image processing and computer graphics [27]. In particular, effective linear-time algorithms have been recently introduced in the literature [37, 58]. Basically, a distance transform takes a model ${\mathcal {M}}_{in}$ as input and produces a model ${\mathcal {M}}_{out}$ as output as follows. Let ${\mathcal {M}}_{in}$ be a model $(((X,{\mathcal {C}}_{R}),d), \mathcal{A}_{in}, \mathcal{V},\mathcal{W})$ such that every point $x \in X$ has an attribute, say $a_{in}$, defined on a binary domain, say $\{0,1\}$—the value of such an attribute may represent the fact that the point satisfies a given formula $\varPhi$ or not. The output model will be ${\mathcal {M}}_{out} = (((X,{\mathcal {C}}_{R}),d), \mathcal{A}_{out}, \mathcal{V},\mathcal{W})$ such that every point $x \in X$ has an attribute, say $a_{out}$, and $\mathcal{A}_{out}(x,a_{out})=d(x,\{y\in X | \mathcal{A}_{in}(y,a_{in})=1\})$.

The algorithm of Fig. 5 is extended with the case for ${\mathcal {D}}^{I} \varPhi$, sketched in Fig. 13; note that, in the general case, the argument ${\mathcal {M}}$ of $\mathtt {Sat}$ is a weighted finite distance closure model $(((X,{\mathcal {C}}_{R}),d), \mathcal{A}, \mathcal{V},\mathcal{W})$, where the distance function d may be defined using the weights in $\mathcal{W}$. It is assumed that two distinct attributes $a_{s}$ (playing the role of $a_{in}$ above) and $a_{d}$ (playing the role of $a_{out}$ above) are defined for all $x \in X$. Two intermediate, auxiliary models ${\mathcal {M}}_s$ and ${\mathcal {M}}_d$ are computed—${\mathcal {M}}_s$ in Step 1 and ${\mathcal {M}}_d$ in Step 2—according to the distance transform method described above. In Fig. 13, for the sake of simplicity, functions $\mathcal{A}, \mathcal{A}_s$ and $\mathcal{A}_d$ are treated as (bi-dimensional) arrays. Again with reference to Fig. 3a, and formula ${\mathcal {D}}^{\, > 2} \; p$—shown in Fig. 10a—intermediate models ${\mathcal {M}}_s$ and ${\mathcal {M}}_d$ are shown in Fig. 12a, b, respectively. Here, the chosen notion of distance is Chamfer over orthogonal adjacency, considering the Euclidean distance between two adjacent voxels equal to the unit. The values in the points in Fig. 12a (Fig. 12b, respectively) are those of attribute $a_s$ ($a_d$, respectively).

Fig. 12

Intermediate models for ${\mathcal {D}}^{\, > 2} \; p$ and input model of Fig. 3a, according to the procedure of Fig. 13

Fig. 13

Sketch of the model checking algorithm for ${\mathcal {D}}^{I} \; \varPhi$

For what concerns the computation of the specific distance and the related distance transform, for Euclidean distance we use the algorithm that was proposed by Maurer in [58]. Such algorithm computes Euclidean distance transforms on anisotropic multi-dimensional grids (such as 2D and 3D medical images); it has linear complexity, its run-time is predictable, and it is among the most efficient algorithms for the purpose [36]. The general idea of the algorithm is to proceed by induction on the number of dimensions of the image. The distance transform problem in $n+1$ dimensions is reduced to the problem in n dimensions by a technique that relies on multi-dimensional Voronoi maps. We refer the interested reader to [27], where a theoretical study of the algorithm is provided. The specification described therein was closely followed in our implementation.

For shortest-path distances over arbitrary directed graphs, we use a variant of the well-known Dijkstra shortest-path algorithm, called “modified Dijkstra distance transform” in [44]. The standard Dijkstra algorithm uses a priority queue sorted by distance from a root node. The queue is initialised to the root node of the considered graph, whose priority is set to 0. In the modified version, when computing the distance transform from a set of nodes identified by formula $\varPhi$, the queue is initialised with all the nodes that satisfy $\varPhi$ and have an outgoing edge reaching a node not satisfying $\varPhi$; all such nodes have priority 0. The algorithm then proceeds as the standard algorithm. As a result, after termination, each node of the graph is labelled with the shortest-path distance from the set of nodes satisfying $\varPhi$, as required by the specification. The asymptotic run-time of this procedure is not linear but quasi-linear due to the usage of a priority queue. In this respect, research is still active to optimise the procedure in specific cases (see e.g. [75]). However, the effective run-time behaviour of the algorithm is highly dependent on the structure of the considered graph and the chosen implementation of data structures.

4 A logical framework for texture analysis

In this section, we define an additional logic operator that, when incorporated in the spatial logic presented in the previous sections, provides a logical framework for Texture Analysis (TA).

TA can be used for finding and analysing patterns in (medical) images, including some that are imperceptible to the human visual system. Patterns in images are entities characterised by distinct combinations of features, such as brightness, colour, shape, size. TA includes several techniques and has proved promising in a large number of applications in the field of medical imaging [16, 30, 50, 56]; in particular, it has been used in Computer Aided Diagnosis [47, 49, 79] and for classification or segmentation of tissues or organs [17, 69, 70]. In TA, image textures are usually characterised by estimating some descriptors in terms of quantitative features. Typically, such features fall into three general categories: syntactic, statistical, and spectral [50]. Our work is mostly focused on statistical approaches to texture analysis. For two-dimensional images, statistical methods consist of extracting a set of statistical descriptors from the distributions of local features in a neighbourhood of each pixel.

In this paper, we explore the use of first-order statistical methods, that are statistics based on the probability distribution function of the intensity values of the pixels of parts, or the whole, of an image. The classical first-order statistical approach to TA makes use of statistical indicators of the local distribution of image intensity around each pixel, such as mean, variance, skewness, kurtosis, entropy [73]. Although such indicators ignore the relative spatial placement of adjacent pixels, statistical operators are useful in MI because their application is invariant under transformations of the image, in particular affine transformations (rotation and scaling), which is necessary when analysing several images acquired in different conditions. It is worth mentioning that current research also focuses on constructing features using first-order operators, keeping some spatial coherence, but loosing at least partially the aforementioned invariance [76]. The method we propose is an attempt to improve over the classical setting described above, by analysing (the histograms of) statistical distributions directly.

In the following, we introduce a spatial logic operator that compares image regions in order to classify points that belong to sub-areas in the image where the statistical distribution of the intensity of pixels is similar to that of a chosen reference region. Several similarity measures exist (see [61]), that can be used to compare distributions in images. In particular, as a starting point, we use the cross-correlation function (also called Pearson’s correlation coefficient), that is often used in the context of image retrieval, but is also popular in other computer vision tasks. In MI, cross-correlation is also frequently used in the case of image co-registration ( [13]).⁵

4.1 A logical operator for statistical similarity

The statistical distribution of the values of a numerical attribute in a set of points Y of a space—e.g. the grey levels of the pixels or voxels of an area of a black and white image—is approximated by the histogramh of the values of the attribute in the points belonging to Y, as described below. Given a minimum value m, a maximum value M, and a positive number of binsk, let $\varDelta = (M - m)/k$ and define the histogram h as a function associating with each bin$i \in [1,k]$ the number of points that have the value of the attribute in the (half-open) interval $[(i-1) \cdot \varDelta + m,i \cdot \varDelta + m)$. The minimum value m and the maximum value M are aimed at improving the resolution of histograms, by excluding rare peaks in the set of points—they might be due to artefacts in acquisition, in the case of images—and would result in a high number of empty bins. A formal definition is given below:

Definition 11

Given closure model ${\mathcal {M}}= ((X,{\mathcal {C}}), \mathcal{A}, \mathcal{V})$, we define function $\mathcal{H}: A \times 2^X \times {\mathbb {R}}\times {\mathbb {R}}\times {\mathbb {N}}\rightarrow ({\mathbb {N}}\rightarrow {\mathbb {N}})$ such that for all values $m,M \in {\mathbb {R}}$, with $m<M$, and $k,i \in {\mathbb {N}}$, with $k>0$ and $i\in [1,k]$, letting $\varDelta =\frac{M-m}{k}$:

$$\begin{aligned} \mathcal{H}(a,Y,m,M,k)(i)= & {} \left| \{y\in Y | (i-1) \varDelta \right. \\\le & {} \left. \mathcal{A}(y,a) - m < i \varDelta \}\right| \end{aligned}$$

$\square$

So $\mathcal{H}(a,Y,m,M,k)$ is the histogram of the distribution of the values of attribute a of the points in Y, in the interval [m, M] with step $\varDelta$.

The definition of cross-correlation between two histograms follows. In the sequel, for histogram $h: [1,k] \rightarrow {\mathbb {N}}$ we let $\overline{h}=\frac{1}{k}\sum _{i=1}^k h(i)$ denote the mean of h.

Definition 12

Let $h_1, h_2: [1,k] \rightarrow {\mathbb {N}}$ be two histograms. The cross-correlation of $h_1$ and $h_2$ is defined as follows:

$$\begin{aligned} {\mathbf {r}}(h_1,h_2) = \frac{\sum _{i=1}^k\left( h_1(i) - \overline{h_1} \right) \left( h_2(i) - \overline{h_2} \right) }{ \sqrt{ \sum _{i=1}^k \left( h_1(i) - \overline{h_1} \right) ^2 } \sqrt{ \sum _{i=1}^k \left( h_2(i) - \overline{h_2} \right) ^2 } } \end{aligned}$$

$\square$

The value of ${\mathbf {r}}{}{}$ is normalised so that $-1\le {\mathbf {r}}(h_1,h_2) \le 1$; ${\mathbf {r}}(h_1,h_2)=1$ indicates that $h_1$ and $h_2$ are perfectly correlated (that is, $h_1 = ah_2+b$, with $a>0$); ${\mathbf {r}}(h_1,h_2) =-1$ indicates perfect anti-correlation (that is, $h_1=ah_2+b$, with $a<0$). On the other hand, ${\mathbf {r}}(h_1,h_2) = 0$ indicates no correlation. Note that normalisation makes the value of ${\mathbf {r}}{}{}$ undefined for constant histograms, having therefore standard deviation of 0; in terms of statistics, a variable with such standard deviation is only (perfectly) correlated to itself. This special case is handled by letting ${\mathbf {r}}(h_1,h_2)=1$ when both histograms are constant, and ${\mathbf {r}}(h_1,h_2)=0$ when only one of the $h_1$ or $h_2$ is constant.

We are now ready for embedding the statistical similarity operator $\triangle \!\!\!{\scriptstyle \triangle }_{\bowtie c} {\tiny \left[ \begin{array}{ccc} m &{} M &{} k\\ \rho &{} a &{} b \end{array} \right] }$ in ImgQL.

Definition 13

Satisfaction${\mathcal {M}}, x \models \varPhi$ at point $x \in X$ in model ${\mathcal {M}}= (((X,{\mathcal {C}}),d), \mathcal{A}, \mathcal{V})$ is defined by induction on the structure of formulas, by adding the following equation to those in Fig. 2, where $m,M \in {\mathbb {R}}$, with $m<M$, and $k\in {\mathbb {N}}$, with $k>0$:

$$\begin{aligned} {\mathcal {M}}, x \, \models \, \triangle \!\!\!{\scriptstyle \triangle }_{\bowtie c} {\tiny \left[ \begin{array}{ccc} m &{} M &{} k\\ \rho &{} a &{} b \end{array} \right] } \varPhi \Leftrightarrow {\mathbf {r}}(h_a,h_b) \bowtie c \end{aligned}$$

with

• $h_a(i)=\mathcal{H}(a,S(x,\rho ),m,M,k)(i)$,

• $h_b(i)=\mathcal{H}(b,\{y | {\mathcal {M}},y \models \varPhi \},m,M,k)(i)$,

• $\bowtie \, \in \, \{=,<,>,\le ,\ge \}$, and

• $S(x,\rho )=\{y\in X | d(x,y) \le \rho \}$ is the sphere of radius $\rho$ centred in x. $\square$

So $\triangle \!\!\!{\scriptstyle \triangle }_{\bowtie c} {\tiny \left[ \begin{array}{ccc} m &{} M &{} k\\ \rho &{} a &{} b \end{array} \right] } \varPhi$ compares the region of the space constituted by the sphere of radius $\rho$ centred in x against the region characterised by $\varPhi$. The comparison is based on the cross-correlation of the histograms of the chosen attributes of (the points of) the two regions, namely a and b and both histograms share the same domain ([m, M]) and the same bins ([1, k]). In summary, the operator allows to check to which extent the sphere around the point of interest is statistically similar to a given region (specified by) $\varPhi$. For example, $\triangle \!\!\!{\scriptstyle \triangle }_{\ge 0.7} {\tiny \left[ \begin{array}{ccc} 200 &{} 2000 &{} 100\\ 10.0 &{} a &{} b \end{array} \right] } \top$ is true at voxels centred in a region—of radius 10.0—where the distribution of the values of attribute a has cross-correlation greater than 0.7 with the distribution of the values of attribute b in the whole image. In this case, cross-correlation is computed using 100 bins, and taking into account only values between 200 and 2000.

Fig. 14

Sketch of the model checking algorithm for the statistical similarity operator

4.2 Model checking ImgQL with statistical similarity operators

The algorithm of Fig. 5 is extended with the case for $\triangle \!\!\!{\scriptstyle \triangle }_{\bowtie c} {\tiny \left[ \begin{array}{ccc} m &{} M &{} k\\ \rho &{} a &{} b \end{array} \right] } \varPhi$, sketched in Fig. 14. Auxiliary function $\mathtt {Idx}$ computes the bin index associated with the intensity level $\ell$ of the relevant attribute, relative to parameters m, M and k: $\mathtt {Idx}(\ell ,m,M,k) = (\ell \; \mathtt{div} \; \frac{M-m}{k}) +1.$ The extension of the algorithm for implementing the statistical similarity operator is straightforward. An array $H_b$, sized to the number of bins k, is allocated, initialised to 0 at each index, and the histogram $h_b$ (see Definition 13) is stored in it, by iterating over all the points y satisfying $\varPhi$, finding the index i of the bin corresponding to the intensity level of y, and increasing the corresponding value of $H_b[i]$. An additional array $H_a$, sized to the number of bins k, is allocated. For each pixel x, $H_a$ is (re-)initialised to 0 at each index, and all the points y laying in the sphere of radius $\rho$ centred in x are examined; for each y, the index i of its bin is identified, and the value of $H_a[i]$ is increased, so that when all the y have been examined, $H_a$ represents the histogram $h_a$. The cross-correlation value ${\mathbf {r}}(h_a,h_b)$ is then computed by simple calculations that are linear in the number of bins k.

Table 1 Benchmark results on some 2d synthetic images. Images have the same horizontal and vertical size

This algorithm has time complexity proportional to $v \cdot \rho ^n \cdot k$, where v is the number of pixels in the image and n the number of dimensions (indeed the number of pixels in an n-dimensional sphere is proportional to $\rho ^n$). Since $\rho$ and k are usually fixed for a given analysis, such algorithm can still be considered “linear” in the size of the image. This basic procedure is amenable to optimisation, for instance by observing that the spheres centred around two different points of the image may share some pixels; therefore, the histogram of each one could be computed starting from the histogram of the other, at the expenses of more memory needed to store the histogram of different points. We leave the study of similar optimisations for future work.

5 The tool topochecker

The tool topochecker⁶ is a global model checker, capable of analysing models specified as weighted graphs, RGB images, or grayscale medical images. The tool is implemented in the functional programming language OCaml,⁷ which provides a good balance between declarative features and computational efficiency. The output of the tool consists of a region of interest (ROI) for each formula, that is, an image where the specific region where such formula holds is coloured according to a user-specified colour. The spatial model checking algorithm is entirely run in central memory, and it uses memoisation (and on-disk caching) to store the intermediate results, so that when the same sub-formula is used more than once, results are reused.

In order to evaluate the efficiency of the tool, we have designed a set of benchmarks.⁸ Currently, we aim at evaluating the algorithms for Euclidean and Chamfer distance transforms, similarity search via statistical cross-correlation, and the reachability / surrounded primitives. Four benchmarks are currently considered: search for exit and blocked paths in a maze, similar to Example 7.4 in [23], which exercises the implementation of the surrounded operator (indirectly, via the touch operator); cross-correlation with various radiuses (plus thresholding), using the whole image as a target; Euclidean distance transform (plus thresholding); Chamfer distance transform (plus thresholding). The last three benchmark types use a checkerboard-like pattern with areas having differently sized squares (see Fig. 15a). Although the graphical results on such images are not surprising in general, we show in Fig. 15b the output from statistical cross-correlation, as it also illustrates how the operator works. Note that the “target” histogram (that of the whole image) mostly consists of an equal number of black and white points (plus a smaller number of points having an intermediate value, due to grey lines separating the different areas of the image). Therefore, the points that have high local cross-correlation with the whole image (depicted in green) are those that lay on the border of squares, whereas in the inner part of any square, the histogram only consists of either white or black points.

Fig. 15

A checkerboard-like pattern (a) and the result of the $\triangle \!\!\!{\scriptstyle \triangle }$ operator applied to it (b)

We have run our benchmarks on a laptop equipped with a 6th generation Core i7 CPU; Table 1 displays the image resolution, radius for cross-correlation, number of voxels, execution time in seconds, and memory used in kilobytes for each test. Execution times are as expected: the cross-correlation operator (benchmark “scmp”) is linear in the size of the model, as well as the Euclidean distance transform algorithm (“maurer”), and the surrounded operator (“maze”), whereas Chamfer distance, employing a variant of the Dijkstra shortest-path algorithm, has complexity $n \log n$, which is apparent when the size of the model grows by powers of two.

6 Medical image analysis with ImgQL

MR images are produced using different kinds of sequences of magnetic field gradients and radio-waves. Images so obtained are called weighted images; these can be further post-processed in various ways. For instance, typical weighted images are those produced using Fluid-attenuated inversion recovery pulse sequence (MR-FLAIR), T2 weighted pulse sequence (MR-T2w), or diffusion-weighted images, whereas the Apparent Diffusion Coefficient maps (ADC) are obtained via post-processing of diffusion-weighted images. A standard reference for such matters is [14]. In this section, we illustrate our approach on the segmentation of glioblastoma tumour and oedema in images obtained using MR-FLAIR. We first show the steps on 2D images and then present further results for 3D images.

For glioblastoma, our procedure was successfully tested on five images from different sources, that were acquired in very different conditions. However, validation of the methodology for actual clinical usage requires extensive clinical research. We refer to Sect. 6.2 for preliminary validation results and a more detailed discussion.

6.1 Example: segmentation of glioblastoma

In this example, we detail the specification of an analysis aimed at the segmentation of glioblastoma (GBM) and oedema in MR-FLAIR images. Being able to segment tumour and oedema in medical images can be of immediate use for automatic contouring applications in radiotherapy, and, in perspective, it can be helpful in detecting the invisible infiltrations in computer-aided diagnosis applications. The procedure is non-trivial, but every step is justified by morphological and spatial considerations on the arrangement of parts of the head and the brain.

Normal tissues of the head can be divided into several classes. The outer layer of the head consists of adipose tissue (and skin) surrounding the skull that in turn consists of bone and bone marrow. The skull encloses the brain tissues. The brain itself is suspended in cerebrospinal fluid (CSF) and isolated from the blood stream. Thresholds in the grey levels of images can be used to single out specific tissues in a medical image; however, in doing so, noise is generated in the form of (small, scattered) regions not belonging to the tissue. The relative positioning of tissues—the so-called topological information of the image—plays an important role in suppressing such noise. We will see in the following how such information is encoded by logic formulas in the methodology we propose.

Fig. 16

a Slice of MR-FLAIR brain acquisition of a patient, Case courtesy of Dr. Ahmed Abd Rabou, Radiopaedia.org, rID: 22779; b a different slice of the acquisition in Fig. 16a; c slice of MR-FLAIR brain acquisition of a different patient—Case courtesy of A.Prof Frank Gaillard, Radiopaedia.org, rID: 5292; d histograms of Fig. 16a (in blue), of Fig. 16b (in green) and of Fig. 16c (in red) (colour figure online)

GBMs are intracranial tumours composed of typically poorly marginated, diffusely infiltrating necrotic masses. Even if the tumour is totally resected, it usually recurs, either near the original site, or at more distant locations within the brain. GBMs are localised to the cerebral hemispheres and grow quickly to various sizes, from only a few centimetres, to lesions that cover a whole hemisphere. Infiltration beyond the visible tumour margin is always present. In MR-FLAIR images, GBMs appear hyperintense and surrounded by vasogenic oedema.⁹

Segmentation of GBM according to our method is performed in three steps:

• 1. a preprocessing step (not using topochecker), aimed at normalisation of images, to make the choice of thresholds in our experiment applicable to different images;

• 2. brain segmentation, to limit the area of the image where the tumour is searched for;

• 3. tumour and oedema segmentation, which is the stated goal of this example.

6.1.1 Preprocessing

Histograms of grey levels of images¹⁰ of the same body part may differ from each other due to inter-patient or inter-scanner differences or depending on the actual acquisition volume (Fig. 16) or the file format used to store the image.¹¹

More uniform results, on different images, can be obtained by dividing the intensity of each pixel by the average of the intensity levels of all the significant pixels in the image. A pixel is considered significant when it does not belong to the background. Significant pixels are selected using a Boolean mask (indicated by the green area in Fig. 17c). In order to compute such a mask, we start from the observation that the background (corresponding to the air surrounding the head of a patient) is darker than the rest of the image, so it mostly contributes to the initial part of its histogram. This situation is witnessed in the histogram by a peak close to 0. A threshold is thus selected for each image as the value immediately following such peak. Using this threshold, it is possible to isolate the background, by separating it from the head (Fig. 17a). Note that the obtained mask also includes cerebrospinal fluid (CSF) and bone. The part of the mask that touches the boundary of the whole image is then selected (Fig. 17b) and its complement, that is, the green area in Fig. 17c, is finally used to select the significant pixels to compute the mean value for normalisation. Figure 17d shows the histograms of images after normalisation.

Fig. 17

Finding the mask for normalisation: a the pixels in Fig. 16c with grey levels below a given threshold are shown in green; b the sub-mask that touches the border of the image is shown in orange; c the mask of the image excluding the background is shown in green; d histograms of normalised version of images in Fig. 16a (in blue), in Fig. 16b (in green), in Fig. 16c (in red), and in Fig. 18a (in orange) (colour figure online)

We remark that equalisation of histograms is another form of normalisation, frequently used for texture analysis ([48]). We do not use this method as it changes the relationship between grey levels of different structures in the image (as shown in Fig. 18), that we use rather prominently for differentiating different tissues; normalisation of image intensity is sufficient for our purposes.

Fig. 18

Effect of histogram equalisation: a a slice of MR acquisition of brain, on the left, and its equalised version, on the right—case courtesy of Dr. Ahmed Abdrabou, Radiopaedia.org, rID: 39024; b histograms of grey levels of the original (green) and equalised (red) version of image in (a) (colour figure online)

6.1.2 Brain segmentation

In this second phase of our method, we perform a segmentation of the brain in order to limit the search area of the tumour, by means of specific logic formulas. This improves the accuracy of the output (e.g. avoiding areas in bone marrow or skull) and reduces computing time.

In the process below, we fix some thresholds for identifying different tissues in the brain; note that, thanks to the preprocessing step described above, these can be kept uniform across different images.

Intuitively, the general model of a patient head that we use to segment the brain in MR-FLAIR images is defined as follows:

• Darker pixels in the head belong to CSF and bones;

• Brighter pixels belong both to adipose tissue surrounding the head, and to bone marrow;

• Also pixels belonging to the tumour and oedema are brighter than the surrounding tissues;

• The brain region is composed of white matter, grey matter, tumour and oedema;

• The brain (excluding the tumour) has intermediate intensities and is mainly surrounded by CSF.

For the segmentation of the brain, we use the normalised NIfTI image of the MR-FLAIR acquisition shown in Fig. 16c. In the rest of the analysis, the relevant attribute, i.e. the normalised grey level, of each pixel in this image is referred to as FLAIR.

It is convenient to define a few additional operators that serve as macros and that are specifically useful in the segmentation procedure that follows; for readability reasons, we use a prefix notation for these operators:

$$\begin{aligned} \begin{array}{l c l} \mathtt{grow}(\varPhi _1,\varPhi _2) &{} \triangleq &{} (\varPhi _1 \vee \varPhi _2) \; {\mathcal {S}}\; \lnot \varPhi _2\\ \mathtt{denoise}(\varPhi ) &{} \triangleq &{} \varPhi \; \mathcal{T}\; {\mathcal {D}}^{\ge 2} \lnot \varPhi \\ \mathtt{closeTo}(\varPhi ) &{} \triangleq &{} {\mathcal {D}}^{< 3}\; \varPhi \end{array} \end{aligned}$$

Formula $\mathtt{grow}(\varPhi _1,\varPhi _2)$ is inspired by the image segmentation method of seeded region growing [1]. This method starts from a number of seed points in the region of interest and examines neighbouring points to decide whether they should be added to the region. The definition of $\mathtt{grow}(\varPhi _1,\varPhi _2)$ is a form of region growing, under the assumption that it is guaranteed that all points satisfying $\varPhi _1$ are also satisfying $\varPhi _2$.

We start from points that satisfy property $\varPhi _1$ and to which all points satisfying property $\varPhi _2$ are added that, together with those satisfying $\varPhi _1$, form a common region that is surrounded by points that do not satisfy $\varPhi _2$.

Fig. 19

Experimental results of using topochecker for segmentation of glioblastoma and oedema: a a slice of a brain acquisition of a patient—case courtesy of A.Prof Frank Gaillard, Radiopaedia.org, rID: 5292; b background (in red) and adipose tissue (in green); c output showing $\mathtt{head}$ (in red or green) and $\mathtt{CSF}$ (in red); d output of $\mathtt{brainApprox}$; e output of $\mathtt{brainSeed}$; f output of $\mathtt{noisyBrain}$; g output of $\mathtt{brain}$; h output of $\mathtt{tum0}$ (in green) and $\mathtt{oed0}$ (in red); i output of $\mathtt{tum1}$ (in green) and $\mathtt{oed1}$ (in red); j output of $\mathtt{tum2}$ (in green) and $\mathtt{oed2}$ (in red); k output of $\mathtt{tumour}$ (in green) and $\mathtt{oedema}$ (in red) l a slice of a brain acquisition of another patient—case courtesy of Dr. Ahmed Abd Rabou, Radiopaedia.org, rID: 22779; m output of $\mathtt{tumour}$ (in green) and $\mathtt{oedema}$ (in red); n another slice from the second patient; o output of $\mathtt{tumour}$ (in green) and $\mathtt{oedema}$ (in red) (colour figure online)

Let A be the set of points satisfying formula $\varPhi$. Formula $\mathtt{denoise}(\varPhi )$ is used to remove small areas from A, as follows: first A is shrunk by 2 units; in doing so, some sub-areas of A may disappear; the areas that do not disappear are restored to their original shape by means of the touch operator. This operation is similar to $\mathcal{J}^{< 2}$, but it preserves the contours of the original area A. Formula $\mathtt{closeTo}(\varPhi )$ denotes the points that lay at a distance less than 3 units from the set of points satisfying $\varPhi$. For this analysis, the ${\mathcal {D}}^{}$ Chamfer distance operator uses 4 adjacent pixels per node and the distance units are in millimetres with respect to the actual dimension of the head, i.e. the real-world dimensions.

Next, we define a number of useful thresholds for the grey levels of the image that are used to obtain a first approximation of different kinds of tissue of interest:

$$\begin{aligned} \begin{array}{l c l} \mathtt{lowIntsty}&{} := &{} \mathtt{FLAIR}< 0.5;\\ \mathtt{medIntsty}&{} := &{} \mathtt{FLAIR}> 0.5\; \wedge \; \mathtt{FLAIR}< 1.3;\\ \mathtt{highIntsty}&{} := &{} \mathtt{FLAIR}> 1.7;\\ \mathtt{tumIntsty}&{} := &{} \mathtt{FLAIR}> 1.17\; \wedge \;\mathtt{FLAIR}< 1.53;\\ \mathtt{oedIntsty}&{} := &{} \mathtt{FLAIR}\ge 1.47\; \wedge \;\mathtt{FLAIR}< 2.4; \end{array} \end{aligned}$$

We distinguish three general levels of intensity (low, medium, and high), and two specific intensities that are typical for tumour and oedema, respectively.

We are now ready to start the segmentation procedure. First, we identify the points that are part of the background of the image. These all have a very low intensity, but there are other points in the image that have low intensity as well. What distinguishes the points of the background from the other low intensity points is that the background area touches the border of the image.

We assume that the special atomic proposition, named $\mathtt{border}$ is satisfied by the points that form the border of an image; this predicate is predefined in topochecker . This way points of the background are exactly those that satisfy the property ${\texttt {background}}$:

$$\begin{aligned} \begin{array}{l c l} {\texttt {background}}\triangleq & {} \mathtt{lowIntsty}\; \mathcal{T}\; \mathtt{border}\end{array} \end{aligned}$$

The points that satisfy ${\texttt {background}}$ are shown in red in Fig. 19b. The original image is shown in Fig. 19a.

The next step is to look for the external border of the head, consisting of skin and adipose tissue. For our purposes, it is sufficient to identify the adipose tissue, since the brain is surrounded by the adipose tissue, which separates it from the skin.

Adipose tissue in the normalised MR-FLAIR images has intensity above 1.7, so of high intensity. As before, there may be other points with high intensity in the image, but we exploit the knowledge that adipose is at the external border of the head, and thus close to the background. These points can be found with the following formula:

$$\begin{aligned} \begin{array}{l c l} \mathtt{adipose}\triangleq & {} \mathtt{highIntsty}\; \mathcal{T}\; \mathtt{closeTo}({\texttt {background}}) \end{array} \end{aligned}$$

The points that satisfy $\mathtt{adipose}$ are shown in green in Fig. 19b.

Using the properties ${\texttt {background}}$ and $\mathtt{adipose}$, it is not difficult to specify the points that are part of the head. These are all those points that are not part of the background or close to adipose tissue.

$$\begin{aligned} \begin{array}{l c l} \mathtt{head}\triangleq & {} \lnot (\mathtt{closeTo}(\mathtt{adipose}) \vee {\texttt {background}}) \end{array} \end{aligned}$$

The points that satisfy $\mathtt{head}$ are the union of the green and red points in Fig. 19c (see below).

In the next steps, we show how we can distinguish the various tissues within the area of the head, namely the brain and the cerebrospinal fluid (CSF) that contains it. We start from the identification of points that are part of CSF. These are points that are within the head and that have low intensity:

$$\begin{aligned} \begin{array}{l c l} \mathtt{CSF}\triangleq & {} \mathtt{lowIntsty}\wedge \mathtt{head}\end{array} \end{aligned}$$

The points that satisfy $\mathtt{CSF}$ are shown in red in Fig. 19c.

We proceed with segmentation of the brain in four subsequent steps. As a first approximation, we look for the points of the brain with medium intensity within the head (and that are not belonging to CSF). Within this approximation, we select some inner areas that are most certainly part of brain tissue and that can serve as a seed from which to ‘grow’ in a more precise way points belonging to the brain. Finally, we remove pieces that have been erroneously identified as part of the brain, but that are actually relatively small areas that are part of the skull or bone, having a similar intensity as that of the brain. This way we obtain all pixels that are actually part of the brain. The four steps of the specification are given below.

$$\begin{aligned} \begin{array}{l c l} \mathtt{brainApprox}&{} \triangleq &{} \mathtt{head}\wedge \lnot \mathtt{CSF}\wedge \mathtt{medIntsty}\\ \mathtt{brainSeed}&{} \triangleq &{} {\mathcal {D}}^{> 10} \lnot \mathtt{brainApprox}\\ \mathtt{noisyBrain}&{} \triangleq &{} \mathtt{grow}(\mathtt{brainSeed}, \mathtt{head}\; \wedge \; \lnot \mathtt{CSF})\\ \mathtt{brain}&{} \triangleq &{} \mathtt{noisyBrain}\; \mathcal{T}\; \mathtt{brainSeed}\end{array} \end{aligned}$$

The points that satisfy $\mathtt{brainApprox}$, ($\mathtt{brainSeed}$, and $\mathtt{noisyBrain}$, respectively) are shown in green in Fig. 19d (Fig. 19e, f, respectively). The final result of the brain is shown in Fig. 19g.

Fig. 20

Effects of using cross-correlation on a 3D volume. a, c, e target image for cross-correlation (glioblastoma in red, oedema in blue). b, d, f Output of the cross-correlation operator. Case courtesy of Dr. Ahmed Abdrabou, Radiopaedia.org, rID: 39024 (colour figure online)

Fig. 21

Experimental results of using topochecker for segmentation of glioblastoma and oedema on a 3D volume. a, c, e Original slices. b, d, f Output of the segmentation of glioblastoma (in red) and oedema (in blue). Case courtesy of Dr. Ahmed Abdrabou, Radiopaedia.org, rID: 39024 (colour figure online)

6.1.3 GBM segmentation

In the final part of our analysis, we identify tumour and oedema regions. Since in MR-FLAIR, GBM and oedema are hyperintense areas, and the oedema is brighter than the tumour, we start by using the thresholds we introduced before that provide a rough segmentation of the image shown in Fig. 19a:

$$\begin{aligned} \begin{array}{l c l} \mathtt{tum0}&{} \triangleq &{} \mathcal{J}^{< 1} (\mathtt{tumIntsty}\; {\mathcal {S}}\; (\mathtt{brain}\; \vee \; \mathtt{CSF}))\\ \mathtt{oed0}&{} \triangleq &{} \mathcal{J}^{< 1} (\mathtt{oedIntsty}\; {\mathcal {S}}\; (\mathtt{brain}\; \vee \; \mathtt{CSF})) \end{array} \end{aligned}$$

In Fig. 19h, we show in red the points that satisfy formula $\mathtt{oed0}$ referring to the oedema, and in green those satisfying formula $\mathtt{tum0}$ referring to the tumour. These are points that have the selected intensity ($\mathtt{oedIntsty}$ and $\mathtt{tumIntsty}$, respectively) and are part of the brain tissue, i.e. they are surrounded by $\mathtt{brain}$ or $\mathtt{CSF}$. Note that the regions $\mathtt{oed0}$ and $\mathtt{tum0}$ are partially overlapping. Moreover, we remove from these identified regions areas whose radius is smaller than 1mm using the $\mathcal{J}^{< 1}$ operator.

An important constraint, that drastically reduces noise in the output of our analysis, is the a priori knowledge that oedema and tumour are very close to each other. We exploit this knowledge using the distance operator ${\mathcal {D}}^{}$ as follows:

$$\begin{aligned} \begin{array}{l c l} \mathtt{oeddst}&{} \triangleq &{} {\mathcal {D}}^{\le 2} \mathtt{oed0}\\ \mathtt{tum1}&{} \triangleq &{} \mathtt{tum0}\; \mathcal{T}\; \mathtt{oeddst}\\ \mathtt{oed1}&{} \triangleq &{}\mathtt{oed0}\; \wedge \; (\mathtt{oeddst}\; \mathcal{R}\; \mathtt{tum1}) \end{array} \end{aligned}$$

We first define the region $\mathtt{oeddst}$ at distance less than 2mm from $\mathtt{oed0}$ then select sub-regions of $\mathtt{tum0}$ that touch$\mathtt{oeddst}$ (formula $\mathtt{tum1}$) and sub-regions of $\mathtt{oed0}$ that can reach points satisfying $\mathtt{tum1}$ by passing only through points satisfying $\mathtt{oeddst}$ (formula $\mathtt{oed1}$). The result is shown in Fig. 19i. Comparing the latter with Fig. 19h, we can observe that some green areas, located in the left half of the brain, have disappeared. These were points with a similar intensity as that of tumour tissue, but not actually part of it since they were not connected to the tumour. In this example, we used shortest-path distance as an approximation of Euclidean distance, for the sake of execution speed, as high accuracy for the distance is less important in this particular case.

$$\begin{aligned} \begin{array}{l c l} \mathtt{tum2}&{} \triangleq &{} \mathtt{denoise}(\mathtt{tum1})\\ \mathtt{oed2}&{} \triangleq &{} \mathtt{denoise}(\mathtt{oed1}) \end{array} \end{aligned}$$

Figure 19j illustrates the areas characterised by $\mathtt{tum2}$ (green) and $\mathtt{oed2}$ (red). Compared to Fig. 19i, this removes a number of small detached areas of oedema that were located in the tumour area and should be considered as noise.

Finally, $\mathtt{tumour}$ and $\mathtt{oedema}$ are defined as being inter-reachable. This part could remove some separate areas that have tumour or oedema intensity but should not be considered as such since they are too far apart. In this particular case, no such areas were present apparently as can be observed comparing Fig. 19j with the final output of the segmentation in Fig. 19k.

$$\begin{aligned} \begin{array}{l c l} \mathtt{tumour}&{} \triangleq &{} \mathtt{tum2}\; \mathcal{T}\; \mathtt{oed2}\\ \mathtt{oedema}&{} \triangleq &{} \mathtt{oed2}\; \mathcal{T}\; \mathtt{tum2}\end{array} \end{aligned}$$

As a further result, in Fig. 19 we show the final segmentation of tumour and oedema on two other images from a different patient applying the same specification. Figure 19m shows the segmentation of the image in Figs. 16a, and 19o shows the one of the image in Fig. 16b. The original images are also shown aside of the result in Fig. 19 for more convenient comparison.

The whole analysis presented in this section has been carried out in 2D. The same approach also works in 3D, with minor modifications. Fig. 21 shows some slices of the segmentation of MR-FLAIR acquisition of the patient in Fig. 18a, using topochecker on the whole 3D volume image. Some minor modifications to the model checking session presented in this section were required; the most relevant one is that cross-correlation was used to enlarge the area of tum1 to tum1’ prior to using tum2$\triangleq$denoise(tum1’). See Fig. 20.

In general, there may be many different ways to obtain an accurate segmentation. Ideally, these should be robustly working for many different images, both in 2D and in 3D. In future work, we plan to investigate this in more detail and compare various variants from the point of view of robustness, accuracy and computational efficiency. Regarding the latter, the 2D analysis of GBM was performed on a standard laptop (equipped with an 6th generation Intel CORE i7 CPU, and 8 gigabytes of RAM) and performed in a little less than 1 minute, which as a first indication is in line with the current state of the art. However, the tool topochecker still does not scale well to 3D image analysis, as execution time for a 3D image (resolution: $512\times 512\times 1024$, about 6 million points) on the same machine takes about half an hour. We envisage that new algorithms (mostly, for statistical cross-correlation) and the adoption of specialised imaging libraries—in place of the general-purpose graph-based approach which is currently implemented—may improve performance considerably.

6.2 Validation

The work presented in this section is aimed at providing an illustration of the analysis capabilities of our logic-based methodology, rather than providing complete clinical case studies. For instance, consider the glioblastoma specification, which is rather concise, consisting of a less than 30 lines long logical specification, and a simple preprocessing step. Although such procedure was successfully tested on five images from different sources and acquired in very different conditions, this is certainly not sufficient to validate our example as a glioblastoma segmentation methodology for future clinical usage. Future work aims at improving the method, eliminating corner cases in the formulas as much as possible, making it robust to different acquisition conditions and properly validating it. More generally speaking, clinical experimentation is the next step in our research programme.

However, some conclusions can already be drawn from the data we have, both with respect to efficiency and to accuracy of the obtained results.

Analysis time is proportional to the size of the image (the algorithm is linear). In the glioblastoma example, MR-FLAIR very often has a slice size of $256 \times 256$ pixels, multiplied by $20-30$ slices. As a rough estimate, the execution time for the analysis of a single $1024 \times 1024$-voxels slice—including preprocessing—on a standard laptop (equipped with an Intel CORE i7 CPU, and 8 gigabytes of RAM) currently stays below one minute. This information, although not being a fully fledged benchmark, provides a first indication that, efficiency-wise, our approach is in par with the state of the art in semi-automatic glioblastoma segmentation procedures (see for example [38]). We remark that our procedure makes use of a prototype general-purpose model checker, that could be amenable to further optimisation, e.g. employing specialised, well-known flood-filling algorithms for images for model checking the surrounded connective—in place of the current graph-theoretical method.

A preliminary assessment of the quality of the obtained results in the case of glioblastoma was performed for a patient of the A.O.U.S. university hospital. The patient underwent first surgery and then radiotherapy. We compared our results on the post-surgery MR-FLAIR with target volumes delineated on the pre-treatment Computed Tomography (CT) by one experienced radiotherapist. In particular, we considered the gross tumour volume (GTV), i.e. what can be seen or imaged, and the clinical target volume (CTV), which contains the GTV, plus a margin for sub-clinical disease spread which therefore cannot be fully imaged [15]. Usually for glioblastomas, the CTV is defined as a 2–2.5-cm isotropic expansion of GTV within the brain. In order to quantify the effectiveness of our segmentation, we computed the Dice coefficient ($DC$), that we used to measure the morphological similarity between the manual segmentation $MS$ and automatic segmentation $AS$. The coefficient is defined as $DC=\frac{2V( MS \cap AS )}{V( MS )+V( AS )}$, where V(a) is the volume of a, that is, the number of voxels that belong a; $DC$ ranges from 0 to 1; 0 indicates no overlap, and 1 indicates complete overlap. The CT volume was co-registered to the FLAIR volume. Then, we considered the region R obtained as the union of the oedema and tumour regions, as found using our method. We compared R to the GTV contour, and furthermore we compared R, expanded by 2.5cm (as explained above) to the CTV contour. We obtained $DC=0.76$ for GTV and $DC=0.81$ for CTV. Although a single case does not have clinical significance, these results are very encouraging, and aligned with state-of-the-art methods for automatic and semi-automatic segmentation of glioblastoma [35]. In [11], a variant of the method we described was assessed on a dataset of 7 patients affected by GBM, that have undergone radiotherapy. Segmentation results were evaluated using the Dice coefficient and the percent (0.95) Hausdorff distance (HD) between obtained segmentation volumes and the CTV manually delineated by an expert radiotherapist for radiotherapy planning. The results are shown in Table 2. The evaluation was performed on a midrange portable with an intel i7 CPU and 8 GB of RAM, the same machine used for the other experiments in the current paper. The average execution time per patient (3D image size: 256 $\times$ 256 $\times$ 40) was 10 minutes.

The state of the art in automated glioblastoma segmentation is represented by the Brain Tumor Image Segmentation Benchmark (BraTS) [60]. The top results in most recent editions, as already mentioned, are almost exclusively based on machine learning algorithms. The BraTS challenge is aimed at segmentation of the GTV, as opposed to the CTV that was studied in [11]. A direct comparison is therefore not possible. Future work will be directed to clinical studies of procedures formalised using spatial logics, including (possibly refined) versions of the one we presented, and to comparison with existing benchmarks and methods for each type of study.

Table 2 Score of comparison with manual segmentation (from [11])

Finally, we note that numeric thresholds and other parameters (e.g. the number of nested $\mathtt N$ constructs in some formulas, the number of bins for statistical analysis, etc.) have been chosen by the medical physicist in charge of the analysis, on the basis of expert knowledge on the matter and in some cases by trial-and-error. The values that we used might prove stable in clinical validation (and this is the purpose of the preliminary normalisation of images that we use), but this is not yet to be taken for granted, or even to be expected in more general situations. Instead, parameter calibration on a per-image or per-study basis will be an important subject in our future research. Such calibration may be fully automatic (e.g. through machine learning techniques), but this is just one possibility. It would also make sense to adopt a semi-automatic approach (which is also frequent in state-of-the-art techniques, see e.g. [35, 38, 72, 80]), involving human interaction with an expert to merely calibrate the parameters, rather than performing a full manual segmentation, in order to save a large part of the time (and costs) required for preparation to radiotherapy or surgery.

7 Conclusions and future work

This work provides a first, promising exploration of logical methods for declarative medical image analysis in the domain of radiotherapy. A declarative approach makes analysis transparent, reproducible, human-readable, and exchangeable, and permits domain experts who are not technicians to understand the specifications. Such advantages are akin to those obtained in other domains, such as the application of the Structured Query Language (SQL) in the field of databases, or the introduction of query languages (XPATH, XSLT, ...) in semi-structured data management.

Logical properties are used as classifiers for points of an image; this can be used both for colouring regions that may be similar to diseased tissues, and therefore being diseased tissue in turn, and for colouring regions corresponding to organs of the human body. Envisaged applications range from contouring to computer-aided diagnosis. Our logic ImgQL is able to predicate on both shortest-path and Euclidean distance at the same time, and topochecker implements both operators. In MI, shortest-path distances proved useful so far mostly to speed up interactive development; this is implementation dependent, as the Modified Dijkstra transform that we use (see Sect. 3.2) currently performs faster than Maurer distance transform in our tests. We also considered the embedding of specific operators for MI in ImgQL such as an operator for texture analysis based on first-order statistical methods. Other options and operators could be considered following a similar approach, providing a way to include state-of-the-art analysis techniques that can be conveniently combined using the spatial operators of the logic.

It is noteworthy that the analysis we designed for glioblastoma segmentation can be used, with mild modifications, also to analyse the whole 3D volume of an image at once. 3D analysis is a relatively new application in medical imaging, leveraging the precision/efficiency trade-off of more classical methods. Furthermore, 3D analysis may be combined with existing applications of 3D printing in preparation for surgery (see [68]), by providing practitioners with models of a patient’s body, with the relevant regions, identified by our method, printed in different colours. Such aspects constitute a further interesting line of research for future work.

Part of our ongoing work consists in identifying novel logical operators that are useful in medical imaging. So far, we only used operators that classify individual pixels or voxels. However, drawing inspiration from the family of region calculi (see [3]), one could also classify regions, taking advantage of “collective” observations on sets of voxels that belong to the same area. Some work in this direction is [23], including the definition of operators related to connectedness of regions; further work will be directed to the investigation of properties related to the size of regions, or to their morphological properties. Also, the “distance-bounded surrounded” operator defined in [64] could be useful in medical imaging. A limitation of the model checking algorithm in [64] is its quadratic complexity. We have shown that the application of distance transforms yields a linear algorithm for a weaker variant of the bounded surrounded operator for the case of images (that is, regular grids).

We recall that topochecker is a spatio-temporal model checker. Temporal reasoning could be exploited in future work to consider, for instance, the sequence of acquisitions of a patient in order to reason about the evolution of image features such as tumours, which is very important in radiotherapy applications.

Our experiments show that typical analyses carried out using spatial model checking in medical imaging require careful calibration of numeric parameters (for example, a threshold for the distance between a tumour and the associated oedema, or the size of areas identified by a formula, that are small enough to be considered noise, and ought be filtered out). The calibration of such parameters might be performed using machine learning techniques. In this respect, future work could be focused on the application, in the context of our research line, of the methodology used in the development of the logic SpaTeL, aimed at signal analysis (see [6, 7, 42, 45]), that pursues machine learning of the logical structure of image features. We emphasise that such a development, if implemented, would be a radical improvement in application of machine learning to medical imaging. It can be framed under the recent research trend on explainable artificial intelligence, as it would yield a procedure that can explain in terms of a human-readable language the methodology that a machine learning algorithm extrapolates from data. Our topological approach to spatial logics would be a key enabling technique for this purpose, as the formulas obtained in the SpaTeL approach are not meant to be intelligible by humans. It is worth noting that machine learning and deep learning methods have also been applied to the detection of tumours in very recent literature [4, 74]. On the other hand, our application of machine learning could as well be focused simply on the identification of numeric parameters, rather than logic formulas, that may depend on complex features of images.

The example of glioblastoma that we illustrated in Sect. 6.1 has immediate practical relevance. As we already mentioned, improvement and validation of the procedure are in progress; see for instance [10] for a revised version of the tool including validation of glioblastoma segmentation on a larger dataset. The normalisation step that we employ could be improved using state-of-the-art methods (see [54, 57], and the references therein).

Planned future developments also include means for interactive refinement of analysis, based on visual fine-tuning of specific values (e.g. thresholds or distances) that may have a non-linear effect on the results of complex queries, with significant impact on methods that require human interaction—e.g. interactive segmentation in preparation for surgery, or contouring for radiotherapy planning.