Model checking 6 13 is an automated procedure for determining whether a finite state program satisfies a temporal property.Model checking tools, due to the complex nature of the specification methods, are used most effectively by verification experts. In order to make these tools more accessible to non-expert users, who may not be familiar with these formal notations, we need to make model checkers easier to use. Visually intuitive specification methods may provide an alternative way to specify temporal behavior.