# Towards a Spatial Model Checker on GPU

Laura Bussi, Vincenzo Ciancia, Fabio Gadducci

► To cite this version:

Laura Bussi, Vincenzo Ciancia, Fabio Gadducci. Towards a Spatial Model Checker on GPU. 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2021, Valletta, Malta. pp.188-196, 10.1007/978-3-030-78089-0_12. hal-03740266

HAL Id: hal-03740266

https://inria.hal.science/hal-03740266v1

Submitted on 29 Jul 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Towards a spatial model checker on GPU*

Laura Bussi¹, Vincenzo Ciancia², and Fabio Gadducci¹

¹ Dipartimento di Informatica, Università di Pisa

² Istituto di Scienza e Tecnologie dell'Informazione, CNR

**Abstract.** The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.

**Keywords:** Spatial logics · Model Checking · GPU computation

## 1 Introduction and background

Spatial and Spatio-temporal model checking have gained an increasing interest in recent years in various application domains, including collective adaptive [12, 11] and networked systems [5], runtime monitoring [17, 15, 4], modelling of cyber-physical systems [20] and medical imaging [13, 3]. Introduced in [7], VoxLogicA (*Voxel-based Logical Analyser*)<fnref n="3" /> caters for a declarative approach to (medical) image segmentation, supported by spatial model checking. A spatial logic is defined, tailored to high-level imaging features, such as regions, contact, texture, proximity, distance. Spatial operators are mostly derived from the *Spatial Logic of Closure Spaces* (SLCS, see Figure 1). Models of the spatial logic are (pixels of) images, with atomic propositions given by imaging features (e.g. colour, intensity), and spatial structure obtained via adjacency of pixels. SLCS features a modal operator *near*, denoting adjacency of pixels, and a reachability operator $\rho \phi_1[\phi_2]$, holding at pixel *x* whenever there is a path from *x* to a pixel *y* satisfying $\phi_1$, with all intermediate points, except the extremes, satisfying $\phi_2$.

The main case study of [7] is brain tumour segmentation for radiotherapy, using the BraTS 2017 public dataset of medical images [2]. An high-level specification for glioblastoma segmentation was proposed and tested using VoxLogicA,

<footnote>* Research partially supported by the MIUR Project PRIN 2017FTXR7S "IT- MaT-TerS" and by POR FESR Toscana 2014-2020 As. 1 - Az. 1.1.5 - S.A. A1 N. 7165 project STINGRAY. The authors are thankful to: Raffaele Perego, Franco Maria Nardini and the HPC-Lab at ISTI-CNR for a powerful GPU used in early development; Gina Belmonte, Diego Latella, and Mieke Massink, for fruitful discussions. The authors are listed in alphabetical order, having equally contributed to this work.</footnote>

<footnote n="3">³ VoxLogicA: see https://github.com/vincenzoml/VoxLogicA</footnote>
$$ \phi ::= p \mid \neg \phi \mid \phi_1 \wedge \phi_2 \mid \mathcal{N}\phi \mid \rho \phi_1[\phi_2] $$

<caption>**Fig. 1.** SLCS syntax. Atomic propositions *p* correspond to image properties (e.g. *in-tensity*, *colour*); boolean operators act pixel-wise; the *near* operator *N* denotes pixel *adjacency* (using *8-adjacency*: the pixels having a vertex in common with a given one).</caption>

resulting in a procedure that competes in accuracy with state-of-the-art techniques. In [6], also an accurate specification for nevus segmentation was presented. This paper introduces a novel development in the direction of taking advantage of Graphical Processing Units: high-performance, massively parallel computational devices. GPU computing differs from the *multi-core* paradigm of modern CPUs in many respects: the execution model is *Single Instruction Multiple Data*; the number of computation cores is high; the memory model is highly localised and synchronisation among parallel threads is very expensive. Each GPU core performs the same operation on different coordinates (a single pixel, in our case). The dimension of the problem (e.g. the size of an image) is provided to the GPU when the program (*kernel*) is launched, yet the number of threads does not scale with the problem size, being bounded by the number of computing units in the GPU. Currently, such a number is in the order of thousands, whereas the problem size may include millions of tasks. The problems that benefit the most of such architecture are the inherently massively parallel ones. In that case, the main issue is to minimise read/write operations from and to the GPU memory, and to turn a problem into a highly parallel implementation.

