Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2010

Abstract

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.

Keywords

Model Check, Temporal Logic, Markov Decision Process, Mutual Exclusion, Probabilistic Choice

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19

First Page

388

Last Page

403

ISBN

9783642169007

Identifier

10.1007/978-3-642-16901-4_26

Publisher

Springer Link

City or Country

Shanghai, China

Additional URL

https://doi.org/10.1007/978-3-642-16901-4_26

Download

Share

COinS