Top

Published in:

2019 | OriginalPaper | Chapter

Innovating Medical Image Analysis via Spatial Logics

Authors : Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink

Published in: From Software Engineering to Formal Methods and Tools, and Back

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Current computer-assisted medical imaging for the planning of radiotherapy requires high-level mathematical and computational skills. These are often paired with the case-by-case integration of highly specialised technologies. The lack of modularity at the right level of abstraction in this field hinders research, collaboration and transfer of expertise among medical physicists, engineers and technicians. The longer term aim of the introduction of spatial logics and spatial model checking in medical imaging is to provide an open platform introducing declarative medical image analysis. This will provide domain experts with a convenient and very concise way to specify contouring and segmentation operations, grounded on the solid mathematical foundations of Topological Spatial Logics. We show preliminary results, obtained using the spatial model checker VoxLogicA, for the automatic identification of specific brain tissues in a healthy brain and we discuss a selection of challenges for spatial model checking for medical imaging.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Improving Software Engineering Research Through Experimentation Workbenches

next chapter Formal Methods in Designing Critical Cyber-Physical Systems

Topochecker: a topological model checker, see http://topochecker.isti.cnr.it, https://github.com/vincenzoml/topochecker.

Part of the central nervous system in the brain.

Place where neurons are located in the outer part of the brain.

VoxLogicA: https://github.com/vincenzoml/VoxLogicA.

Sometimes called von Neumann adjacency. The relation is reflexive and symmetric.

The reader interested in the formal definition of closure spaces and on their properties is referred to the literature (see e.g. [12, 13, 21‐23] and references therein). Here it suffices to say that \(\mathcal {C}(Y)\) is essentially the set of points close to any point in Y; note that, since closure spaces generalize topological spaces, in the latter, the closure operator \(\mathcal {C}\) coincides with topological closure, so that, for instance, in the monodimensional Euclidean space \(\mathbb {R}\), \(\mathcal {C}([0,1))= \mathcal {C}((0,1))=\mathcal {C}((0,1])=\mathcal {C}([0,1])=[1,0]\).

We refer to [13] for a discussion on paths on the more general class of closure spaces, including e.g. Euclidean spaces, including e.g. Euclidean spaces.

Note that this colour does not correspond to any atomic predicate and so it is not part of the model; we use it only for illustration purposes.

See https://brainweb.bic.mni.mcgill.ca/brainweb/anatomic_normal_20.html (Publicly available).

The NIfTI file format is a special data format by the Neuro-imaging Informatics Technology Initiative, https://nifti.nimh.nih.gov/.

Again, note that we are processing a 3D image.

See http://brainweb.bic.mni.mcgill.ca/brainweb/anatomic_normal_20.html.

\(Dice = 2*\text {TP} / (2*\text {TP} + \text {FN} +\text {FP})\), where \(\text {TP}\) denotes True Positive and \(\text {FN}\) denotes False Negative.

The Insight Segmentation and Registration Toolkit, see https://itk.org and http://www.simpleitk.org.

Some operators may be derived from others; for this reason in the definition of the language we use a minimal set of connectives. As usual in logics, there are several different choices for such a set.

Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4CrossRefMATH

Aubert-Broche, B., Griffin, M., Pike, G., Evans, A., Collins, D.: Twenty new digital brain phantoms for creation of validation image data bases. IEEE Trans. Med. Imaging 25(11), 1410–1416 (2006). https://doi.org/10.1109/TMI.2006.883453CrossRef

Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. (2019). https://doi.org/10.1007/s10009-019-00511-9. Online First

Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Talpin, J., Derler, P., Schneider, K. (eds.) Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, 29 September–02 October 2017, pp. 146–155. ACM (2017). https://doi.org/10.1145/3127041.3127050

Belmonte, G., et al.: A topological method for automatic segmentation of glioblastoma in mr flair for radiotherapy - ESMRMB 2017, 34th annual scientific meeting. Magn. Reson. Mater. Phys. Biol. Med. 30(S1), 437 (2017). https://doi.org/10.1007/s10334-017-0634-zCrossRef

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: ter Beek, M.H., Loreti, M. (eds.) Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016. EPTCS, vol. 217, pp. 81–92 (2016). https://doi.org/10.4204/EPTCS.217.10

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, Part I. LNCS, vol. 11427, pp. 281–298. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_16. Preprint http://arxiv.org/abs/1811.05677CrossRef

van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Handbook of Spatial Logics [1], pp. 217–298

10.

