Finite Approximation of LMPs for Exact Verification of Reachability Properties.

We give a discretization technique that allows one to check reachability properties in a family of continuous-state processes. We consider a sub-family of labelled Markov processes (LMP), whose transitions can be defined by uniform distributions, and simple reachability formulas. The key of the discretization is the use of the mean-value theorem to construct, for a family of LMPs and reachability properties, a (finite) Markov decision process (MDP) equivalent to the initial (potentially infinite) LMP with respect to the formula. On the MDP obtained, we can apply known algorithms and tools for probabilistic systems with finite or countable state space. The MDP is constructed in such a way that the LMP satisfies the reachability property if and only if the MDP also satisfies it. Theoretically, our approach gives a precise final result. In practice, this is not the case, of course, but we bound the error on the formula with respect to the errors that can be introduced in the computation of the MDP. We also establish a bisimulation relation between the latter and the theoretical MDP.