23 March 2012
Recently, many systems consisting of a large number of interacting objects were analysed using the mean-field method, which allows a quick and accurate analysis of such systems, while avoiding the state-space explosion problem. So far, the mean-field method has only been used for performance evaluation. Here we use it for model checking. We define and motivate two logics for describing properties of systems composed of many identical interacting objects. These properties are expressed using (i) global atomic properties, defined in terms of the fraction of objects that have a certain local atomic property; and (ii) the until operator, which allows to describe the evolution of the system over time, in mean – field logic (MFL). In mean-field continuous stochastic logic (MF-CSL), however, the logical formulas are expressed in terms of expectations of CSL-like properties. Furthermore, we compare the expressivity of the proposed logics and present examples.