The Topological Approach to Spatial Model Checking with Applications to Imaging and 3D Meshes
Abstract
This presentation provides an outlook on the topological approach to spatial and spatio-temporal model checking. We introduce spatial logics, the SLCS language, and its semantics applied to various classes of models: Closure Spaces, Graphs, Polyhedra, and Posets. Additionally, we briefly discuss minimization techniques via the Hennessy-Milner property, and current implementation methods, highlighting relevant tools and applications. Special attention is given to how these techniques are used in practical domains such as imaging and 3D mesh analysis.
Please note that the meeting will be recorded and live-streamed to YouTube:
Vincenzo Ciancia
Researcher
I am a researcher at ISTI-CNR in Pisa, working in the Formal Methods & Tools Laboratory. Previously, I’ve been working at the IIT-CNR in Pisa, at the ILLC (University of Amsterdam), and at the Universidad Complutense in Madrid. I received my Ph.D. in 2009 from the Department of Computer Science at the University of Pisa, under the supervision of Prof. Ugo Montanari. My Ph.D. thesis and subsequent work was devoted to Coalgebras, Presheaf Categories, and History Dependent Automata. My research interests include Formal Methods in Computer Science, Spatial Logics and Spatio-Temporal Model Checking, Automata and Category Theory, Artificial Intelligence, with an accent on pairing solid mathematical theories with usable tools and implementation. Recently, my interests have been mostly focused on the VoxLogicA project, bringing formally specified expert knowledge to the realm of Medical Imaging via Model checking, in collaboration with colleagues at ISTI-CNR, San Luca Hospital in Lucca, University of Pisa, ILLC@University of Amsterdam, Razmadze Mathematical Institute - Tbilisi State University, TU Eindhoven. See http://www.voxlogica.org