Model checking hierarchical probabilistic systems
Probabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been designed for simple systems without hierarchy. In...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2010
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/5035 https://ink.library.smu.edu.sg/context/sis_research/article/6038/viewcontent/model.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| Summary: | Probabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been designed for simple systems without hierarchy. In this paper, we extend the PAT toolkit to support probabilistic model checking of hierarchical complex systems. We propose to use PCSP#, a combination of Hoare’s CSP with data and probability, to model such systems. In addition to temporal logic, we allow complex safety properties to be specified by non-probabilistic PCSP# model. Validity of the properties (with probability) is established by refinement checking. Furthermore, we show that refinement checking can be applied to verify probabilistic systems against safety/co-safety temporal logic properties efficiently. We demonstrate the usability and scalability of the extended PAT checker via automated verification of benchmark systems and comparison with state-of-art probabilistic model checkers. |
|---|