Quantitative Multi-Objective Verification for Probabilistic Systems

Abstract : We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for ex- ample, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or re- ward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.
Type de document :
Communication dans un congrès
P. Abdulla and K. Leino. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), 2011, Saarbrücken, Germany. Springer, 6605, pp.112--127, 2011, LNCS
Liste complète des métadonnées

https://hal.inria.fr/hal-00647055
Contributeur : Hongyang Qu <>
Soumis le : jeudi 1 décembre 2011 - 13:41:33
Dernière modification le : mardi 6 décembre 2011 - 10:36:13
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:58:17

Fichier

tacas11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00647055, version 1

Collections

Citation

Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu. Quantitative Multi-Objective Verification for Probabilistic Systems. P. Abdulla and K. Leino. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), 2011, Saarbrücken, Germany. Springer, 6605, pp.112--127, 2011, LNCS. 〈hal-00647055〉

Partager

Métriques

Consultations de la notice

120

Téléchargements de fichiers

68