PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. On-the-fly fast mean-field model-checking - Extended version. Paper published in Arxiv 1312.3416 [cs.LO]. Technical report, 2013.
 
 
Abstract
(English)
A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is shown and some results of the application of a prototype implementation of the FlyFast model-checker are presented.
URL: http://arxiv.org/abs/1312.3416
Subject Deterministic approximation
Mean field approximation
Markov Chains
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.2 Modes of Computation
F.1.1 Models of Computation
F.3.1 Specifying and Verifying and Reasoning about Programs
G.3 PROBABILITY AND STATISTICS
39-XX Difference and functional 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