Formal methods for labelled Markov processes

我研究的总体目标是建立关于并发概率过程的形式化推理方法。我尤其对具有连续状态空间的过程感兴趣，这是一种我们称为标记马尔可夫过程(LMP)的模型。可能应用的领域包括通信协议和过程控制软件。后者的一个例子是车辆等系统的控制器。我想继续发展LMP理论与其他领域的互动，但我的主要目标是沿着LMP的两个推广发展该理论。最近，我们定义了Pre-LMP，通过削弱LMP的概率结构上的属性来推广LMP；这导致了使用能力理论的概念，能力理论是为经济数学开发的理论。这个模型对于其他目标非常有希望，正如它可能代表的--一种从一组属性自动生成模型的方法。-一种在概率环境中以及在更传统的环境中推理非决定论的方式，而不是概率。他说这很有趣，因为非决定论一直是一个非常重要的主题，已经不止一次引发了辩论。-一种完成对LMP的明确观点的方式，到目前为止，在考虑LMP之间的关系时，这种观点因存在回调的问题而停止。我们认为，这些回调可能存在于LMP之前的更一般类别中。LMP的另一个推广是区域理论和泛函分析。我们想提出LMP的一个抽象版本，通过采取线性泛函而不是概率的观点(遵循Lawvere的建议，该建议后来被证明在领域和估值方面非常有效)。

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).