IIT Home Page CNR Home Page

A Quantitative Partial Model-Checking Function and Its Optimisation

Partial Model-Checking (PMC) is an effcient tool to reduce the combinatorial explosion of a state-space, arising in the verification of loosely-coupled software systems. At the same time, it is useful to consider quantitative temporal-modalities. This allows for checking whether satisfying such a desired modality is too costly, by comparing the final score consisting of how much the system spends to satisfy the policy, to a given threshold. We stir these two ingredients together in order to provide a Quantitative PMC function (QPMC), based on the algebraic structure of semirings. We design a method to extract part of the weight during QPMC, with the purpose to avoid the evaluation of a modality as soon as the threshold is crossed. Moreover, we extend classical heuristics to be quantitative, and we investigate the complexity of QPMC.
LPAR-21, Maun, Botswana, 2017

External authors: Stefano Bistarelli (Università di Perugia), Francesco Santini (Università di Perugia)
IIT authors:

Type: Contributo in atti di convegno
Field of reference: Computer Science & Engineering

File: main.pdf

Activity: Architetture, protocolli e meccanismi di sicurezza per sistemi e servizi distribuiti