Refinement and Difference for Probabilistic Automata

Delahaye, Benoit;Fahrenberg, Uli;Larsen Kim, Guldstrand;Legay, Axel
(2014) Logical Methods in Computer Science — p. LMCS-2013 (2014)

Files

No attached file found for this publication.

Details

Authors
  • Delahaye, Benoit
    Author
  • Fahrenberg, Uli
    Author
  • Larsen Kim, Guldstrand
    Author
  • Legay, AxelUCLouvain
    Author
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 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 to implement than refinement checking.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

Delahaye, B., Fahrenberg, U., Larsen Kim, G., & Legay, A. (2014). Refinement and Difference for Probabilistic Automata. Logical Methods in Computer Science, LMCS-2013. https://hdl.handle.net/2078.5/173042 (Original work published 2014)