Istituto di Scienza e Tecnologie dell'Informazione     
Bortolussi L., Lanciani R. Model checking Markov population models by central Limit approximation. In: QEST 2013 - Quantitative Evaluation of Systems. 10th International Conference (Buenos Aires, Argentina, 27-30 August 2013). Proceedings, pp. 123 - 138. Kaustubh Joshi, Markus Siegle, MariŽlle Stoelinga, Pedro R. DíArgenio. (Lecture Notes in Computer Science, vol. 8054). Springer, 2013.
In this paper we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-40196-1_9
DOI: 10.1007/978-3-642-40196-1_9
Subject Markov Chains
Fluid Model Checking
Markov population models
B.8.2 Performance Analysis and Design Aids
F.3.1 Specifying and Verifying and Reasoning about Program
G.1.7 Ordinary Differential Equations
60Jxx Markov processes

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional