Scalable verification for spatial stochastic logics

Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., Paskauskas R., Tribastone M., Tschaikowski M.

Spatial logics  Stochastic logics  Specifying and verifying and reasoning about programs 

This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOL

Source: ISTI Technical reports, 2016