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 kolesnichenko | 1 | 19 | 1.69 |
de Boer, P.-T. | 2 | 17 | 1.34 |
Anne Remke | 3 | 175 | 23.96 |
Boudewijn R. Haverkort | 4 | 84 | 5.08 |