Recently, many systems that consist of a large number of interacting objects have been analysed using the mean-field method, which allows a quick and accurate analysis of such systems, while avoiding the state-space explosion problem. To date, the mean-field method has primarily been used for classical performance evaluation purposes. In this chapter, we discuss model-checking mean-field models. We define and motivate two logics, called Mean-Field Continuous Stochastic Logic (MF-CSL) and Mean-Field Logic (MFL), to describe properties of systems composed of many identical interacting objects. We present model-checking algorithms and discuss the differences in the expressiveness of these two logics and their combinations.
|Title of host publication||Principles of Performance and Reliability Modeling and Evaluation - Essays in Honor of Kishor Trivedi on his 70th Birthday|
|Editors||Lance Fiondella, Antonio Puliafito|
|Place of Publication||London|
|Number of pages||29|
|Publication status||Published - Apr 2016|
|Name||Springer series in reliability engineering|
Kolesnichenko, A. V., Remke, A. K. I., de Boer, P-T., & Haverkort, B. R. H. M. (2016). Model checking two layers of mean-field models. In L. Fiondella, & A. Puliafito (Eds.), Principles of Performance and Reliability Modeling and Evaluation - Essays in Honor of Kishor Trivedi on his 70th Birthday (pp. 341-369). (Springer series in reliability engineering). Springer Verlag. https://doi.org/10.1007/978-3-319-30599-8_13