A new probable decision making approach for verification of probabilistic real-time systems

Probabilistic real-time systems have a difficult controlling management, because of their random behaviors and quantitative operations. So, the procedure of system behavior will changed any time. Adding a probable factor can effect on some systematic problems such as fairness, deadlock and starvation in a probabilistic real-time system. In this paper, we study on a new probable decision making approach for the probabilistic real-time systems using PAT and NuSMV model checkers. Also we analyze the verification methods and the feasibility of our approach on a case study by comparing two model checkers results. The experimental results show that the proposed approach performs substantially better than the other benchmark methods.