On-the-fly fluid model checking via discrete time population models - Extended version. (Rapporti tecnici/preprint/working paper)

Type
Label
  • On-the-fly fluid model checking via discrete time population models - Extended version. (Rapporti tecnici/preprint/working paper) (literal)
Anno
  • 2014-01-01T00:00:00+01:00 (literal)
Alternative label
  • Latella D., Loreti M., Massink M. (2014)
    On-the-fly fluid model checking via discrete time population models - Extended version.
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Latella D., Loreti M., Massink M. (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni
  • Grant agreement: 600708 Tipo Progetto: EU_FP7 (literal)
Note
  • PuMa (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#supporto
  • Altro (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • CNR-ISTI, Pisa, Italy; Università di Firenze e IMT-Lucca, Italy; CNR-ISTI, Pisa, Italy (literal)
Titolo
  • On-the-fly fluid model checking via discrete time population models - Extended version. (literal)
Abstract
  • 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. (literal)
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:


Autore CNR di
Prodotto
Insieme di parole chiave di
data.CNR.it