Formal methods for labelled Markov processes

我的研究的总体目标是建立形式化的方法推理并发概率过程。 特别是，我对具有连续状态空间的过程感兴趣，我们称之为标记马尔可夫过程（LMP）的模型。 可能的应用领域包括通信协议和过程控制软件。 后者的一个例子是用于像车辆这样的系统的控制器。我想继续发展LMPs理论与其他领域的相互作用，但我的主要目标是沿着LMPs的两个概括发展理论。 在最近的过去，我们已经定义了前LMP，通过削弱其概率结构上的属性来推广LMP;这导致了与经济数学发展的理论能力理论的概念一起工作。 这个模型对于其他目标来说是非常有前途的，因为它可能代表了一种从一组属性自动生成模型的方法。- 一种在概率环境下以及在更传统的环境下，没有概率的情况下，对非决定论进行推理的方法。 这是有趣的，因为非决定论一直是一个非常重要的主题，已经引起了辩论不止一次。- 一种方法来完成一个明确的看法LMP，到目前为止，已停止的问题存在的回调时，考虑LMP之间的关系。 我们认为，这些回调可能存在于更一般的预LMP类别中。LMP的另一个推广是域理论和功能分析。 我们想提出一个抽象版本的LMPs，采取的角度来看，线性泛函，而不是概率（以下的建议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).