Model Checking Open Probabilistic Systems Using Hierarchical Probabilistic Automata

In this report we will systematically introduce using 1-HPA for model checking failure-prone open concurrent systems with respect to the non-extremal threshold language emptiness decision problem and the universal robustness problem. We have proved such problems are undecidable for 2-HPA but decidable for 1-HPA. We have developed two EXPTIME algorithms - backward algorithm and forward algorithm, and a tool - HiPAM, to model check 1-HPA, which can be obtained via combining open concurrent systems and properties expressed as deterministic automata. Properties are defined on system executions as either safety properties or non-safety properties. For some domain areas such as web applications, we have designed and implemented complete model abstraction techniques. When data models can be extracted from system models, such as in the domain of business process management, we have outlined a methodology to obtain failure specifications more precisely. Other contributions include verifying acyclic 1-HPA and proving that their language non-emptiness decision problem is NP-complete in general.