2016
Conference article  Open Access

From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging

Belmonte G., Ciancia V., Latella D., Massink M.

Spatial Model-checking  Model logics  Medical Imaging  D.2.4 model checking  Logic in Computer Science (cs.LO)  Spatial Logics  Software/Program Verification  Computer Vision and Pattern Recognition (cs.CV)  FOS: Computer and information sciences  J.3 medical information systems  Computer Science - Logic in Computer Science  Mathematical Logic  F.4.1 modal logic  Computer Science - Computer Vision and Pattern Recognition 

Recent research on formal verification for Collective Adaptive Systems (CAS) pushed advancements in spatial and spatio-temporal model checking, and as a side result provided novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such technologies show potential for ground-breaking innovation. In this position paper, we present a preliminary investigation centred on applications of spatial model checking to MI. The focus is shifted from pure logics to a mixture of logical, statistical and algorithmic approaches, driven by the logical nature intrinsic to the specification of the properties of interest in the field. As a result, novel operators are introduced, that could as well be brought back to the setting of CAS.

Source: FORECAST 2016 - Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, pp. 81–92, Vienna, Austria, 8 July 2016


[1] C. Baier & J. Katoen (2008): Principles of model checking. MIT Press.
[2] E. Bartocci, L. Bortolussi, D. Milios, L. Nenzi & G. Sanguinetti (2015): Studying Emergent Behaviours in Morphogenesis Using Signal Spatio-Temporal Logic, pp. 156-172. Springer, doi:10.1007/978-3-319-26916- 0 9.
[3] J. van Benthem & G. Bezhanishvili (2007): Modal Logics of Space. In: Handbook of Spatial Logics, Springer, pp. 217-298, doi:10.1007/978-1-4020-5587-4 5.
[4] L. Bortolussi, J. Hillston, Latella. D. & M. Massink (2013): Continuous approximation of collective system behaviour: A tutorial. Perform. Eval. 70(5), pp. 317-349, doi:10.1016/j.peva.2013.01.001.
[5] Luca Bortolussi & Jane Hillston (2012): Fluid Model Checking. In: CONCUR 2012 - Concurrency Theory - 23rd International Conference, Lecture Notes in Computer Science 7454, Springer, pp. 333-347, doi:10.1007/978-3-642-32940-1 24.
[6] K.K. Brock (2014): Image processing in radiation therapy. CRC Press, doi:10.1118/1.4905156.
[7] G. Castellano, L. Bonilha, L.M. Li & F. Cendes (2004): Texture analysis of medical images. Clinical Radiology 59(12), pp. 1061-1069, doi:10.1016/j.crad.2004.07.008.
[8] C.-C. Chen, J.S. DaPonte & M.D. Fox (1989): Fractal feature analysis and classification in medical imaging. IEEE Transactions on Medical Imaging 8(2), pp. 133-142, doi:10.1109/42.24861.
[9] G. Chetelat & J. Baron (2003): Early diagnosis of alzheimer's disease: contribution of structural neuroimaging. NeuroImage 18(2), pp. 525-541, doi:10.1016/S1053-8119(02)00026-5.
[10] V. Ciancia, S. Gilmore, D. Latella, M. Loreti & M. Massink (2014): 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, IEEE Computer Society, pp. 32-37, doi:10.1109/SASOW.2014.16.
[11] V. Ciancia, G. Grilletti, D. Latella, M. Loreti & M. Massink (2015): An Experimental Spatio-Temporal Model Checker. In: Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops, Lecture Notes in Computer Science 9509, Springer, pp. 297-311, doi:10.1007/978-3-662-49224-6 24.
[12] V. Ciancia, D. Latella, M. Loreti & M. Massink (2014): Specifying and Verifying Properties of Space. In: Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, Lecture Notes in Computer Science 8705, Springer, pp. 222-235, doi:10.1007/978-3-662-44602-7 18.
[13] V. Ciancia, D. Latella, M. Massink & R. Pakauskas (2015): Exploring Spatio-temporal Properties of BikeSharing Systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops, IEEE Computer Society, pp. 74-79, doi:10.1109/SASOW.2015.17.
[14] F. Davnall, C. S. P. Yip, G. Ljungqvist, M. Selmi, F. Ng, B. Sanghera, B. Ganeshan, K. A. Miles, G. J. Cook & V. Goh (2012): Assessment of tumor heterogeneity: an emerging imaging tool for clinical practice? Insights into Imaging 3(6), pp. 573-589, doi:10.1007/s13244-012-0196-6.
[15] R. De Nicola, J. Katoen, D. Latella, M.. Loreti & M. Massink (2007): Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), pp. 42-70, doi:10.1016/j.tcs.2007.05.008.
[16] S. De Santis, M. Drakesmith, S. Bells, Y. Assaf & D. K. Jones (2014): Why diffusion tensor MRI does well only some of the time: Variance and covariance of white matter tissue microstructure attributes in the living human brain. NeuroImage 89, pp. 35-44, doi:10.1016/j.neuroimage.2013.12.003.
[17] Kunio Doi (2007): Computer-aided diagnosis in medical imaging: Historical review, current status and future potential. Comput. Med. Imaging Graph. 31(4-5), pp. 198-211, doi:10.1016/j.compmedimag.2007.02.002.
[18] R. Fabbri, L. Da Fontoura Da Costa, J. C. Torelli & O. M. Bruno (2008): 2D Euclidean Distance Transform Algorithms: A Comparative Survey. ACM Comput. Surv. 40(1), pp. 2:1-2:44, doi:10.1145/1322432.1322434.
[19] E.A. Gol, E. Bartocci & C. Belta (2014): A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108-113, doi:10.1109/CDC.2014.7039367.
[20] N. Gordillo, E. Montseny & E. Sobrevilla (2013): State of the art survey on MRI brain tumor segmentation. Magn. Reson. Imaging. 31(8), pp. 1426-1438, doi:10.1016/j.mri.2013.05.002.
[21] G. J. Grevera (2007): Distance Transform Algorithms And Their Implementation And Evaluation. In: Deformable Models, Springer Science, pp. 33-60, doi:10.1007/978-0-387-68413-0 2.
[22] R. Grosu, S.A. Smolka, F. Corradini, A. Wasilewska, E. Entcheva & E. Bartocci (2009): Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), pp. 97-105, doi:10.1145/1467247.1467271.
[23] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Grosu & C. Belta (2015): 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 '15, ACM, New York, NY, USA, pp. 189-198, doi:10.1145/2728606.2728633.
[24] F. Han, H. Wang, G. Zhang, H. Han, B. Song, L. Li, W. Moore, H. Lu, H. Zhao & Z. Liang (2014): Texture Feature Analysis for Computer-Aided Diagnosis on Pulmonary Nodules. Journal of Digital Imaging 28(1), pp. 99-115, doi:10.1007/s10278-014-9718-8.
[25] T. Heinonen, T. Arola, A. Kalliokoski, P. Dastidar, M. Rossi, S. Soimakallio, J. Hyttinen & H. Eskola (2009): Computer Aided Diagnosis Tool for the Segmentation and Texture Analysis of Medical Images. In: IFMBE Proceedings, Springer Science, pp. 274-276, doi:10.1007/978-3-642-03879-2 77.
[26] A. Kassner & R. E. Thornhill (2010): Texture Analysis: A Review of Neurologic MR Imaging Applications. Am. J. Neuroradiol. 31(5), pp. 809-816, doi:10.3174/ajnr.A2061.
[27] R. Kimmel, N. Kiryati & A. M. Bruckstein (1996): Sub-pixel distance maps and weighted distance transforms. Journal of Mathematical Imaging and Vision 6(2), pp. 223-233, doi:10.1007/BF00119840.
[28] R. Kontchakov, A. Kurucz, F. Wolter & M. Zakharyaschev (2007): Spatial Logic + Temporal Logic = ? In: Handbook of Spatial Logics, Springer, pp. 497-564, doi:10.1007/978-1-4020-5587-4 9.
[29] O. Kutz, F. Wolter, H. Sturm, N. Suzuki & M. Zakharyaschev (2003): Logics of metric spaces. ACM Trans. Comput. Log. 4(2), pp. 260-294, doi:10.1145/635499.635504.
[30] D. Latella, M. Loreti & M. Massink (2015): On-the-fly PCTL fast mean-field approximated modelchecking for self-organising coordination. Science of Computer Programming 110, pp. 23 - 50, doi:10.1016/j.scico.2015.06.009.
[31] C. Li, J. G. Herndon, F. J. Novembre & X. Zhang (2015): A Longitudinal Magnetization Transfer Imaging Evaluation of Brain Injury in a Macaque Model of NeuroAIDS. AIDS Research and Human Retroviruses 31(3), pp. 335-341, doi:10.1089/aid.2014.0166.
[32] R. Lopes, A. Ayache, N. Makni, P. Puech, A. Villers, S. Mordon & N. Betrouni (2011): Prostate cancer characterization on MR images using fractal features. Med. Phys. 38(1), p. 83, doi:10.1118/1.3521470.
[33] Aiello M., Pratt-Hartmann I. & van Benthem J., editors (2007): Handbook of Spatial Logics. Springer, doi:10.1007/978-1-4020-5587-4.
[34] C.R. Maurer, Rensheng Qi & V. Raghavan (2003): A linear time algorithm for computing exact Euclidean distance transforms of binary images in arbitrary dimensions. IEEE Transactions on Pattern Analysis and Machine Intelligence 25(2), pp. 265-270, doi:10.1109/TPAMI.2003.1177156.
[35] L. Nenzi & L. Bortolussi (2014): 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, December 9-11, 2014, ICST, doi:10.4108/icst.valuetools.2014.258183.
[36] L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti & M. Massink (2015): Qualitative and Quantitative Monitoring of Spatio-Temporal Properties. In: Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, Lecture Notes in Computer Science 9333, Springer, pp. 21-37, doi:10.1007/978-3-319-23820-3 2.
[37] O. Prvu & D. Gilbert (2016): A Novel Method to Verify Multilevel Computational Models of Biological Systems Using Multiscale Spatio-Temporal Meta Model Checking. PLoS ONE 11(5), pp. 1-43, doi:10.1371/journal.pone.0154847.
[38] D. Rodriguez Gutierrez, A. Awwad, L. Meijer, M. Manita, T. Jaspan, R. A. Dineen, R. G. Grundy & D. P. Auer (2013): Metrics and Textural Features of MRI Diffusion to Improve Classification of Pediatric Posterior Fossa Tumors. American Journal of Neuroradiology 35(5), pp. 1009-1015, doi:10.3174/ajnr.A3784.
[39] N. Sharma, A. Ray, S. Sharma, K.K. Shukla, S. Pradhan & L. Aggarwal (2008): Segmentation and classification of medical images using texture-primitive features: Application of BAM-type artificial neural network. J Med Phys 33(3), p. 119, doi:10.4103/0971-6203.42763.
[40] G.N. Srinivasan & G. Shobha (2012): Statistical Texture Analysis. In: Proceedings of World Accademy of Science, Engineering and Technology, 36, pp. 1264-1269.
[41] A. Sundstrom, E. Grabocka, D. Bar-Sagi & B. Mishra (2016): Histological Image Processing Features Induce a Quantitative Characterization of Chronic Tumor Hypoxia. PLoS ONE 11(4), pp. 1-30, doi:10.1371/journal.pone.0153623.
[42] B. M. Tijms, P. Series, D. J. Willshaw & S. M. Lawrie (2011): Similarity-Based Extraction of Individual Networks from Gray Matter MRI Scans. Cerebral Cortex 22(7), pp. 1530-1541, doi:10.1093/cercor/bhr221.
[43] A. T. Toosy (2003): Diffusion tensor imaging detects corticospinal tract involvement at multiple levels in amyotrophic lateral sclerosis. J. Neurol. Neurosurg. Psychiatry 74(9), pp. 1250-1257, doi:10.1136/jnnp.74.9.1250.
[44] B.J. Woods, B. D. Clymer, T. Kurc, J. T. Heverhagen, R. Stevens, Orsdemir A., O. Bulan & M. V. Knopp (2007): Malignant-lesion segmentation using 4D co-occurrence texture analysis applied to dynamic contrast-enhanced magnetic resonance breast image data. J. Magn. Reson. Imaging 25(3), pp. 495-501, doi:10.1002/jmri.20837.

Metrics



Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:357986,
	title = {From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging},
	author = {Belmonte G. and Ciancia V. and Latella D. and Massink M.},
	doi = {10.4204/eptcs.217.10 and 10.48550/arxiv.1607.02235},
	booktitle = {FORECAST 2016 - Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, pp. 81–92, Vienna, Austria, 8 July 2016},
	year = {2016}
}

QUANTICOL
A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours


OpenAIRE