Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains

Serge Haddad 1 Nihal Pekergin
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We consider model checking of Discrete Time Markov Chains (DTMC) with transition probabilities which are not exactly known but lie in a given interval. Model checking a Probabilistic Computation Tree Logic (PCTL) formula for interval-valued DTMCs (IMC) has been shown to be NP hard and co-NP hard. Since the state space of a realistic DTMC is generally huge, these lower bounds prevent the application of exact algorithms for such models. Therefore we propose to apply the stochastic comparison method to check an extended version of PCTL for IMCs. More precisely, we first design linear time algorithms to quantitatively analyze IMCs. Then we develop an efficient, semi-decidable PCTL model checking procedure for IMCs. Furthermore, our procedure returns more refined answers than traditional ones: YES, NO, DON'T KNOW. Thus we may provide useful partial information for modelers in the "DON'T KNOW" case.
Type de document :
Communication dans un congrès
Proceedings of the 6th International Conference on Quantitative Evaluation of Systems (QEST'09), Sep 2009, Budapest, Hungary, Hungary. IEEE Computer Society Press, pp.177-186, 2009, 〈10.1109/QEST.2009.42〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772668
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 22:46:08
Dernière modification le : jeudi 11 janvier 2018 - 01:56:18

Identifiants

Collections

Citation

Serge Haddad, Nihal Pekergin. Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains. Proceedings of the 6th International Conference on Quantitative Evaluation of Systems (QEST'09), Sep 2009, Budapest, Hungary, Hungary. IEEE Computer Society Press, pp.177-186, 2009, 〈10.1109/QEST.2009.42〉. 〈hal-00772668〉

Partager

Métriques

Consultations de la notice

164