A logic for model-checking mean-field models

Anna Kolesnichenko, Pieter-Tjerk de Boer, Anne Remke, Boudewijn R. Haverkort

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    22 Downloads (Pure)

    Abstract

    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
    Title of host publication43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013)
    Place of PublicationPiscataway, NJ
    PublisherIEEE
    Pages1-12
    Number of pages12
    ISBN (Electronic)978-1-4673-6472-0
    ISBN (Print)978-1-4673-6471-3
    DOIs
    Publication statusPublished - Jun 2013

    Publication series

    NameInternational Conference on Dependable Systems and Networks
    PublisherIEEE
    Volume43
    ISSN (Print)1530-0889
    ISSN (Electronic)2158-3927

    Keywords

    • Model checking
    • Mean field
    • Continuous stochastic logic

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

  • Cite this

    Kolesnichenko, A., de Boer, P-T., Remke, A., & Haverkort, B. R. (2013). A logic for model-checking mean-field models. In 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013) (pp. 1-12). (International Conference on Dependable Systems and Networks; Vol. 43). Piscataway, NJ: IEEE. https://doi.org/10.1109/DSN.2013.6575345