Incremental Quantitative Verification for Markov Decision Processes - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Incremental Quantitative Verification for Markov Decision Processes

Marta Kwiatkowska
  • Fonction : Auteur
  • PersonId : 861066
Hongyang Qu
  • Fonction : Auteur

Résumé

Quantitative verification techniques provide an effective means of computing performance and reliability properties for a wide range of systems. However, the com- putation required can be expensive, particularly if it has to be performed multiple times, for example to determine optimal system parameters. We present efficient incremental techniques for quantitative verification of Markov decision processes, which are able to re-use results from previous verification runs, based on a decomposition of the model into its strongly connected components (SCCs). We also show how this SCC-based approach can be further optimised to improve verification speed and how it can be combined with symbolic data structures to offer better scalability. We illustrate the effectiveness of the approach on a selection of large case studies.

Domaines

Informatique
Fichier principal
Vignette du fichier
pds11.pdf (334.7 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00647057 , version 1 (30-01-2012)

Identifiants

  • HAL Id : hal-00647057 , version 1

Citer

Marta Kwiatkowska, David Parker, Hongyang Qu. Incremental Quantitative Verification for Markov Decision Processes. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-PDS'11), 2011, Hong Kong, China. pp.359--370. ⟨hal-00647057⟩

Collections

CONNECT
69 Consultations
294 Téléchargements

Partager

Gmail Facebook X LinkedIn More