Refinement and Difference for Probabilistic Automata

Benoît Delahaye 1 Uli Fahrenberg 2 Kim Guldstrand Larsen 3 Axel Legay 2
1 AELOS
LINA - Laboratoire d'Informatique de Nantes Atlantique
2 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two deterministic APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex than refinement checking.
Type de document :
Communication dans un congrès
Kaustubh Joshi; Markus Siegle; Mariëlle Stoelinga; Pedro R. D’Argenio. QEST 2013 - 10th International Conference Quantitative Evaluation of Systems, Aug 2013, Buenos Aires, Argentina. Springer, pp.22 - 38, 2013, 〈10.1007/978-3-642-40196-1_3〉
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087931
Contributeur : Uli Fahrenberg <>
Soumis le : jeudi 27 novembre 2014 - 10:01:06
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:18:49

Fichier

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

Identifiants

Citation

Benoît Delahaye, Uli Fahrenberg, Kim Guldstrand Larsen, Axel Legay. Refinement and Difference for Probabilistic Automata. Kaustubh Joshi; Markus Siegle; Mariëlle Stoelinga; Pedro R. D’Argenio. QEST 2013 - 10th International Conference Quantitative Evaluation of Systems, Aug 2013, Buenos Aires, Argentina. Springer, pp.22 - 38, 2013, 〈10.1007/978-3-642-40196-1_3〉. 〈hal-01087931〉

Partager

Métriques

Consultations de la notice

496

Téléchargements de fichiers

57