"Duality, approximations and distances for probabilistic processes"

点击翻译按钮获取中文摘要

The general goal of the research project is to establish formal methods for reasoning about concurrent probabilistic processes. In particular, I am interested in processes that have a continuous state-space, but are observed in discrete time steps: a well-known model for these systems are Labelled Markov Processes (LMPs). Possible application areas include communication protocols and process control software. For such systems we would like to reason about correctness, performance and safety critical properties. I want to develop the field along theoretic and practical sides. I work with LMPs, but also with infLMPs, which are a generalisation of LMPs where the usual requirement for measures to be additive is dropped. This model subsumes the usual ones: probabilistic transition systems, LMPs, probabilistic automata. It allows to model underspecified systems, for example systems for which we only have incomplete specification.