Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Proofs and Refutations for Probabilistic Refinement
verfasst von : A. K. McIver, C. C. Morgan, C. Gonzalia
Erschienen in: FM 2008: Formal Methods
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
We consider the issue of finding and presenting counterexamples to a claim “this
spec
is implemented by that
imp
”, that is
$\textit{spec} \sqsubseteq \textit{imp}$
(refinement), in the context of
probabilistic
systems: using a geometric interpretation of the probabilistic/demonic semantic domain we are able to encode both refinement success and refinement failure as linear satisfaction problems, which can then be analysed automatically by an SMT solver. This allows the automatic discovery of certificates for counterexamples in independently and efficiently checkable form. In many cases the counterexamples can subsequently be converted into “source level” hints for the verifier.