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.
Year
DOI
Venue
2013
10.1109/DSN.2013.6575345
Dependable Systems and Networks
Keywords
DocType
ISSN
formal logic,formal verification,software performance evaluation,stochastic processes,MF-CSL logic,MF-CSL operators,biology,chemistry,computer science,mean field continuous stochastic logic,model checking mean-field model,performance evaluation,random individual object,satisfaction relation check
Conference
1530-0889
ISBN
Citations 
PageRank 
978-1-4673-6471-3
12
0.53
References 
Authors
15
4
Name
Order
Citations
PageRank
anna kolesnichenko1191.69
de Boer, P.-T.2171.34
Anne Remke317523.96
Boudewijn R. Haverkort4845.08