Tutorial Speaker Mieke Massink
Mieke Massink (PhD 1996, University of Nijmegen, The Netherlands) is a Senior Researcher in Computer Science at the Formal Methods and Tools lab at CNR-ISTI (Institute of Information Science and Technology “A. Faedo”), a computer science research institute of the National Research Council of Italy (CNR). Prior to this appointment, she held several research positions at the University of Nijmegen, The University of Twente, both in the Netherlands, and, in the context of several European projects, at the CNR-CNUCE and CNR-ISTI institutes, Italy, and the University of York, United Kingdom. Her research areas include the development and application of formal methods for the specification and verification of concurrent, safety-critical systems, including those exhibiting stochastic and large-scale emergent behaviour. In the last decade she increasingly focused on the theory and development of logic-based spatial model checking with applications to medical image analysis. She is a coordinator of the Computers and Society Working Group of GI-STS (Interdisciplinary Group on Science, Technology and Society of Area della Ricerca CNR in Pisa) and a member of USPID (Union of Scientists for Disarmament).
Talk
Model Checking in Space with Applications to Medical Image Analysis
Time: TBA
Room: TBA
Model checking has traditionally focused on temporal aspects of system behaviour. However, when analysing more complex, distributed, systems, such as large-scale collective adaptive systems, it quickly becomes clear that spatial aspects of such systems are as much relevant as their temporal aspects. Just think about agents that can only locally interact with each other, while affecting the global system behaviour, such as in gossip protocols used for data diffusion. This observation triggered the development of novel spatial and spatio-temporal model checking techniques and related model checkers, such as topochecker, VoxLogicA, and the polyhedral model checker PolyLogicA for the analysis of discrete space models and continuous space models, respectively. Spatial model checking has also found interesting applications in unexpected domains such as medical image analysis.
This tutorial will introduce you to spatial model checking with VoxLogicA and PolyLogicA, and their logic specification language ImgQL (Image Query Language), which is an extension of the Spatial Logic for Closure Spaces (SLCS). It will explain the directly relevant theoretical foundations of the spatial and polyhedra semantics of this logic that find their origin in closure spaces, a generalisation of topology. It will illustrate the use of spatial model checking, including examples in the medical domain, and provide ideas for a hybrid approach combining it with subsymbolic approaches such as deep learning.