A substantial redesign is thus required to port existing algorithms to GPUs. *VoxLogicA-GPU* implements the core logical primitives of *VoxLogicA* on GPU, sharing motivation with a recent trend on implementing formal methods on GPU [8, 21, 22, 16, 18]. This paper aims to describe the tool architecture, including asynchronous execution of logical primitives on GPU and garbage collection, and to demonstrate a consistent efficiency improvement. In doing so, we had to overcome two major issues: implementing connected component labelling on GPUs and minimising the number of (computationally expensive) CPU ↔ GPU memory transfers. Our current results are very encouraging, obtaining a (task-dependent) speed-up of one or two orders of magnitude.

## 2 Functional Description and Implementation

*VoxLogicA-GPU*<fnref n="4" /> is a *global, explicit state* model checker, aiming at high efficiency and maximum portability. It is implemented in *FSharp*, using the *NET Core* infrastructure, and the *General-Purpose GPU computing* library *OpenCL*<fnref n="5" />. The choice of *OpenCL* is motivated by portability to different GPU brands.

<footnote n="4">⁴ *VoxLogicA-GPU* is Free and Open Source software. Its source code is currently available at https://github.com/vincenzoml/VoxLogicA/tree/experimental-gpu.</footnote>

<footnote n="5">⁵ *FSharp*: see https://fsharp.org. *NET Core*: see https://dotnet.microsoft.com. *OpenCL*: see https://www.khronos.org/opencl. *ITK*: see https://itk.org.</footnote>
VoxLogicA-GPU is a command line tool, accepting as input a text file describing the analysis, and a number of input images. The text file contains a set of logic formulas and parametrised, non-recursive macro abbreviations. As in [7], the tool expands macros, identifies the *ground* formulas (that is, without variables), and constructs a directed acyclic graph of *tasks* and *dependencies*. Such a graph is equivalent to the syntax tree, but it enjoys *maximal sharing*: no sub-formula is ever computed twice. In the CPU version, the tasks run in parallel on the available CPU cores, yielding a speed-up proportional to the degree of parallelism of the task graph and to the number of cores. In the GPU version, the tasks are currently executed asynchronously with respect to the main CPU execution thread, but sequentially: so-called *out-of-order execution* is left for future work.

The focus of this first release of VoxLogicA-GPU is on the *design* of a free and open source GPU-based infrastructure, with proven scalability. Thus, development has been narrowed to a core implementation that is powerful enough to reach the stated objectives, although not as feature-complete as VoxLogicA. In particular, the implemented primitives are those of SLCS plus basic arithmetics, and computation is restricted to 2D and integer-valued images. Implementation-wise, VoxLogicA-GPU is a command-line tool. It takes only one parameter, a text file containing the specification to be executed, i.e., a sequence of commands. Five commands are currently implemented: *let*, *load*, *save*, *print*, *import*. The model checking algorithm of VoxLogicA-GPU is shared with VoxLogicA. After parsing, parametric macros are expanded, while at the same time (to avoid explosion of the syntax tree) the aforementioned task graph is computed. A major issue is that each task allocates a memory area proportional to the size of the input image to store its results, thus *garbage collection* is required. The current strategy is a simple reference counting, as the number of reverse dependencies of each task (i.e. the tasks taking the given one as argument) is known before execution, and no task is created at run time. This problem is more relevant to the GPU implementation: as a GPU memory is usually smaller than a CPU one, and GPU buffers are explicitly allocated by the programmer, large formulas can easily lead to *Out of Memory* errors at run time. If a reference counter turns to 0, no more tasks take the given one as an input, and the pointer referencing the buffer can be disposed. As no pointer longer refers that GPU memory area, this can be reused. A task is an operator of the language or an output instruction. The semantics of the former is delegated to the GPU implementation of the VoxLogicA API, defining the core type *Value*, which is instantiated as a shorthand for a type called *GPUImage*. Such type represents a computation, asynchronously running on a GPU, whose purpose is to fill an image buffer. *GPUImage* contains a pointer to a buffer stored in the GPU, its imaging features, and an *OpenCL event* (an handle to the asynchronous computation). The latter is used to wait for termination before transferring the results to the CPU and to make task dependencies explicit to the GPU for proper sequencing. Since commands, parameters, and results must be transferred from the CPU to the GPU and back, keeping pointers to GPU buffers minimises this overhead, allowing for the reuse of partial results. Thus, data is transferred only at the beginning of the com-
putation and when retrieving results to be saved to disk. The model checker is
responsible for decreasing reference counts after each task terminates, and for
scheduling garbage collection when a reference counter reaches 0. Each operator
is implemented in a small module running on CPU, whose only purpose is to
prepare memory buffers and launch one or more kernels (i.e. functions running
on GPU). As in VoxLogicA, the reachability operator ρ φ₁[φ₂] is implemented
using connected components labelling.

