Topochecker is a spatio-temporal model checker based on closure spaces and Kripke frames. Currently it checks a spatial extension of CTL named STLCS (spatio-temporal logic of closure spaces).
The current version of topochecker, given its prototypical nature, is available in source code form at github, where you can find more information, download the tool and experiment with it.
Github:
https://github.com/vincenzoml/topochecker
Contact:
vincenzoml@gmail.com