Probabilistic Analysis of Hybrid Systems

Tulane University, New Orleans LA

Investigators

Abstract

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, and 3. 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.