On-the-fly probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014 (Rapporti tecnici/preprint/working paper)

Type

• Prodotto della ricerca (Classe)
• Rapporti tecnici/preprint/working paper (Classe)

Label

• On-the-fly probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014 (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 probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014
  
  (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

• Tipo Progetto EU_FP7 A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours Acronimo QUANTICOL Grant agreement 600708 QUANTICOL Technical Report TR-QC-09-2014. Technical report, 2014 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url

• http://milner.inf.ed.ac.uk/wiki/files/z4f158B0/QCOL_TR_09_OTF_PMC_2014_12_08pdf.html (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 probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014 (literal)

Abstract

• Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula Φ, and local approaches in which, given a state s in M, the procedure determines whether s satisfies Φ. When s is a term of a process language, the model-checking procedure can be executed \"on-the-fly\", driven by the syntactical structure of s. For certain classes of systems, e.g. those composed of many parallel components, the local approach is preferable because, depending on the specific property, it may be sufficient to generate and inspect only a relatively small part of the state space. We propose an efficient, on-the-fly, PCTL model checking procedure that is parametric with respect to the semantic interpretation of the language. The procedure comprises both bounded and unbounded until modalities. The correctness of the procedure is shown and its efficiency is explored on a number of benchmark applications in comparison with the global PCTL model checker PRISM. (literal)

Prodotto di

• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)
• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)

Autore CNR

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Insieme di parole chiave

• Parole chiave di "On-the-fly probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014" (Insieme di parole chiave)

Incoming links:

Autore CNR di

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Insieme di parole chiave di

• Parole chiave di "On-the-fly probabilistic model checking. Extended version. QUANTICOL Technical Report nr. TR-QC-09-2014" (Insieme di parole chiave)