انجمن کامپیوتر ایران

We introduce a new tool for probabilistic model checking, GPMC, with a graphical user interface, and compare it with existing well-known tool in this scope PRISM. Some case studies are presented to show the efficiency and performance of it against PRISM. Two of these case studies are collected from several examples that were used for testing PRISM and another one is an extended simple example of a DTMC. We explain in each case study the powers and weaknesses of these tools, and find new methods for solving weaknesses.