Floris Zeven: Spatial Model Checking with mCRL2

Event Details

Image analysis using spatial model checking is a relatively recent approach that has promising applications in the medical field. We investigated whether it is possible to verify spatial proper- ties using the mCRL2 toolset, which was built to verify concurrent systems and protocols. This was achieved by translating Spatial Logic for Closure Spaces (SLCS) formulae to μ-calculus formulae, proving this translation is correct, and by creating a script that associates an mCRL2 specification with an image. As mCRL2 only verifies properties on an initial state, which would correspond to a single pixel, a proof-of-concept implementation was subsequently created that utilizes the mCRL2 toolset to mark every pixel that satisfies a spatial property.