QUANTICOL - Foundations of scalable verification for stochastic logics

Massink M., Bortolussi L., Ciancia V., Hillston J., Lluch-Lafuente A., Latella D., Loreti M., Reijsbergen D., Vandin A.

Mean-Field  Stochastic Processes  F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs 

This deliverable reports on the study of the theoretical foundations of scalable model checking approaches, including those based on mean-eld and uid ow techniques, addressing the rst phase of Task 3.1. Model checking has been widely recognised as a powerful approach to the automatic verication of concurrent and distributed systems. It consists of an ecient procedure that, given an abstract model of the behaviour of the system, decides whether that model satises properties of interest, typically expressed using a form of temporal logic. Despite their success, scalability of model checking procedures has always been a concern due to the potential combinatorial explosion of the state space that needs to be searched. This is particularly an issue when analysing large collective adaptive systems that typically consist of a large number of independent, communicating objects. This deliverable reports on the theoretical foundations of several novel scalable model checking approaches that have been developed during the rst year of the QUANTICOL project to address the challenge of scalability. A rst approach concerns Fluid Model Checking. This approach exploits uid ow approximations and fast simulation techniques in a global model checking algorithm to verify continuous stochastic logic properties of an individual object, or a few objects, in the context of large population models. The approach has been extended considering steady state properties and a method has been developed to lift local properties to global collective ones exploiting the central limit theorem. The second approach concerns mean-eld fast probabilistic model checking. This approach exploits mean-eld approximation and fast simulation in a discrete time probabilistic setting. Furthermore, it combines the above mentioned techniques with on-the- y model checking techniques. The asymptotic correctness of the approach is outlined and the use of the prototype implementation of the algorithm, developed during the rst year of the QUANTICOL Project, is brie y illustrated on a variant of the bike-sharing case study. A third approach concerns a novel and ecient statistical model checking technique and tool to deal with uncertainty in the values of model parameters in a statistically sound way. The approach is based also on recent advances in machine learning and pattern recognition. Finally, we report on a literature study that was conducted on spatial logics and that is complementing the work on spatial representations in Work Package 2, in preparation for the future extension of the scalable model checking techniques addressing properties of spatially inhomogeneous collective adaptive systems.

Source: Project report, QUANTICOL, Deliverable D1.0, 2014