## 2.1 Connected components labelling in VoxLogicA-GPU

We designed a simple algorithm for connected component labelling, biased to-
wards implementation simplicity, although efficient enough for our prototype.
Similarly to the classic result in [19], the algorithm exploits the *pointer jumping* technique<sup>6</sup>: see Algorithm 1 for the pseudo-code of the kernels (termination checking is omitted) and Figure 2 for an example. After initialisation, *mainIteration* is iterated. By pointer jumping, it converges in logarithmic time with respect to the number of pixels *N*, but it may fail to correctly label connected components with corners in specific directions (see Figure 2, Iteration 13). Then *reconnect* is called, checking if there are two adjacent pixels with different labels, and changing one of them (deterministically chosen) so that the two labels now coincide The way *reconnect* changes the image ensures that *mainIteration* will restart and will be enabled to converge again. The termination condition is reached when *reconnect* does not change the image, which requires a global check on its input and output. For checking termination we adopted a *reduce*-type operation<sup>7</sup>: it takes log(*N*) iterations, since it divides the image size at each iteration until a single-pixel image containing a boolean flag is obtained. If the termination condition is false, the algorithm restarts from *mainIteration*<sup>8</sup>. In most cases, *reconnect* is called a very small number of times before convergence, and the total number of iterations is in the order of log(*N*) (see [10] for details).

# 3 Preliminary evaluation

This section illustrates the scalability results obtained in our preliminary tests<fnref n="9" />.
Experiments have been executed on a machine equipped with an Intel Core
i9-9900K and a NVIDIA RTX 3080 GPU. This is indicative of the attainable
speed-up as both CPU and GPU are current, high-end (workstation-oriented)
devices. It is important to remark that CPU and GPU execution times are sub-
ject to high variability. Indeed, a highly parallel test may run about 8 times

<footnote n="6">⁶ Pointer jumping or path doubling is a design technique for parallel algorithms that operate on pointer structures, such as linked lists and directed graphs. It allows an algorithm to follow paths with a time complexity that is logarithmic with respect to the length of the longest path. It does this by “jumping” to the end of the path computed by neighbors. See https://en.wikipedia.org/wiki/Pointer_jumping.</footnote>

<footnote n="7">⁷ See e.g. https://en.wikipedia.org/wiki/MapReduce.</footnote>

<footnote n="8">⁸ Since checking termination takes log(N) iterations, instead of waiting for mainIteration to converge, reconnect is called each k iterations (k = 8 in the current implementation, which experimentally proved to be a reasonable compromise).</footnote>

