  This paper considers the problem of decentralized monitoring of a class of
non-functional properties (NFPs) with quantitative operators, namely cumulative
cost properties. The decentralized monitoring of NFPs can be a non-trivial task
for several reasons: (i) they are typically expressed at a high abstraction
level where inter-event dependencies are hidden, (ii) NFPs are difficult to be
monitored in a decentralized way, and (iii) lack of effective decomposition
techniques. We address these issues by providing a formal framework for
decentralised monitoring of LTL formulas with quantitative operators. The
presented framework employs the tableau construction and a formula unwinding
technique (i.e., a transformation technique that preserves the semantics of the
original formula) to split and distribute the input LTL formula and the
corresponding quantitative constraint in a way such that monitoring can be
performed in a decentralised manner. The employment of these techniques allows
processes to detect early violations of monitored properties and perform some
corrective or recovery actions. We demonstrate the effectiveness of the
presented framework using a case study based on a Fischertechnik training
model,a sorting line which sorts tokens based on their color into storage bins.
The analysis of the case study shows the effectiveness of the presented
framework not only in early detection of violations, but also in developing
failure recovery plans that can help to avoid serious impact of failures on the
performance of the system.
