A logic for model-checking mean-field models

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

doi:10.1109/DSN.2013.6575345

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)

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 language	English
Publisher	Institute of Electrical and Electronics Engineers ( IEEE )
Number of pages	12
Place of Publication	USA
ISBN (Print)	978-1-4673-6471-3
DOIs	https://doi.org/10.1109/DSN.2013.6575345
Publication status	Published - Jun 2013
Externally published	Yes

Keywords

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

Access to Document

10.1109/DSN.2013.6575345

Cite this

@misc{fec9a172bc5b4be6821d942d66470d3f,

title = "A logic for model-checking mean-field models",

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.",

keywords = "METIS-299978, IR-88353, Model Checking, Mean Field, mean field continuous stochastic logic, EWI-23500, model checkingmean fieldmean field continuous stochastic logic",

author = "A.V. Kolesnichenko and {de Boer}, Pieter-Tjerk and Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.}",

note = "eemcs-eprint-23500",

year = "2013",

month = jun,

doi = "10.1109/DSN.2013.6575345",

language = "English",

isbn = "978-1-4673-6471-3",

publisher = "Institute of Electrical and Electronics Engineers ( IEEE )",

type = "Other",

}

TY - GEN

T1 - A logic for model-checking mean-field models

AU - Kolesnichenko, A.V.

AU - de Boer, Pieter-Tjerk

AU - Remke, Anne Katharina Ingrid

AU - Haverkort, Boudewijn R.H.M.

N1 - eemcs-eprint-23500

PY - 2013/6

Y1 - 2013/6

N2 - 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.

AB - 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.

KW - METIS-299978

KW - IR-88353

KW - Model Checking

KW - Mean Field

KW - mean field continuous stochastic logic

KW - EWI-23500

KW - model checkingmean fieldmean field continuous stochastic logic

U2 - 10.1109/DSN.2013.6575345

DO - 10.1109/DSN.2013.6575345

M3 - Other contribution

SN - 978-1-4673-6471-3

PB - Institute of Electrical and Electronics Engineers ( IEEE )

CY - USA

ER -

A logic for model-checking mean-field models

Abstract

Keywords

Access to Document

Fingerprint

Cite this