A logic for model-checking mean-field models

A.V. Kolesnichenko, Pieter-Tjerk de Boer, Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort

Research output: Other contribution

9 Citations (Scopus)


Recently the mean-field method has been adopted for analysing systems consisting of a large number of interacting objects in computer science, biology, chemistry, etc. It allows for a quick and accurate analysis of such systems, while avoiding the state-space explosion problem. So far, the method has primarily been used for performance evaluation. In this paper, we use the mean-field method for model-checking. We define and motivate a logic MF-CSL for describing properties of systems composed of many identical interacting objects. The proposed logic allows describing both properties of the overall system and of a random individual object. Algorithms to check the satisfaction relation for all MF-CSL operators are proposed. Furthermore, we explain how the set of all time instances that fulfill a given MF-CSL formula for a certain distribution of objects can be computed.
Original languageEnglish
PublisherInstitute of Electrical and Electronics Engineers ( IEEE )
Number of pages12
Place of PublicationUSA
ISBN (Print)978-1-4673-6471-3
Publication statusPublished - Jun 2013
Externally publishedYes


  • METIS-299978
  • IR-88353
  • Model Checking
  • Mean Field
  • mean field continuous stochastic logic
  • EWI-23500
  • model checkingmean fieldmean field continuous stochastic logic


Dive into the research topics of 'A logic for model-checking mean-field models'. Together they form a unique fingerprint.

Cite this