An Efficient Method of Probabilistic Model Checking

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.