Reasoning About Probabilistic and Concurrent Systems

关于概率和并发系统的推理

• 批准号: RGPIN-2015-05508
• 负责人: Panangaden, Prakash
• 金额: $ 3.64万
• 依托单位: McGill University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2016
• 资助国家: 加拿大
• 起止时间: 2016-01-01 至 2017-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=613593
• 关键词: Reasoning; About; Probabilistic; 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.

我的主要关注点是开发技术来近似和推理连续状态的马尔可夫决策过程。这些模型是机器学习、嵌入式系统和机器人学的核心。在过去，我已经开发了近似方案，这些方案构造了一族有限状态的马尔可夫过程，这些有限状态的马尔可夫过程逼近给定的连续状态的马尔可夫过程。我还开发了行为伪度量，即当两个过程处于零距离时，它们是两个相似的：任何观察都无法区分它们。到目前为止，这项工作已经得到了很好的证实，并将导致有趣的理论，但计算这些指标的成本很高。在接下来的一段时间里，我希望探索近似指标的新方法，甚至定义新的指标，这些指标也捕捉到行为相似性的有趣概念，但不那么严格，计算起来也不那么昂贵。我所采用的方法论是使用二元论。 我和我的合作者发现了这种二元性的一些惊人后果。例如，Brzozowski从20世纪60年代提出的用于最小化有限自动机的引人注目的算法可以被视为对偶的实例。这种一般观点的观点是，人们能够为加权和概率自动机的最小化开发类似风格的算法。对偶定理也将完备性结果包含在逻辑中。例如，斯通对偶定理包含了命题逻辑的完备性定理，Jonsson和Tarski的推广包含了情态完备性定理。2013年，我们发现了马尔可夫过程的一个惊人的Stone-型对偶。这为我们加深对关于概率系统的推理的定量逻辑(如概率模式逻辑)的理解开辟了道路。在提案中，我将讨论如何使用其他对偶，如Gelfand对偶或凸对偶，来为加权转移系统以及MDP和OPOMDP等概率系统开发新的最小化技术和新的逼近技术。我还将探索马尔可夫过程的基本理论，以期为大系统开发技术。 其应用领域是机器学习，其中压缩大系统的描述是重要的，也是在概率统计系统的验证中，其中为有限状态系统开发的已知模型检测技术可以扩展到定义在连续状态空间上的概率系统。