PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Massink M., Bortolussi L., Ciancia V., Hillston J., Lluch-Lafuente A., Latella D., Loreti M., Reijsbergen D., Vandin A. QUANTICOL - Foundations of scalable verification for stochastic logics. A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL). Deliverable D3.1, 2014.
 
 
Abstract
(English)
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 veri cation 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 satis es 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.
Subject Mean-Field
Stochastic Processes
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs
03B70 Logic in computer science


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional