L11 (10.17) Formal verification of stochastic properties