Refinement and Difference for Probabilistic Automata - LINA-AELOS Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Refinement and Difference for Probabilistic Automata

Benoît Delahaye

Résumé

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.
Fichier principal
Vignette du fichier
qest.pdf (373.86 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01087931 , version 1 (27-11-2014)

Identifiants

Citer

Benoît Delahaye, Uli Fahrenberg, Kim Guldstrand Larsen, Axel Legay. Refinement and Difference for Probabilistic Automata. QEST 2013 - 10th International Conference Quantitative Evaluation of Systems, Aug 2013, Buenos Aires, Argentina. pp.22 - 38, ⟨10.1007/978-3-642-40196-1_3⟩. ⟨hal-01087931⟩
394 Consultations
85 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More