Formal methods for labelled Markov processes

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

The general goal of my research is to establish formal methods for reasoning about concurrent probabilistic processes.  In particular, I am interested in processes that have a continuous state-space, a model that we call Labelled Markov Processes (LMP).  Possible application  areas include communication protocols and process control software.  An example of the latter is a controller for a system like a vehicle. I want to continue develop interactions of the theory of LMPs with other fields, but my main goal is to develop the theory along two generalizations of LMPs.  In a recent past, we have defined pre-LMPs, a generalization of LMPs by weakening a property on their probabilistic structure;  this resulted in working with notions from capacity theory, a theory developed for economic mathematics.  This model is very promising for other goals, as it may represent - a way to  automatically generate a model from a set of properties. - a way to reason about non determinism, in a probabilistic setting as well as in a more traditional one, without probabilities.   This is interesting since non-determinism has been  a very important subject that has raised debates more than once. - a way to complete a categorical view of LMPs which, until now, has been stopped by the problem of existence of pullbacks when considering relations between LMPs.  We believe that these pullbacks may exist in the more general category of pre-LMPs. Another generalization of LMPs is with domain theory and  functional analysis.  We want to propose an abstract version of LMPs, by taking the point of view of linear functionals rather than probabilities (following a suggestion of Lawvere which has since proved very efficient in the context of domains and valuations).