Model checking two layers of mean-field models

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

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    Abstract

    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.
    Original languageUndefined
    Title of host publicationPrinciples of Performance and Reliability Modeling and Evaluation - Essays in Honor of Kishor Trivedi on his 70th Birthday
    EditorsLance Fiondella, Antonio Puliafito
    Place of PublicationLondon
    PublisherSpringer
    Pages341-369
    Number of pages29
    ISBN (Print)978-3-319-30597-4
    DOIs
    Publication statusPublished - Apr 2016

    Publication series

    NameSpringer series in reliability engineering
    PublisherSpringer Verlag
    ISSN (Print)1614-7839

    Keywords

    • IR-104415
    • EWI-27782

    Cite this