A Sound Up-to-n,δ Bisimilarity for PCTL
share
We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity similar to the one introduced by Desharnais, Laviolette, and Tracol, which is parametric with respect to an approximation error δ, and to the depth n of the observation along traces. Essentially, our soundness theorem establishes that, when a state q satisfies a given formula up-to error δ and steps n, and q is bisimilar to q' up-to error δ' and enough steps, we prove that q' also satisfies the formula up-to a suitable error δ" and steps n. The new error δ” is computed from δ, δ' and the formula, and only depends linearly on n. We provide a detailed overview of our soundness proof, which exploits the min-cut/max-flow theorem on graphs.
READ FULL TEXT