PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. On-the-fly fluid model checking via discrete time population models - Extended version. Codice TR: TR-QC-08-2014, Technical report, 2014.
 
 
Abstract
(English)
We show that, under suitable conditions, fluid model checking bounded CSL properties of selected individuals in a continuous PEPA population model can be approximated by checking equivalent bounded PCTL formulas on corresponding objects in a discrete time, time synchronous Markov population model, using an on-the-fly probabilistic approach. The proposed technique is applied to a benchmark client-server case study showing promising results also for the challenging case of nested formulas with time dependent truth values. The on-the-fly results are compared to those obtained with a global fluid model checking technique.
URL: http://milner.inf.ed.ac.uk/wiki/files/X0U160/QCOL_TR_08_OTF_FAST_MC_PEPA_2014_09_10pdf.html
Subject Deterministic approximation
Fluid model-checking
Mean Field model-checking
On-th-fly model-checking
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.2 Modes of Computation
G.1.7 Ordinary Differential Equations
G.3 PROBABILITY AND STATISTICS
34-XX ORDINARY DIFFERENTIAL EQUATIONS
39-XX Difference and functional equations


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