Specifying and Verifying Properties of Space

spatialmodelcheckingmediumSpatial aspects of position, location and adjacency play a strong role in collective adaptive systems  in shaping the behaviour which can emerge from a system.

The QUANTICOL project has implemented a model checker that operates on space in the sense of a model described by topological means, or, more precisely, by closure spaces. Closure spaces encompass topological spaces and graph-like structures.

The work is supported by a model-checker tool, implemented using the functional language OCaml, which contains a generic implementation of a global model checker using closure spaces, parametrised by the type of models.  The model-checker is available from https://github.com/vincenzoml/slcs

An example of the tool usage is to approximately identify regions of interest on a digital picture (e.g., a map, or a medical image), using spatial formulae. In this case, digital pictures are treated as quasi-discrete models in the integer cartesian plane. The language of propositions is extended to formulae dealing with colour ranges, in order to cope with images where there are different shades of certain colours.

Applications of the model-checker include finding your way out of a maze, when given a picture of the maze. In another example, the model-checker was given a portion of the map of Pisa, featuring a red circle which denotes a train station. Streets of different importance are painted with different colours in the map. The model checker is used to identify the area surrounding the station which is delimited by main streets, and the delimiting main streets.

More information is available at https://blog.inf.ed.ac.uk/quanticol/technical-reports/

Authors: Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink