Model-Checking Mean-Field Models: Algorithms & Applications

A.V. Kolesnichenko

Research output: ThesisPhD Thesis - Research UT, graduation UT

Abstract

Large systems of interacting objects are highly prevalent in today's world. Such system usually consist of a large number of relatively simple identical objects, and can be observed in many different field as, e.g., physics (interactions of molecules in gas), chemistry (chemical reactions), epidemiology (spread of the infection), etc. In this thesis we primarily address large systems of interacting objects in computer science, namely, computer networks. Analysis of such large systems is made difficult by the state space explosion problem, i.e., the number of states of the model grows exponentially with the number of interacting objects. In this thesis we tackle the state-space explosion problem by applying mean-field approximation, which was originally developed for models in physics, like the interaction of molecules in a gas. The mean-field method works by not considering the state of each individual object separately, but only their average, i.e., what fraction of the objects are in each possible state at any time. It allows to compute the exact limiting behaviour of an infinite population of identical objects, and this limiting behaviour is a good approximation, even when the number of objects is not infinite but sufficiently large. In this thesis we provide the theoretical background necessary for applying the mean-field method and illustrate the approach by a peer-to-peer Botnet case study. This thesis aims at formulating and analysing advanced properties of large systems of interacting objects using fast, efficient, and accurate algorithms. We propose to apply model-checking techniques to mean-field models. This allows (i) defining advanced properties of mean-field models, such as survivability, steady-state availability, conditional instantaneous availability using logic; and (ii) automatically checking these properties using model-checking algorithms. Existing model-checking logics and algorithms can not directly be applied to mean-field models since the model consist of two layers: the local level, describing the behaviour of a randomly chosen individual object in a large system, and the global level, which addresses the overall system of all interacting objects. Therefore, we motivate and define two logics, called Mean Field Continuous Stochastic Logic (MF-CSL), and Mean-Field Logic (MFL), for describing properties of systems composed of many identical interacting objects, on both the local and the global level. We present model-checking algorithms for checking both MF-CSL and MFL properties, and illustrated these algorithms using an extensive example on virus propagation in a computer network. We discuss the differences in the expressiveness of these two logics as well as their possible combination. Additionally, we combine the mean-field method with parameter fitting techniques in order to model real-world large systems, and obtain a better understanding of the behaviour of such systems. We explain how to build a mean-field model of the system, and how to estimate the corresponding parameter values, so as to find the best fit between the available data and the model prediction. We also discuss a number of intricate technical issues, ranging from the additional (preprocessing) work to be done on the measurement data, the interpretation of the data to, for instance, a restructuring of the model (based on data unavailability), that has to be performed before applying the parameter estimation procedures. To illustrate the approach we estimate the parameter values for the outbreak of the real-world computer worm Code-Red. The techniques presented in this thesis allow an involved analysis of large systems of interacting objects, including (i) obtaining parameter values of mean-field model using measurements; (ii) defining advanced properties of the model; and (iii) automatically checking such properties.
LanguageUndefined
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Haverkort, Boudewijn R.H.M., Supervisor
  • Remke, Anne Katharina Ingrid, Supervisor
  • de Boer, Pieter-Tjerk , Advisor
Award date17 Dec 2014
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-3821-3
DOIs
StatePublished - 17 Dec 2014

Keywords

  • IR-93238
  • mean-field approximationmodel-checkingMean Field LogicMean Field Continuous Stochastic Logicparameter estimation
  • METIS-307189
  • EWI-25594

Cite this

