A logic for model-checking mean-field models

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

doi:10.1109/DSN.2013.6575345

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 proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013)
Place of Publication	Piscataway, NJ
Publisher	IEEE
Pages	1-12
Number of pages	12
ISBN (Electronic)	978-1-4673-6472-0
ISBN (Print)	978-1-4673-6471-3
DOIs	https://doi.org/10.1109/DSN.2013.6575345
Publication status	Published - Jun 2013

Publication series

Name	International Conference on Dependable Systems and Networks
Publisher	IEEE
Volume	43
ISSN (Print)	1530-0889
ISSN (Electronic)	2158-3927

Keywords

Model checking
Mean field
Continuous stochastic logic

Access to Document

10.1109/DSN.2013.6575345

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

@inproceedings{e793ebfd595044bcbd6efc9fbabf7121,

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 = "Model checking, Mean field, Continuous stochastic logic",

author = "Anna Kolesnichenko and {de Boer}, Pieter-Tjerk and Anne Remke and Haverkort, {Boudewijn R.}",

year = "2013",

month = "6",

doi = "10.1109/DSN.2013.6575345",

language = "English",

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

series = "International Conference on Dependable Systems and Networks",

publisher = "IEEE",

pages = "1--12",

booktitle = "43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013)",

address = "United States",

}

A logic for model-checking mean-field models. / Kolesnichenko, Anna; de Boer, Pieter-Tjerk; Remke, Anne; Haverkort, Boudewijn R.

43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013). Piscataway, NJ : IEEE, 2013. p. 1-12 (International Conference on Dependable Systems and Networks; Vol. 43).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Kolesnichenko, Anna

AU - de Boer, Pieter-Tjerk

AU - Remke, Anne

AU - Haverkort, Boudewijn R.

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 - Model checking

KW - Mean field

KW - Continuous stochastic logic

U2 - 10.1109/DSN.2013.6575345

DO - 10.1109/DSN.2013.6575345

M3 - Conference contribution

SN - 978-1-4673-6471-3

T3 - International Conference on Dependable Systems and Networks

SP - 1

EP - 12

BT - 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013)

PB - IEEE

CY - Piscataway, NJ

ER -