Probabilistic Analysis of Hybrid Systems

这项提议将汇集三个具体的、最新的进展来研究混合系统的行为，最引人注目的是那些传统算法方法由于可达性和omega语言问题无法确定而失败的系统。将使用的工具包括：1.概率进程代数PCSP模型的最新发展，其中非确定性选择和概率选择算子的预期规律成立；2.关于同时支持非确定性选择和概率选择的有限状态系统的推理的量化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.