Kolesnichenko, A. V. (2014). Model-Checking Mean-Field Models: Algorithms & Applications Enschede: Centre for Telematics and Information Technology (CTIT) DOI: 10.3990/1.9789036538213
Kolesnichenko, A.V.. / Model-Checking Mean-Field Models: Algorithms & Applications. Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 194 p.
@phdthesis{2c699c8dff504432b9271d4a5bfa084d,
title = "Model-Checking Mean-Field Models: Algorithms & Applications",
abstract = "Large systems of interacting objects are highly prevalent in today's world. Such system usually consist of a large number of relatively simple identical objects, and can be observed in many different field as, e.g., physics (interactions of molecules in gas), chemistry (chemical reactions), epidemiology (spread of the infection), etc. In this thesis we primarily address large systems of interacting objects in computer science, namely, computer networks. Analysis of such large systems is made difficult by the state space explosion problem, i.e., the number of states of the model grows exponentially with the number of interacting objects. In this thesis we tackle the state-space explosion problem by applying mean-field approximation, which was originally developed for models in physics, like the interaction of molecules in a gas. The mean-field method works by not considering the state of each individual object separately, but only their average, i.e., what fraction of the objects are in each possible state at any time. It allows to compute the exact limiting behaviour of an infinite population of identical objects, and this limiting behaviour is a good approximation, even when the number of objects is not infinite but sufficiently large. In this thesis we provide the theoretical background necessary for applying the mean-field method and illustrate the approach by a peer-to-peer Botnet case study. This thesis aims at formulating and analysing advanced properties of large systems of interacting objects using fast, efficient, and accurate algorithms. We propose to apply model-checking techniques to mean-field models. This allows (i) defining advanced properties of mean-field models, such as survivability, steady-state availability, conditional instantaneous availability using logic; and (ii) automatically checking these properties using model-checking algorithms. Existing model-checking logics and algorithms can not directly be applied to mean-field models since the model consist of two layers: the local level, describing the behaviour of a randomly chosen individual object in a large system, and the global level, which addresses the overall system of all interacting objects. Therefore, we motivate and define two logics, called Mean Field Continuous Stochastic Logic (MF-CSL), and Mean-Field Logic (MFL), for describing properties of systems composed of many identical interacting objects, on both the local and the global level. We present model-checking algorithms for checking both MF-CSL and MFL properties, and illustrated these algorithms using an extensive example on virus propagation in a computer network. We discuss the differences in the expressiveness of these two logics as well as their possible combination. Additionally, we combine the mean-field method with parameter fitting techniques in order to model real-world large systems, and obtain a better understanding of the behaviour of such systems. We explain how to build a mean-field model of the system, and how to estimate the corresponding parameter values, so as to find the best fit between the available data and the model prediction. We also discuss a number of intricate technical issues, ranging from the additional (preprocessing) work to be done on the measurement data, the interpretation of the data to, for instance, a restructuring of the model (based on data unavailability), that has to be performed before applying the parameter estimation procedures. To illustrate the approach we estimate the parameter values for the outbreak of the real-world computer worm Code-Red. The techniques presented in this thesis allow an involved analysis of large systems of interacting objects, including (i) obtaining parameter values of mean-field model using measurements; (ii) defining advanced properties of the model; and (iii) automatically checking such properties.",
keywords = "IR-93238, mean-field approximationmodel-checkingMean Field LogicMean Field Continuous Stochastic Logicparameter estimation, METIS-307189, EWI-25594",
author = "A.V. Kolesnichenko",
year = "2014",
month = "12",
day = "17",
doi = "10.3990/1.9789036538213",
language = "Undefined",
isbn = "978-90-365-3821-3",
publisher = "Centre for Telematics and Information Technology (CTIT)",
address = "Netherlands",
school = "University of Twente",

}

Kolesnichenko, AV 2014, 'Model-Checking Mean-Field Models: Algorithms & Applications', University of Twente, Enschede. DOI: 10.3990/1.9789036538213

Model-Checking Mean-Field Models: Algorithms & Applications. / Kolesnichenko, A.V.

Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 194 p.

Research output: ThesisPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Model-Checking Mean-Field Models: Algorithms & Applications

AU - Kolesnichenko,A.V.

PY - 2014/12/17

Y1 - 2014/12/17

N2 - Large systems of interacting objects are highly prevalent in today's world. Such system usually consist of a large number of relatively simple identical objects, and can be observed in many different field as, e.g., physics (interactions of molecules in gas), chemistry (chemical reactions), epidemiology (spread of the infection), etc. In this thesis we primarily address large systems of interacting objects in computer science, namely, computer networks. Analysis of such large systems is made difficult by the state space explosion problem, i.e., the number of states of the model grows exponentially with the number of interacting objects. In this thesis we tackle the state-space explosion problem by applying mean-field approximation, which was originally developed for models in physics, like the interaction of molecules in a gas. The mean-field method works by not considering the state of each individual object separately, but only their average, i.e., what fraction of the objects are in each possible state at any time. It allows to compute the exact limiting behaviour of an infinite population of identical objects, and this limiting behaviour is a good approximation, even when the number of objects is not infinite but sufficiently large. In this thesis we provide the theoretical background necessary for applying the mean-field method and illustrate the approach by a peer-to-peer Botnet case study. This thesis aims at formulating and analysing advanced properties of large systems of interacting objects using fast, efficient, and accurate algorithms. We propose to apply model-checking techniques to mean-field models. This allows (i) defining advanced properties of mean-field models, such as survivability, steady-state availability, conditional instantaneous availability using logic; and (ii) automatically checking these properties using model-checking algorithms. Existing model-checking logics and algorithms can not directly be applied to mean-field models since the model consist of two layers: the local level, describing the behaviour of a randomly chosen individual object in a large system, and the global level, which addresses the overall system of all interacting objects. Therefore, we motivate and define two logics, called Mean Field Continuous Stochastic Logic (MF-CSL), and Mean-Field Logic (MFL), for describing properties of systems composed of many identical interacting objects, on both the local and the global level. We present model-checking algorithms for checking both MF-CSL and MFL properties, and illustrated these algorithms using an extensive example on virus propagation in a computer network. We discuss the differences in the expressiveness of these two logics as well as their possible combination. Additionally, we combine the mean-field method with parameter fitting techniques in order to model real-world large systems, and obtain a better understanding of the behaviour of such systems. We explain how to build a mean-field model of the system, and how to estimate the corresponding parameter values, so as to find the best fit between the available data and the model prediction. We also discuss a number of intricate technical issues, ranging from the additional (preprocessing) work to be done on the measurement data, the interpretation of the data to, for instance, a restructuring of the model (based on data unavailability), that has to be performed before applying the parameter estimation procedures. To illustrate the approach we estimate the parameter values for the outbreak of the real-world computer worm Code-Red. The techniques presented in this thesis allow an involved analysis of large systems of interacting objects, including (i) obtaining parameter values of mean-field model using measurements; (ii) defining advanced properties of the model; and (iii) automatically checking such properties.

