Reasoning About Probabilistic and Concurrent Systems

我的主要重点是开发技术来近似和推理连续状态马尔可夫决策过程。这些模型是机器学习、嵌入式系统和机器人技术的核心。我已经制定了，在过去，近似计划，构建一个家庭的有限状态马尔可夫过程，近似给定的连续状态马尔可夫过程。我还开发了行为伪度量，当两个过程处于零距离时，它们是双相似的：没有观察将区分它们。这项工作现在已经很好地建立起来，并导致有趣的理论，但度量计算是昂贵的。在接下来的一段时间里，我希望探索新的方法来近似度量，并定义新的度量，这些度量也可以捕捉到行为相似性的有趣概念，但计算起来并不那么严格和昂贵。我所采用的方法是使用对偶理论。 我和我的同事发现了一些二元性的惊人结果。例如，Brzozowski在20世纪60年代提出的最小化有限自动机的著名算法可以被看作是对偶的一个实例。这个一般观点的观点是，人们能够开发类似风格的算法，用于加权和概率自动机的最小化。对偶定理也是逻辑中的次完备性结果。例如，斯通对偶定理包含了命题逻辑的完备性定理和由琼森和塔斯基子模态完备性定理推广的完备性定理。在2013年，我们发现了马尔可夫过程的一个惊人的斯通型对偶。这为深化我们对定量逻辑（如概率模态逻辑）的理解开辟了道路，用于概率系统的推理。在建议中，我将讨论如何其他对偶，如Gelfand对偶或凸对偶，可以用来开发新的最小化技术和新的近似技术的加权过渡系统和概率系统，如MDPs和POMDPs。 我还将探索马尔可夫过程的基本理论，以期开发大型系统的技术。 应用领域是机器学习，压缩大型系统的描述是重要的，也在概率系统的验证中，已知的模型检查技术开发的有限状态系统可以扩展到连续状态空间上定义的概率系统。

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.