A Formal and Run-Time Framework for the Adaptation of Local Behaviours to Match a Global Property

We address the problem of automatically identifying what local properties the agents of a Cyber Physical System have to satisfy to guarantee a global required property phi. To enrich the picture, we consider properties where, besides qualitative requirements on the actions to be performed, we assume a weight associated with them: quantitative properties are specified through a weighted modal-logic. We propose both a formal machinery based on a Quantitative Partial Model Checking function on contexts, and a run-time machinery that algorithmically tries to check if the local behaviours proposed by the agents satisfy phi. The proposed approach can be seen as a run-time decomposition, privacy sensitive in the sense agents do not have to disclose their full behaviour.