Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Refinement and Difference for Probabilistic Automata
verfasst von : Benoît Delahaye, Uli Fahrenberg, Kim Guldstrand Larsen, Axel Legay
Erschienen in: Quantitative Evaluation of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.