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: | , , |
|---|---|
| 格式: | text |
| 語言: | English |
| 出版: |
Institutional Knowledge at Singapore Management University
2010
|
| 主題: | |
| 在線閱讀: | https://ink.library.smu.edu.sg/sis_research/5035 https://ink.library.smu.edu.sg/context/sis_research/article/6038/viewcontent/model.pdf |
| 標簽: |
添加標簽
沒有標簽, 成為第一個標記此記錄!
|
| 總結: | 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. |
|---|