Labelled Markov Processes: Stronger and Faster Approximations

This paper proposes a measure-theoretic reconstruc- tion of the approximation schemes developed for La- belled Markov Processes: approximants are seen as quo- tients with respect to sets of temporal properties ex- pressed in a simple logic. 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. The measure-theoretic apparatus meshes well with an enriched logic, extended with a greatest fix-point, and gives means to define approximants which retain cyclic properties of their target.