Central Limit Approximation for Stochastic Model Checking
- Day - Time: 28 May 2013, h.11:00
- Place: Area della Ricerca CNR di Pisa - Room: C-40
Speakers
- Roberta Lanziani (IMT Lucca)
Referent
Abstract
In this talk 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.