<footnote n="9">⁹ All the tests we present, and the script to run them, are available in the source code repository https://github.com/vincenzoml/VoxLogicA/tree/experimental-gpu.</footnote>
<table><caption>**Algorithm 1:** Pseudocode for connected components labelling</caption><tr><td>1</td><td><b>initialization</b>(start: image of bool, output: image of int × int)</td></tr><tr><td>2</td><td>// parallel for on GPU</td></tr><tr><td>3</td><td><b>for</b> (i, j) ∈ <i>Coord</i>s <b>do</b></td></tr><tr><td>4</td><td><b>if</b> <i>start</i>(i,j) <b>then</b></td></tr><tr><td>5</td><td>&nbsp;&nbsp;&nbsp;&nbsp;<i>output</i>(i,j) = (i,j) // null otherwise</td></tr><tr><td>6</td><td><b>mainIteration</b>(start: image of bool, input, output: image of int × int)</td></tr><tr><td>7</td><td>// parallel for on GPU</td></tr><tr><td>8</td><td><b>for</b> (i, j) ∈ <i>Coord</i>s <b>do</b></td></tr><tr><td>9</td><td><b>if</b> <i>start</i>(i,j) <b>then</b></td></tr><tr><td>10</td><td>&nbsp;&nbsp;&nbsp;&nbsp;(i', j') = <i>input</i>(i,j) // pointer jumping</td></tr><tr><td>11</td><td>&nbsp;&nbsp;&nbsp;&nbsp;<i>output</i>(i,j) = <i>maxNeighbour</i>(<i>input</i>, i', j')</td></tr><tr><td>12</td><td><b>reconnect</b>(start: image of bool, input, output: image of int × int)</td></tr><tr><td>13</td><td>// parallel for on GPU</td></tr><tr><td>14</td><td><b>for</b> (i, j) ∈ <i>Coord</i>s <b>do</b></td></tr><tr><td>15</td><td><b>if</b> <i>start</i>(i,j) <b>then</b></td></tr><tr><td>16</td><td>&nbsp;&nbsp;&nbsp;&nbsp;(i', j') = <i>input</i>(i,j)</td></tr><tr><td>17</td><td>&nbsp;&nbsp;&nbsp;&nbsp;(a, b) = <i>maxNeighbour</i>(<i>input</i>, i, j)</td></tr><tr><td>18</td><td>&nbsp;&nbsp;&nbsp;&nbsp;(c, d) = <i>input</i>(i', j')</td></tr><tr><td>19</td><td><b>if</b> (a, b) > (c, d) <b>then</b></td></tr><tr><td>20</td><td>&nbsp;&nbsp;&nbsp;&nbsp;<i>output</i>(i', j') = (a, b) // Requires atomic write</td></tr></table>

faster on CPU with 16 cores (a current high-end desktop workstation) than a machine with 2 cores (a current travelling laptop), as witnessed by the law on theoretical speed-up given by parallel machines [14]. Since the range of current CPUs is highly variable, so are the execution times in our tests. This fact also explains the different speedup in our tests comparing CPU and GPU on sequential and parallel tasks (see Figure 3 and Figure 4). In the parallel test, all the 16 cores of the chosen CPU are exploited, thus the CPU is more efficient.

We built two kinds of large formulas for stressing the tool: sequential (i.e. of shape $f(g(...(x)))$ and “parallel” ones, where the operators are composed in order to maximise parallelism. More precisely, formulas are written in order to have many independent sub-formulas (i.e., having shape $f(g(..., ...), h(..., ...))$). In the CPU implementation, such sub-formulas can be computed in parallel, up to the number of available cores. Note again that maximising CPU usage entails a smaller speedup for the GPU. Figure 3 and 4 report execution times for each type of test. Each row reports the number of tasks to execute (i.e, the number of nodes in the directed acyclic graph described in Section 2), and the obtained speed-up for the two GPU algorithms. In all cases, **VoxLogicA-GPU** achieves a relevant speed-up. The CPU version performs better on very small formulas, due to the overhead needed to set up GPU computation. The version with garbage collection is much slower than the version without. This is due to garbage collection being run in the current implementation as soon as reference counts reach 0, and recall that memory deallocation and reallocation is particularly expensive on GPUs. Obvious improvements are expected by scheduling garbage collection
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** CC-labelling of a 2048 × 2048 pixels image in 24 iterations. Different colours represent different labels. Reconnect is called every 8 main iterations. Iteration 13: the main iterations converged; the image does not change until iteration 16 (reconnect). Iteration 17: label propagation after reconnect. Iteration 24: termination.</figcaption></figure>

<table><caption>**Fig. 3.** Execution times for the sequential test.</caption><thead><tr><th rowspan="2">No. of Tasks</th><th>CPU</th><th colspan="2">GPU</th><th colspan="2">GPU-GC</th></tr><tr><th>Time</th><th>Time</th><th>Speed-up</th><th>Time</th><th>Speed-up</th></tr></thead><tbody><tr><td>11</td><td>410ms</td><td>190ms</td><td>2.15</td><td>200ms</td><td>2.05</td></tr><tr><td>35</td><td>1470ms</td><td>190ms</td><td>7.73</td><td>230ms</td><td>6.39</td></tr><tr><td>67</td><td>1800ms</td><td>190ms</td><td>9.47</td><td>230ms</td><td>7.82</td></tr><tr><td>195</td><td>8200ms</td><td>200ms</td><td>41.00</td><td>320ms</td><td>25.62</td></tr><tr><td>259</td><td>10900ms</td><td>210ms</td><td>51.90</td><td>360ms</td><td>30.27</td></tr><tr><td>1027</td><td>43600ms</td><td>350ms</td><td>124.57</td><td>980ms</td><td>44.48</td></tr><tr><td>4099</td><td>174600ms</td><td>Out of memory</td><td>-</td><td>4100ms</td><td>42.58</td></tr><tr><td>8195</td><td>479000ms</td><td>Out of memory</td><td>-</td><td>12000ms</td><td>39.91</td></tr></tbody></table>

to be run only when a memory usage threshold is reached. However, we plan to design a garbage collector which is more specific to the execution patterns of a model checker. We also carried out a preliminary assessment of the brain tumour segmentation case study of [7]. Given the current restrictions of **VoxLogicA-GPU** to 2D images and the core logical primitives (see Section 2), it is only possible to use a simplified dataset and specification, obtaining too small tasks for interesting measurements. We omit the full results (see [10]), but we note that a mild speed-up was obtained: this is interesting, as the CPU version uses a state-of-the-art imaging library designed for high efficiency.

## 4 Conclusions and Future Work

Our preliminary evaluation of spatial model checking on GPU is encouraging: large formulas benefit most, with significant speedups. Connected components labelling will be a focus for future work: indeed, the topic is very active, and our simple, proof-of-concept algorithm might well be replaced by state-of-the-art procedures (see e.g. the recent [1]). The currently attained speed-up can be used, for instance, for interactive calibration of parameters or for automated parameter optimisation, e.g. using gradient descent algorithms. However, given the peak performance of recent GPUs, our results are just the tip of the iceberg of what can be achieved. Future work will concentrate on fully exploiting more powerful
<table><caption>Fig. 4. Execution times for the parallel test.</caption><thead><tr><th rowspan="2">No. of Tasks</th><th colspan="2">CPU</th><th colspan="2">GPU</th><th colspan="2">GPU-GC</th></tr><tr><th>Time</th><th>Time</th><th>Speed-up</th><th>Time</th><th>Speed-up</th><th>Speed-up</th></tr></thead><tbody><tr><td>10</td><td>70ms</td><td>180ms</td><td>0.38</td><td>200ms</td><td>0.35</td><td>0.35</td></tr><tr><td>26</td><td>260ms</td><td>180ms</td><td>1.44</td><td>200ms</td><td>1.30</td><td>1.30</td></tr><tr><td>43</td><td>310ms</td><td>180ms</td><td>1.72</td><td>210ms</td><td>1.47</td><td>1.47</td></tr><tr><td>61</td><td>500ms</td><td>190ms</td><td>2.63</td><td>210ms</td><td>2.38</td><td>2.38</td></tr><tr><td>73</td><td>510ms</td><td>190ms</td><td>2.68</td><td>220ms</td><td>2.31</td><td>2.31</td></tr><tr><td>174</td><td>860ms</td><td>200ms</td><td>4.30</td><td>270ms</td><td>3.18</td><td>3.18</td></tr><tr><td>323</td><td>1600ms</td><td>220ms</td><td>7.27</td><td>340ms</td><td>4.70</td><td>4.70</td></tr><tr><td>472</td><td>2400ms</td><td>290ms</td><td>8.27</td><td>430ms</td><td>5.58</td><td>5.58</td></tr><tr><td>621</td><td>3000ms</td><td>360ms</td><td>8.33</td><td>510ms</td><td>5.88</td><td>5.88</td></tr><tr><td>1813</td><td>8800ms</td><td>Out of memory</td><td>-</td><td>1200ms</td><td>7.33</td><td>7.33</td></tr><tr><td>3005</td><td>14600ms</td><td>Out of memory</td><td>-</td><td>2000ms</td><td>7.30</td><td>7.30</td></tr></tbody></table>

GPUs, using out-of-order execution to permit the execution of more independent tasks at the same time, and taking into account GPU-specific architectural features (memory banking, number of channels, etc.). Making *VoxLogicA-GPU* feature-complete with respect to *VoxLogicA* is also a goal. In this respect, we remark that although in this work we decided to go through the “GPU-only” route, future developments will also consider a *hybrid* execution mode with some operations executed on the CPU, so that existing primitives in *VoxLogicA* can be run in parallel with those that have a GPU implementation. Usability of *VoxLogicA-GPU* would be greatly enhanced by a user interface. However, understanding modal logical formulas is generally considered a difficult task, and cognitive/human aspects may become predominant with respect to technological concerns. Formal methods could be used to mitigate such concerns (see e.g. [9]).

## References

1. Allegretti, S., Bolelli, F., Grana, C.: Optimized block-based algorithms to label connected components on GPUs. IEEE Transactions on Parallel and Distributed Systems **31**(2), 423–438 (2020)

2. Bakas, S., Akbari, H., Sotiras, A., Bilello, M., Rozycki, M., Kirby, J.S., Freymann, J.B., Farahani, K., Davatzikos, C.: Advancing the cancer genome atlas glioma MRI collections with expert segmentation labels and radiomic features. Scientific Data **4** (2017)

3. Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Software Tools for Technology Transfer **22**(2), 195–217 (2020)

4. Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Talpin, J., Derler, P., Schneider, K. (eds.) MEMOCODE 2017. pp. 146–155. ACM (2017)

5. Bartocci, E., Gol, E., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Transactions on Control of Network Systems **5**(1), 308–320 (2016)
6. Belmonte, G., Broccia, G., Ciancia, V., Latella, D., Massink, M.: Feasibility of spatial model checking for nevus segmentation. In: Bliudze, S., Semini, L. (eds.) FORMALISE@ICSE 2021. p. To appear (2021)

7. Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Voxlogica: A spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281–298. Springer (2019)

8. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: IPDPS 2013. pp. 1025–1036. IEEE Computer Society (2013)

9. Broccia, G., Milazzo, P., Ölveczky, P.C.: Formal modeling and analysis of safety-critical human multitasking. Innovations in Systems and Software Engineering 15(3-4), 169–190 (2019)

10. Bussi, L., Ciancia, V., Gadducci, F.: A spatial model checker in GPU (extended version). CoRR abs/2010.07284 (2020)

11. Ciancia, V., Latella, D., Massink, M., Paškauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISOLTA 2016. LNCS, vol. 9952, pp. 657–673 (2016)

12. Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Software Tools for Technology Transfer 20(3), 289–311 (2018)

13. Grosu, R., Smolka, S., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Communications of ACM 52(3), 97–105 (2009)

14. Gustafson, J.L.: Reevaluating Amdahl's law. Communications of the ACM 31(5), 532–533 (1988)

15. Ma, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L.: SaSTL: Spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: ICCPS 2020. pp. 51–62. IEEE (2020)

16. Neele, T., Wijs, A., Bošnački, D., van de Pol, J.: Partial-order reduction for GPU model checking. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 357–374. Springer (2016)

17. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Logical Methods in Computer Science 14(4) (2018)

18. Osama, M., Wijs, A.: Parallel SAT simplification on GPU architectures. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 21–40. Springer (2019)

19. Shiloach, Y., Vishkin, U.: An O(logn) parallel connectivity algorithm. Journal of Algorithms 3(1), 57–67 (1982)

20. Tsigkanos, C., Kehrer, T., Ghezzi, C.: Modeling and verification of evolving cyberphysical spaces. In: Bodden, E., Schäfer, W., van Deursen, A., Zisman, A. (eds.) ESEC/FSE 2017. pp. 38–48. ACM (2017)

21. Wijs, A., Bošnački, D.: Many-core on-the-fly model checking of safety properties using GPUs. Software Tools for Technology Transfer 18(2), 169–185 (2016)

22. Wijs, A., Neele, T., Bošnački, D.: GPUexplore 2.0: Unleashing GPU explicit-state model checking. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 694–701. Springer (2016)