Reasoning About Probabilistic and Concurrent Systems

我的主要重点是开发技术来近似和推理连续状态马尔可夫决策过程。这些模型是机器学习、嵌入式系统和机器人技术的核心。在过去，我已经开发了一种近似方案，它构建了一组有限状态马尔可夫过程来近似给定的连续状态马尔可夫过程。我还开发了行为伪度量，当两个过程处于零距离时，它们是双相似的：没有观察可以区分它们。到目前为止，这项工作已经很好地建立起来，并产生了有趣的理论，但计算指标的成本很高。在接下来的一段时间里，我希望探索近似度量的新方法，并定义新的度量，这些度量也可以捕获有趣的行为相似性概念，但不那么严格，计算成本也不高。我使用的方法是使用对偶理论。我和我的合作者发现了对偶的一些惊人的结果。例如，Brzozowski在20世纪60年代提出的最小化有限自动机的卓越算法可以被视为对偶性的一个实例。这种一般观点的观点是，人们能够为加权自动机和概率自动机的最小化开发类似风格的算法。对偶定理也包含逻辑中的完备性结果。例如，Stone对偶定理包含了命题逻辑的完备性定理，Jonsson和Tarski的推广包含了模态完备性定理。2013年，我们发现了马尔可夫过程的惊人的stone型对偶性。这为加深我们对概率系统推理的定量逻辑（如概率模态逻辑）的理解开辟了道路。在提案中，我将讨论如何使用其他对偶性，如Gelfand对偶或凸对偶，来开发新的最小化技术和新的近似技术，用于加权转移系统和概率系统，如mdp和pomdp。我还将探讨马尔可夫过程的基本理论，以期为大型系统开发技术。***应用领域是机器学习，其中压缩大型系统的描述是很重要的，并且在概率系统的验证中，已知的为有限状态系统开发的模型检查技术可以扩展到定义在连续状态空间上的概率系统

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