Labelled Markov Processes: Stronger and Faster Approximations

Vincent Danos, Josée Desharnais, Prakash Panangaden

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)157 - 203
Number of pages47
JournalElectronic Notes in Theoretical Computer Science
Volume87
Issue number0
DOIs
Publication statusPublished - Nov 2004

Fingerprint Dive into the research topics of 'Labelled Markov Processes: Stronger and Faster Approximations'. Together they form a unique fingerprint.

Cite this