Ciancia, V., Gilmore, S., Latella, D., Loreti, M., Massink, M.: Data verification for collective adaptive systems: spatial model-checking of vehicle location data. In: Eighth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW, pp. 32–37. IEEE Computer Society (2014)

11.

Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 297–311. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-49224-6_24CrossRef

12.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222–235. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_18CrossRef

13.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4) (2016). http://lmcs.episciences.org/2067

14.

Ciancia, V., Latella, D., Massink, M.: Embedding RCC8D in the collective spatial logic CSLCS. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 260–277. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_15CrossRef

15.

Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. STTT 20(3), 289–311 (2018). https://doi.org/10.1007/s10009-018-0483-8CrossRef

16.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 156–201. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_6CrossRefMATH

17.

Ciancia, V., Latella, D., Massink, M., Paškauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, 21–25 September 2015, pp. 74–79. IEEE Computer Society (2015). https://doi.org/10.1109/SASOW.2015.17

18.

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.) ISoLA 2016. LNCS, vol. 9952, pp. 657–673. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_46CrossRef

19.

Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (2001). http://books.google.de/books?id=Nmc4wEaLXFEC

20.

Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_19CrossRef

21.

Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251–266. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48384-5_17CrossRef

22.

Galton, A.: A generalized topological view of motion in discrete space. Theor. Comput. Sci. 305(1–3), 111–134 (2003). https://doi.org/10.1016/S0304-3975(02)00701-6MathSciNetCrossRefMATH

23.

Galton, A.: Discrete mereotopology. In: Calosi, C., Graziani, P. (eds.) Mereology and the Sciences. SL, vol. 371, pp. 293–321. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05356-1_11CrossRef

24.

Gambino, O., Rundo, L., Cannella, V., Vitabile, S., Pirrone, R.: A framework for data-driven adaptive GUI generation based on DICOM. J. Biomed. Inform. 88, 37–52 (2018). https://doi.org/10.1016/j.jbi.2018.10.009CrossRef

25.

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

26.

Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: SpaTel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, pp. 189–198. ACM, New York (2015)

27.

Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic + temporal logic = ? In: Handbook of Spatial Logics [1], pp. 497–564

28.

Kwan, R.S., Evans, A., Pike, G.: MRI simulation-based evaluation of image-processing and classification methods. IEEE Trans. Med. Imaging 18(11), 1085–1097 (1999)CrossRef

29.

Litjens, G.J.S., et al.: A survey on deep learning in medical image analysis. Med. Image Anal. 42, 60–88 (2017). https://doi.org/10.1016/j.media.2017.07.005CrossRef

30.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12CrossRefMATH

31.

Massink, M., Paškauskas, R.: Model-based assessment of aspects of user-satisfaction in bicycle sharing systems. In: Sotelo Vazquez, M., Olaverri Monreal, C., Miller, J., Broggi, A. (eds.) 18th IEEE International Conference on Intelligent Transportation Systems, pp. 1363–1370. IEEE (2015). https://doi.org/10.1109/ITSC.2015.224

32.

Mazzara, G., Velthuizen, R., Pearlman, J., Greenberg, H., Wagner, H.: Brain tumor target volume determination for radiation treatment planning through automated mri segmentation. Int. J. Radiat. Oncol. Biol. Phys. 59(1), 300–312 (2004)CrossRef

33.

Menze, B., et al.: The multimodal brain tumor image segmentation benchmark (BRATS). IEEE Trans. Med. Imaging 34(10), 1993–2024 (2015)CrossRef

34.

Nenzi, L., Bortolussi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: 8th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2014, Bratislava, Slovakia, 9–11 December 2014. ICST (2014)

35.

Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_2CrossRef

36.

Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR 1992), pp. 165–176. Morgan Kaufmann, Burlington (1992)

37.

Randell, D.A., Landini, G., Galton, A.: Discrete mereotopology for spatial reasoning in automated histological image analysis. IEEE Trans. Pattern Anal. Mach. Intell. 35(3), 568–581 (2013). https://doi.org/10.1109/TPAMI.2012.128CrossRef

38.

Spyridon (Spyros) Bakas, et al. (eds.): 2017 International MICCAI BraTS Challenge: Pre-conference Proceedings, September 2017. https://www.cbica.upenn.edu/sbia/Spyridon.Bakas/MICCAI_BraTS/MICCAI_BraTS_2017_proceedings_shortPapers.pdf

Title: Innovating Medical Image Analysis via Spatial Logics
Authors: Gina Belmonte
Vincenzo Ciancia
Diego Latella
Mieke Massink
Publisher: Springer International Publishing
Book: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner