On the Numerical Verification of Probabilistic Rewriting Systems
J.B. Hassen, Sofiène Tahar · 2006
We present in this paper a technique for the formal verification of probabilistic systems described in PMaude, a probabilistic extension of the rewriting system Maude. Our methodology is based on a numerical verification using the probabilistic symbolic model checking tool PRISM. In particular, we show how we can construct an abstract system from the runs of a model that preserve all the probabilistic properties of the latter. Then we deduce the probabilistic matrix that will be used for the verification in PRISM