Delahaye, Benoît and Fahrenberg, Uli and Larsen, Kim G. and Legay, Axel - Refinement and Difference for Probabilistic Automata

lmcs:942 - Logical Methods in Computer Science, August 26, 2014, Volume 10, Issue 3
Refinement and Difference for Probabilistic Automata

Authors: Delahaye, Benoît and Fahrenberg, Uli and Larsen, Kim G. and Legay, Axel

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.


Source : oai:arXiv.org:1212.4288
DOI : 10.2168/LMCS-10(3:11)2014
Volume: Volume 10, Issue 3
Published on: August 26, 2014
Submitted on: November 12, 2013
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 67 times.
This article's PDF has been downloaded 21 times.