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