Probabilistic Analysis of Hybrid Systems

本提案将汇集三个具体的，最近的进展，以研究混合系统的行为，最显著的是那些传统的算法方法失败的系统，因为可达性和ω -语言问题是不可确定的。将使用的工具包括：1。本文研究了概率过程代数PCSP模型的最新进展，其中不确定性选择算子和概率选择算子的期望律都成立。最近发展的量化m-演算和相关的量化时间逻辑，用于推理支持不确定性选择和概率选择的有限状态系统；关于局部紧空间上简单测度的可表达性的最新结果——特别是在这样一个空间上的任何概率测度都是简单测度的有向上的事实。这些结果结合在一起，为混合系统建模提供了一种有趣而新颖的方法。

This proposal will bring together three specific, recent advances to study the behavior of hybrid systems, most notably those systems for which the traditional algorithmic methods fail because the reachability and omega-language problems are undecidable. The tools that will be used include:1. The recent development of a model for the probabilistic process algebra PCSP in which the expected laws for both nondeterministic choice and for probabilistic choice operators hold,2. The recent development of a quantified m-calculus and associated quantified temporal logic for reasoning about finite state systems that support both nondeterministic choice and probabilistic choice, and3. Recent results about the expressibility of simple measures on locally compact spaces - in particular, the fact that any probability measure on such a space is the directed supremum of simple measures.These results tie together to provide an interesting and novel approach to modeling hybrid systems.