AB - Large systems of interacting objects are highly prevalent in today's world. Such system usually consist of a large number of relatively simple identical objects, and can be observed in many different field as, e.g., physics (interactions of molecules in gas), chemistry (chemical reactions), epidemiology (spread of the infection), etc. In this thesis we primarily address large systems of interacting objects in computer science, namely, computer networks. Analysis of such large systems is made difficult by the state space explosion problem, i.e., the number of states of the model grows exponentially with the number of interacting objects. In this thesis we tackle the state-space explosion problem by applying mean-field approximation, which was originally developed for models in physics, like the interaction of molecules in a gas. The mean-field method works by not considering the state of each individual object separately, but only their average, i.e., what fraction of the objects are in each possible state at any time. It allows to compute the exact limiting behaviour of an infinite population of identical objects, and this limiting behaviour is a good approximation, even when the number of objects is not infinite but sufficiently large. In this thesis we provide the theoretical background necessary for applying the mean-field method and illustrate the approach by a peer-to-peer Botnet case study. This thesis aims at formulating and analysing advanced properties of large systems of interacting objects using fast, efficient, and accurate algorithms. We propose to apply model-checking techniques to mean-field models. This allows (i) defining advanced properties of mean-field models, such as survivability, steady-state availability, conditional instantaneous availability using logic; and (ii) automatically checking these properties using model-checking algorithms. Existing model-checking logics and algorithms can not directly be applied to mean-field models since the model consist of two layers: the local level, describing the behaviour of a randomly chosen individual object in a large system, and the global level, which addresses the overall system of all interacting objects. Therefore, we motivate and define two logics, called Mean Field Continuous Stochastic Logic (MF-CSL), and Mean-Field Logic (MFL), for describing properties of systems composed of many identical interacting objects, on both the local and the global level. We present model-checking algorithms for checking both MF-CSL and MFL properties, and illustrated these algorithms using an extensive example on virus propagation in a computer network. We discuss the differences in the expressiveness of these two logics as well as their possible combination. Additionally, we combine the mean-field method with parameter fitting techniques in order to model real-world large systems, and obtain a better understanding of the behaviour of such systems. We explain how to build a mean-field model of the system, and how to estimate the corresponding parameter values, so as to find the best fit between the available data and the model prediction. We also discuss a number of intricate technical issues, ranging from the additional (preprocessing) work to be done on the measurement data, the interpretation of the data to, for instance, a restructuring of the model (based on data unavailability), that has to be performed before applying the parameter estimation procedures. To illustrate the approach we estimate the parameter values for the outbreak of the real-world computer worm Code-Red. The techniques presented in this thesis allow an involved analysis of large systems of interacting objects, including (i) obtaining parameter values of mean-field model using measurements; (ii) defining advanced properties of the model; and (iii) automatically checking such properties.

KW - IR-93238

KW - mean-field approximationmodel-checkingMean Field LogicMean Field Continuous Stochastic Logicparameter estimation

KW - METIS-307189

KW - EWI-25594

U2 - 10.3990/1.9789036538213

DO - 10.3990/1.9789036538213

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-3821-3

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Kolesnichenko AV. Model-Checking Mean-Field Models: Algorithms & Applications. Enschede: Centre for Telematics and Information Technology (CTIT), 2014. 194 p. Available from, DOI: 10.3990/1.9789036538213