Labelled Markov Processes: Stronger and Faster Approximations

This paper reports on and discusses three notions of approximation for Labelled Markov Processes that have been developed last year. The three schemes are improvements over former constructions [11,9] in the sense that they define approximants that capture more properties than before and that converge faster to the approximated process. One scheme is constructive and the two others are driven by properties on which one wants to focus. All three constructions involve quotienting the state-space in some way and the last two are quotients with respect to sets of temporal properties expressed in a simple logic with a greatest fixed point operator. This gives the possibility of customizing approximants with respect to properties of interest and is thus an important step towards using automated techniques intended for finite state systems, e.g., model checking, for
continuous state systems. Another difference between the schemes is how they relate approximants with the approximated process. The requirement that approximants should be simulated by the approximated process has been abandoned in the last scheme.