Secure Software Integration and Reliability Improvement Companion, IEEE International Conference on (2010)
June 9, 2010 to June 11, 2010
A probabilistic system is useful in modeling randomized algorithms (e.g., consensus algorithms), unreliable or unpredictable behaviors (e.g., human behaviors in decision making process), etc. Markov Decision Process (MDP) is used to construct this kind of system, because it has both nondeterministic and probabilistic choices. In this work, we study probabilistic models and analyze some issues such as reachability and LTL model checking with some new methods in calculating the probability.
Probabilistic, MDP, LTL, Model Checking
S. Song, "An Efficient Method of Probabilistic Model Checking," Secure Software Integration and Reliability Improvement Companion, IEEE International Conference on(SSIRI-C), Singapore, Singapore, 2010, pp. 24-25.