Reasoning About Probabilistic and Concurrent Systems

我的主要重点是开发技术来近似和推理连续状态马尔可夫决策过程。这些模型是机器学习、嵌入式系统和机器人技术的核心。在过去，我已经开发了一种近似方案，它构建了一组有限状态马尔可夫过程来近似给定的连续状态马尔可夫过程。我还开发了行为伪度量，当两个过程处于零距离时，它们是双相似的：没有观察可以区分它们。到目前为止，这项工作已经很好地建立起来，并产生了有趣的理论，但计算指标的成本很高。在接下来的一段时间里，我希望探索近似度量的新方法，并定义新的度量，这些度量也可以捕获有趣的行为相似性概念，但不那么严格，计算成本也不高。我使用的方法是使用对偶理论。

My primary focus is to develop techniques to approximate and reason about continuous-state Markov decision processes. These models are central to machine learning, embedded systems and to robotics. I have developed, in the past, approximation schemes that construct a family of finite-state Markov processes that approximate given continuous-state Markov processes. I have also developed behavioural pseudo-metrics such that when two processes are at zero distance they are bisimilar: no observation will distinguish them. This work is well established by now and lead to interesting theory but the metrics are expensive to compute. In the coming period I wish to explore new ways of approximating the metrics and indeed defining new metrics that also capture interesting notions of behavioural similarity but are not so stringent and so expensive to compute. The methodology that I exploit is to use duality theory. My collborators and I have discovered some striking consequences of  duality. For example, Brzozowski's remarkable algorithm, from the 1960s, for minimizing finite automata can be viewed as an instance of duality. The point of this general view is that one is able to develop similar style algorithms for the minimization of weighted and probabilistic automata. Duality theorems also subsume completeness results in logic. For example, the Stone duality theorem subsumes the completeness theorems for propositional logic and generalizations by Jonsson and Tarski subsume modal completeness theorems. In 2013 we discovered a striking Stone-type duality for Markov processes. This opens the way to deepen our understanding of quantitative logics (like probabilistic modal logics) for reasoning about probabilistic systems. In the proposal I will discuss how other dualities, like Gelfand duality or convex duality, could be used to develop new minimization techniques and new approximation techniques for weighted transition systems and for probabilistic systems like MDPs and POMDPs.  I will also explore the fundamental theory of Markov processes with a view to developing techniques for large systems. The application areas are to machine learning where compressing decriptions  of large systems is important and also in verification of probabilistic systems where the known model-checking techniques developed for finite-state systems can be extended to probabilistic systems defined on continuous state spaces.