A unified view of spatial representation and analysis techniques

Galpin V., Bortolussi L., Ciancia V., Feng C., Gast N., Hillston J., Massink M., Latella D., Tribastone M., Tschaikowski M.

Space modelling  Specifying and verifying and reasoning about programs 

This report presents an overview of spatial representations and analysis techniques within the context of the QUANTICOL project. It first recaps the spatial classification of mathematical models from Deliverable 2.1 and compares this with an abstract data type approach to space proposed for the Carma language in the technical report TR-QC-01-2015. Based on the guidelines presented in Deliverable 2.1, together with recent research within the project, the report focuses on two types of discrete-space models: population discrete-space models and individual discrete-space models, both of which involve a graph over locations. In both types, we restrict our focus to time-homogeneous systems where graph structure is static. When considering analysis techniques, transformations between mathematical models are important as these permit the application of different analysis techniques. The relevant transformations within the QUANTICOL project are aggregation, disaggregation, fluidisation, discretisation and hybridisation. These mostly support abstraction but some can also lead to more detailed models. The report considers analysis techniques that apply specifically to population discrete-space models, and those that apply specifically to individual discrete-space models. A technique for transforming individual (1-dimensional) continuous-space models to population discrete-space models is presented. Some analyses are applicable to both types of model including spatial model checking, modelling of crowding and analyses that combine techniques and work with hybrid models. The report concludes by considering whether space is a special attribute, the relevance of the various analysis techniques for QUANTICOL and Carma, and proposing research topics for the remainder of Task 2.1. These include application of existing results in the context of the QUANTICOL case studies, a location aggregation technique, further investigation of techniques already considered in the project and the possibility of developing hybrid techniques that abstract from parts of the model but consider other parts in a detailed fashion.

Source: ISTI Technical reports, 2015